AI has made staggering progress in mathematics in recent months, unearthing solutions to thorny puzzles that evaded humans for decades. Key to technology companies being able to announce these complex new findings, confident in their correctness, is a niche field called formalisation.
But recently, the developers behind formalisation tools have realised that the AI models have the potential to cheat their way to success. Now, the battle is on to tighten up the tools and prevent that from happening. 聽
Formalising mathematical theorems essentially turns them into code that allows computers to grapple with them directly, methodically working through the logic and exposing any flaws. The process is so thorough that if a theorem comes through intact, it is considered to have been proved correct beyond all reasonable doubt.聽
Advertisement
The leading software to do this, Lean, has risen to prominence in the AI world as a convenient way for technology giants to quickly and decisively prove the output of their models.聽It鈥檚 by using Lean that the companies can make bold announcements about solving complex puzzles. Without it, they would only be able to claim they had found a possible solution to the puzzles and then invite human mathematicians to assess the solutions 鈥� work that might take weeks or months.
created Lean in the 2010s while working at Microsoft Research. He says that the software was initially a niche tool used only by human mathematicians, and that there were never any attempts at trickery or manipulation.聽
That all changed in July this year when software engineer Ramana Kumar announced he had disproved the Collatz conjecture 鈥� one of the most famous open problems in all of mathematics 鈥� and published a Lean formalisation to back up his claim.聽
De Moura was surprised by the breakthrough, but it seemed legitimate. Not least of the reasons for believing so was that the code had been approved by both the standard Lean kernel 鈥� the tiny bit of code at the heart of Lean that actually checks the mathematics 鈥� and also a separately developed one designed for Lean, called Nanoda. Lean allows for, and actively encourages, the creation of different kernels because variety equals safety; a specific bug that makes something true look false, or vice versa, in one kernel is vanishingly unlikely to appear in another. Formalised code checked by two kernels was as water-tight as things got.
But then it turned out that Kumar鈥檚 disproof wasn鈥檛 what it seemed. He had used AI to discover and exploit two separate bugs in two separate kernels, within the Lean code.聽
鈥淸The AI] managed to do something that we thought was impossible,鈥� says de Moura. 鈥淚t found different bugs and managed to craft a problem that exploited both of them. After that we were really worried. It was clear we had to improve.鈥�
Kumar told New 精东传媒 that he thought the stunt would be 鈥渦seful to throw some cold water on the hype鈥� of formalisation. He didn鈥檛 respond to follow-up questions on why he didn鈥檛 then disclose the bugs he had found so that they could be fixed. In any case, a fix was published .
Regardless of Kumar鈥檚 motivations, it certainly concerned de Moura, the 20 or so full-time developers working on Lean and mathematicians. They feared that malicious actors could use AI to pull such stunts, as Kumar had done.
But they also worried that AI might perform something similar unprompted. When faced with a serious challenge like formalising a fiendishly difficult and complex piece of mathematics, AI might actually find it easier to simply hack Lean and give the appearance of success. This so-called 鈥渞eward hacking鈥� can occur when AI is given vague instructions, and researchers have already seen rather than actually doing their homework.聽
The first thing Lean鈥檚 developers did was to formalise their own kernel, using Lean to check the code at the heart of Lean 鈥� an oddly self-referential safety check 鈥� and verify that there were no bugs that could be exploited. They then used AI to convert that kernel into a different programming language, and verified that second one as well. A third kernel written from scratch was also verified. This gave developers a greater sense of security, but it didn鈥檛 necessarily mean that Lean was infallible.
at the University of Bonn in Germany says there was a vanishingly small chance that Lean had a very unusual bug that caused it to report itself as error-free even when it wasn鈥檛. If such a bug existed, the boot-strapping safety measures would have been meaningless. 鈥淭hat is completely possible, but in practice this would be very weird,鈥� says van Doorn.
To get around this issue, the Lean developers made a lot more kernels, as diverse as possible, built on all types of software and hardware, to increasingly lower the chances of finding a bug that worked universally. These kernels are where league tables record how well they鈥檝e done on known true and false proofs, and unusual problems that have been shown to trip up kernels in the past.聽
The researchers are now also taking steps to push these kernels into wider use 鈥� they only help if they鈥檙e deployed. Lean, which is open source, currently ships with just one, and it鈥檚 on the user to check their code with others if they want more security. But because of the surprising complexity of AI attacks, the next version will ship with four different kernels as standard.聽
Developers now believe that Kumar鈥檚 approach would no longer succeed. 鈥淲e want to get much closer to this idea of being bulletproof,鈥� says de Moura. 鈥淚 can tell you that we鈥檙e sleeping much better now. We don鈥檛 believe the existing AI will be able to break all these layers of defence.鈥�
Even now, though, there are risks. The diversity of kernels makes the chance of a universal bug that works on them all smaller, but not zero 鈥� and future AI models may become so capable that they can continue to find convoluted exploits that somehow work across the board on all kernels.
For instance, when working with engineers from OpenAI, the Lean team found a bug in the runtime of their program 鈥� the compiled code that is actually executed by a computer, constructed from the source code using a tool called a compiler. Exploiting this bug, they managed to incorrectly prove a conjecture that is false. The error cropped up because the compiler wasn鈥檛 perfect, not because Lean鈥檚 code had an error.聽
So the ultimate aim is to show that one particular computer setup, with hardware and software of specified standards, is formalised, verified and guaranteed error-free. This would give Lean users the reassurance not only that the kernel is free of mistakes, but also that the compiler, operating system and hardware are error-free, too. Totally trustable from top to bottom. 鈥淭hat鈥檚 the dream,鈥� says de Moura. But it will take a vast effort.聽
There are other problems. Lean code is a programming language, so it can be crafted to do anything the user wants 鈥� including malicious trickery, says van Doorn.聽This could involve simply writing in the output file created by Lean that a theorem was correct, even if it was false, or changing the actual source code that makes up Lean itself to manipulate results, or report that every proof tried from them on was correct.
鈥淵ou can redefine addition.鈥〢nd then you can prove Fermat鈥檚 last theorem, which mentions addition, and you can say you鈥檝e done it,鈥� says at Imperial College London. 鈥淏ut then when people actually look at what you鈥檝e really done, you haven鈥檛 done it.鈥�
These loopholes are also now being closed in Lean. Another effort involves Google DeepMind, which that have been explicitly defined in Lean and then checked carefully by mathematicians. Anyone claiming to have solved one of these problems can take the appropriate definition off the shelf and use it in an unmodified form to test their proposed proof in Lean. Doing so would demonstrate that they are not trying to cheat by subtly altering the definition of the problem to make it far easier to solve.
When OpenAI solved the Navier-Stokes puzzle earlier this month, for example, we knew it was on stable ground because the statement provided to Lean was taken directly from the Formal Conjectures list.
But for some, none of these efforts will ever be enough.
鈥淐omputer scientists are, in general, very paranoid people, and probably with good reason because they鈥檝e seen all sorts of things,鈥� says Buzzard. 鈥淵ou can find people that will never believe anything. You say 鈥業鈥檝e checked it a million times鈥� and they say 鈥榳ell, what about gamma rays [flipping bits in memory], did you check for them?鈥� There are some people that you can never convince.鈥�
