An AI developed by Google DeepMind has made history by securing a silver medal at this year’s International Mathematical Olympiad (IMO), marking the first instance of an AI achieving a podium finish in this esteemed competition.
Regarded as the pinnacle of contests for young mathematicians, the IMO challenges participants with complex mathematical problems that traditionally exceed the capabilities of AI systems.
Earlier this year, Google DeepMind introduced AlphaGeometry, an AI capable of solving certain geometry problems presented at the IMO, although it was not part of a live competition and struggled with other fields like number theory, algebra, and combinatorics necessary for medal contention.
The newly launched AlphaProof AI displays enhanced capabilities, managing a wider array of mathematical problems alongside an upgraded version of AlphaGeometry that addresses more geometric queries.
In testing both systems against this year’s IMO problems, they achieved a score of 28 out of 42 points by correctly answering four out of six challenges, just one point shy of the gold medal threshold.
The 2023 contest held in Bath, UK, recognized 58 gold medal winners and 123 silver medalists.
Gregor Dolinar, the IMO president remarked on the AI’s progress, stating, “We are all very much aware that AI will eventually be better than humans at solving most mathematical problems, but the rate at which AI is improving is breathtaking.” He noted that missing the gold medal by just one point is an impressive feat.
Timothy Gowers from the University of Cambridge, who assessed AlphaProof’s submissions, expressed surprise at its performance, indicating it found “magic keys” to problem-solving akin to human reasoning. He acknowledged that some tricky problems were solved by the AI in unexpected ways.
AlphaProof utilizes a reinforcement learning approach similar to that of previous Google DeepMind AIs, which have outperformed human champions in games like chess and Go. This technique involves learning from numerous attempts to solve complex problems. However, its effectiveness relies on a substantial problem set presented in a form the AI can digest, while many IMO problems are articulated in English.
To enhance its problem-solving ability, the DeepMind team utilized a separate language model to translate the problems into a programming language called Lean, enabling the AI to learn and verify solutions effectively.
“Initially, it starts with simpler problems, gradually tackling more challenging ones as it learns,” said Hubert from DeepMind. The system outputs its solutions in Lean, facilitating instant verification.
Despite its remarkable achievements, AlphaProof operates at a slower pace, with some solutions taking up to three days to compute, compared to the allotted 4.5 hours for three questions during the competition. It also struggled with combinatorial problems, an area where further investigation is needed according to DeepMind’s Alex Davies.
There remains uncertainty about how AlphaProof derives its solutions and whether it employs mathematical intuition like humans do. Nevertheless, its capability to convert proofs from Lean into English ensures they can be easily verified.
The accomplishments of AlphaProof represent a significant milestone in the development of AI in mathematics. Geordie Williamson from the University of Sydney commented, “Many previous attempts at leveraging reinforcement learning on formal proofs have yielded limited success.”
While AlphaProof has the potential to assist professional mathematicians in developing proofs, it does not address the crucial task of identifying solvable problems—an area that occupies a significant amount of research time, according to a London Institute expert.
Hubert stated that the ultimate goal is for AlphaProof to contribute to enhancing Google’s language models by minimizing inaccuracies.
Additionally, XTX Markets has announced a $5 million prize for an AI capable of achieving a gold medal in the IMO, but AlphaProof is not eligible due to its non-public status. “We hope that DeepMind’s progress will inspire further competition entries and welcome a public submission from them,” remarked XTX Markets’ Alex Gerko.
