Google DeepMind announces that it has developed an AI that can achieve silver medal-level scores in mathematics Olympiad problems



Google DeepMind has announced a new reinforcement learning-based system for formal mathematical reasoning called 'AlphaProof' and a geometry solving system called 'AlphaGeometry 2.' The combination of these two systems is said to have achieved a silver medal-level score at the International Mathematical Olympiad (IMO).

AI achieves silver-medal standard solving International Mathematical Olympiad problems - Google DeepMind

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/



The International Mathematical Olympiad consists of six questions, each scored out of a maximum of seven points. If all questions are answered correctly, the total score is 42 points, and gold, silver, and bronze medals are awarded to the top students at a certain percentage of the total.

AlphaProof, developed by Google DeepMind, won full marks in two algebra problems and one number theory problem. AlphaGeometry 2 also won full marks in the geometry problem, giving it a total score of 28 points. Unfortunately, the gold medal line for the 2024 International Mathematical Olympiad is 29 points, so they did not win the gold medal.



AlphaProof is a model that combines AlphaZero's reinforcement learning algorithm with a pre-trained language model, and trains itself to prove mathematical statements in

a formal language called Lean . Formal languages have the advantage over natural languages in that they allow for formal verification of the 'correctness' of mathematical inference, but they have the disadvantage that the amount of data available for training is overwhelmingly small.

The Google DeepMind team used Google's AI, Gemini , to automatically translate natural language problems into formal language to supplement the amount of data, allowing them to train on millions of problems covering a wide range of difficulty levels and mathematical topic areas.

The training loop for AlphaProof looks like this: Approximately one million natural language problems are converted into formal language by the formalization network, and the solver network searches for proofs or disproofs of the problems. If the search is successful, the solver network is trained through the AlphaZero algorithm to solve more difficult problems.



On the other hand, AlphaGeometry 2 is an AI model specialized for geometry problems. Its predecessor, AlphaGeometry, achieved gold medal-level scores at the International Mathematical Olympiad when it came to geometry problems alone.

Google DeepMind announces 'AlphaGeometry', an AI that can solve geometry problems at the level of the Mathematical Olympiad, demonstrating performance close to that of a human gold medalist - GIGAZINE



AlphaGeometry 2 has been trained from scratch on an order of magnitude more synthetic data, and has significantly improved AlphaGeometry's accuracy rate from 53% to 83% in geometry problems in the past 25 years of the International Mathematical Olympiad. In the 2024 International Mathematical Olympiad geometry problem, it was able to solve it in 19 seconds after the problem formulation was completed.



The Google DeepMind team also experimented with a natural language inference system that can answer questions without translating them into a formal language, with 'very promising results.' The team also said it plans to release technical details about AlphaProof soon.

in Software, Posted by log1d_ts