AlphaGeometry is anartificial intelligence (AI) program that can solve hard problems inEuclidean geometry. The system comprises a data-driven large language model (LLM) and a rule-based symbolic engine (Deductive DatabaseArithmetic Reasoning). It was developed byDeepMind, a subsidiary ofGoogle. The program solved 25 geometry problems out of 30 from theInternational Mathematical Olympiad (IMO) under competition time limits—a performance almost as good as the average human gold medallist. For comparison, the previous AI program, calledWu's method, managed to solve only 10 problems.[1][2]
DeepMind published a paper about AlphaGeometry in the peer-reviewed journalNature on 17 January 2024.[3] AlphaGeometry was featured inMIT Technology Review on the same day.[4]
Traditional geometry programs aresymbolic engines that rely exclusively on human-codedrules to generate rigorous proofs, which makes them lack flexibility in unusual situations. AlphaGeometry combines such a symbolic engine with a specializedlarge language model trained onsynthetic data of geometrical proofs. When the symbolic engine doesn't manage to find a formal and rigorous proof on its own, it solicits the large language model, which suggests a geometrical construct to move forward. However, it is unclear how applicable this method is to other domains of mathematics or reasoning, because symbolic engines rely on domain-specific rules and because of the need for synthetic data.[5]
AlphaGeometry 2 is an improved version of AlphaGeometry, published on February 5, 2025. They added more features to the representation language to describe more geometry problems that involve movements of objects, and problems containing linear equations of angles, ratios, and distances. They targeted IMO geometry questions from 2000 to 2024. The expanded representation language allowed them to cover 88% of the questions.[6][7][8]
It usesGemini finetuned on a synthetically generated dataset of problems and solutions in the representation language. The model is used for making auxiliary constructions like lines and points, to help the tree search. It is also used forautoformalization, i.e. converting a problem in English to a problem in the representation language.[8]
Thisartificial neural network-related article is astub. You can help Wikipedia byexpanding it. |