![\"\"](\"https:\/\/images.newscientist.com\/wp-content\/uploads\/2024\/07\/25144939\/SEI_214089039.jpg\")
<\/div>DeepMind\u2019s AlphaProof AI can tackle a range of mathematical problems<\/p>\n
Google DeepMind<\/p>\n<\/div>\n<\/figcaption><\/figure>\n<\/p>\n
An AI from Google DeepMind has achieved a silver medal score at this year\u2019s International Mathematical Olympiad (IMO), the first time any AI has made it to the podium.<\/p>\n
The IMO is considered the world\u2019s most prestigious competition for young mathematicians. Correctly answering its test questions requires mathematical ability that AI systems typically lack.<\/p>\n
In January, Google DeepMind demonstrated AlphaGeometry<\/a>, an AI system that could answer some IMO geometry questions as well as humans. However, this was not from a live competition, and it couldn\u2019t answer questions from other mathematical disciplines, such as number theory, algebra and combinatorics, which is necessary to win an IMO medal.<\/p>\n Google DeepMind has now released a new AI, called AlphaProof, which can solve a wider range of mathematical problems, and an improved version of AlphaGeometry, which can solve more geometry questions.<\/p>\n When the team tested both systems together on this year\u2019s IMO questions, they answered four out of six questions correctly, giving them a score of 28 out of a possible 42 points. This was enough to win a silver medal and just one point under this year\u2019s gold medal threshold.<\/p>\n At the contest in Bath, UK, last week, 58 entrants won a gold medal and 123 won a silver medal.<\/p>\n <\/p>\n \u201cWe 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,\u201d says Gregor Dolinar<\/a>, the IMO president. \u201cMissing the gold medal at IMO 2024 by just one point a few days ago is truly impressive.\u201d<\/p>\n At a press conference, Timothy Gowers<\/a> at the University of Cambridge, who helped mark AlphaProof\u2019s answers, said the AI\u2019s performance was surprising and it appeared to find \u201cmagic keys\u201d to answer problems in a similar way to humans. \u201cI thought that these magic keys would probably be a little bit beyond what it could do, so it came as quite a surprise in one or two instances when the program had indeed found these keys,\u201d said Gowers.<\/p>\n AlphaProof works similarly to Google DeepMind\u2019s previous AIs that can beat the best humans at chess<\/a> and Go<\/a>. All of these AIs rely on a trial-and-error approach called reinforcement learning,\u00a0 where the system finds its own way to solve a problem over many attempts. However, this method requires a large set of problems written in language that the AI can understand and verify, whereas most IMO-like problems are written in English.<\/p>\n To get around this, Thomas Hubert<\/a> at DeepMind and his colleagues used Google\u2019s Gemini AI, a language model like the one that powers ChatGPT, to translate these problems into a programming language called Lean so that the AI could learn how to solve them.<\/p>\n \u201cAt the beginning, it will be able to solve perhaps the simplest problems, and learn from solving those simpler problems to attack harder and harder problems,\u201d Hubert said at the press conference. It also produces its answers in Lean, so they can be instantly verified as correct.<\/p>\n While AlphaProof\u2019s performance is impressive, it works slowly, taking up to three days to find some solutions instead of the 4.5 hours per three questions that competitors are allowed. It also failed to answer both questions on combinatorics, which is the study of counting and arranging numbers. \u201cWe are still working to understand why this is, which will hopefully lead us to improve the system,\u201d says Alex Davies<\/a> at Google DeepMind.<\/p>\n It is also not clear how AlphaProof arrives at its answers or whether it uses the same kind of mathematical intuitions that humans do, said Gowers, but its ability to translate proofs from Lean into English makes it easy to check they are correct.<\/p>\n The result is impressive and a significant milestone, says Geordie Williamson<\/a> at the University of Sydney, Australia. \u201cThere have been many previous attempts to do reinforcement learning on formal proofs and none have had much success.\u201d<\/p>\n While a system like AlphaProof could be useful for working mathematicians in helping develop proofs, it obviously can\u2019t help with identifying problems to solve and work on, which takes up a large portion of researchers\u2019 time, says Yang-Hui He<\/a> at the London Institute for Mathematical Sciences.<\/p>\n Hubert said his team hopes that AlphaProof will be able to help improve Google\u2019s large language models, like Gemini, by reducing incorrect responses.<\/p>\n The trading company XTX Markets has offered a $5 million prize \u2013 called the AI Mathematical Olympiad \u2013 for an AI capable of achieving a gold medal at the IMO, but AlphaProof is not eligible because it is not publicly available. \u201cWe hope that DeepMind\u2019s advances will inspire more teams to enter the AIMO Prize, and would of course welcome a public entry from DeepMind themselves,\u201d says Alex Gerko at XTX Markets.<\/p>\n Topics:<\/p>\n<\/section><\/div>\n