New Scientist
AI is solving mathematical puzzles that have stumped humans for decades, but it has also discovered how to fake its own developments.
The battle for mathematical truth
Author: Matthew Sparkes
AI HAS made staggering progress in mathematics in recent months, unearthing solutions to thorny puzzles that had evaded humans for decades. Key to technology firms 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, 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 beyond all reasonable doubt.
The leading software to do this, Lean, has risen to prominence as a convenient way for tech giants to quickly and decisively prove the output of their AI models. 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.
Leonardo de Moura 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, when software engineer Ramana Kumar announced he had disproved the Collatz conjecture and published a Lean formalisation to back up his claim.
De Moura was surprised by the breakthrough, but it seemed legitimate, not least because 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 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’s disproof wasn’t 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. “It 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 Scientist that he thought the stunt would be “useful to throw some cold water on the hype” of formalisation. He didn’t respond to follow-up questions on why he didn’t then disclose the bugs he had found so that they could be fixed. In any case, a fix was published an hour after the bug was officially logged.
The experience concerned de Moura, the 20 or so full-time developers working on Lean and mathematicians. They worried that AI might perform something similar unprompted. When faced with formalising a fiendishly difficult and complex piece of mathematics, AI might find it easier to hack Lean and give the appearance of success. This “reward hacking” can occur when an AI is given vague instructions, and researchers have already seen evidence of models trying to exploit Lean bugs rather than actually doing their homework.
The AI found different bugs and managed to craft a problem that exploited both of them
The first thing Lean’s developers did was to formalise their own kernel, using Lean to check the code at the heart of the software and verify 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’t necessarily mean that Lean was infallible.
Floris van Doorn at the University of Bonn in Germany says there was a vanishingly small chance that Lean had an unusual bug that caused it to report itself as error-free even when it wasn’t. If so, the boot-strapping safety measures would have been meaningless. “That 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 tested head to head in a battle arena website where league tables record how well they have 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. Lean, which is open source, currently ships with just one, and it is on the user to check their code with others if they want more security. But because of the complexity of AI attacks, the next version will ship with four different kernels as standard.
Defensive moves
Developers now believe Kumar’s approach would no longer succeed. “We want to get much closer to this idea of being bulletproof,” says de Moura. “We don’t believe the existing AI will be able to break all these layers of defence.”
There are still risks, however. 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 its program – the compiled code that is actually executed by a computer, created 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’t perfect, not because Lean’s code had an error.
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 that it is totally trustworthy from top to bottom. “That’s the dream,” says de Moura.
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.
“You can redefine addition. And then you can prove Fermat’s last theorem, which mentions addition, and you can say you’ve done it,” says Kevin Buzzard at Imperial College London. “But then when people actually look at what you’ve really done, you haven’t done it.”
These loopholes are also now being closed in Lean. Another effort involves Google DeepMind, which maintains a list of open mathematics problems that have been explicitly defined in Lean and then checked carefully by mathematicians. Anyone claiming to have solved one of these 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 aren’t trying to cheat by subtly altering the definition of the problem to make it easier to solve.
We don’t believe the existing AI will be able to break all these layers of defence
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. “You can find people that will never believe anything,” says Buzzard. “You say ‘I’ve checked it a million times’ and they say ‘well, what about gamma rays [flipping bits in memory], did you check for them?’ There are some people that you can never convince.”
Credits: TCA, LLC.