AlphaProof and AlphaGeometry: Learning to Communicate with Mathematicians Using Neural-Symbolic Methods
AlphaProof combines a language model with the technique of reinforcement learning, using the ‘AlphaZero’ engine the company has employed successfully for attacking games such as Go as well as some specific mathematical problems. Neural networks learn by trial-and-error. This works well when its answers can be evaluated by some objective metric. AlphaProof was trained to read and write proof in the same language as the proof assistant software package that is popular with mathematicians. AlphaProof ran its outputs in the Lean package to see if they were correct and it filled in some of the steps in the code.
Indeed, the research raises the prospect of addressing the worst tendencies of large language models by applying logic and reasoning in a more grounded fashion. As impressive as the large language models are, they are often unable to comprehend even basic math or reason logically.
In the future, the neural-symbolic method could be used to turn questions and tasks into forms that can be reasoned over in a way that produces reliable results. The system is known asStrawberry and Openai is rumored to be working on it.
The systems revealed today have a limitation, as Silver acknowledges. AlphaProof and AlphaGeometry are able to work their way toward the right answer through correct or incorrect math solutions. Many real-world problems have a lot of possibilities, and which one is the right solution may be unclear. Silver says the solution for more ambiguous questions may be for a language model to try to determine what constitutes a “right” answer during training. “There’s a spectrum of different things that can be tried,” he says.
Silver is also careful to note that Google DeepMind won’t be putting human mathematicians out of jobs. He says that mathematicians do more than just provide a system that can prove anything. “A big part of mathematics is to pose problems and find what are the interesting questions to ask. You might think of this as another tool along the lines of a slide rule or calculator or computational tools.”
AlphaProof, a Frankensteinian Theorem Prover for High School Students, at the 2024 International Math Olympiad
Their new Frankensteinian creation, dubbed AlphaProof, has demonstrated its prowess by tackling several problems from the 2024 International Math Olympiad (IMO), a prestigious competition for high school students.
Several years before ChatGPT began jibber-jabbering away, Google developed a very different kind of artificial intelligence program called AlphaGo that learned to play the board game Go with superhuman skill through tireless practice.
“This is the first time any AI system has been able to achieve medal-level performance”, said Pushmeet Kohli, vice-president of AI for science at DeepMind, in a briefing to reporters. The journey of building advanced theorem provers is a key milestone in the process.
In their latest effort, the researchers used AlphaGeometry2 to solve the geometry problem in under 20 seconds; the AI is an improved and faster version of their record-setting system, says DeepMind computer scientist Thang Luong.
A team of researchers from software companies Numina and Huggingface used a language model to win an intermediate AIMO progress prize. The companies made their systems available for anyone to download. Nature told the winners that language models alone wouldn’t be enough to solve harder problems.
Many of the Lean translations were nonsensical, but enough were good enough to get AlphaProof to the point that it could start its reinforcement-learning cycles. The results were much better than expectations, Gowers said at the press briefing. There are some problems in the IMO that have this magic-key property. The issue looks hard at first until you can find a magic key that unlocks it.
“It’s clearly a very substantial advance,” says Joseph Myers, a mathematician based in Cambridge, UK, who — together with Fields Medal-winner Tim Gowers — vetted the solutions and who had helped select the original problems for this year’s IMO.
In the mid-2010s David Silver was the lead researcher in developing AlphaGo, and he said that problems that are challenging to the best young mathematicians in the world could be proof of not open research problems.
Even though the techniques could be perfect to the point of doing research-level work in mathematics, it’s not known, according to the press briefing. Is it possible that it could extend to other types of mathematics, where there might not be a million problems to solve?
