Hubbry Logo
search
logo
AlphaGeometry avatar
AlphaGeometry
AlphaGeometry
current hub
A

AlphaGeometry

logo
Community Hub0 Subscribers
Read side by side
AlphaGeometry
View on Wikipedia
from Wikipedia

AlphaGeometry is an artificial intelligence (AI) program that can solve hard problems in Euclidean geometry. The system comprises a data-driven large language model (LLM) and a rule-based symbolic engine (Deductive Database Arithmetic Reasoning). It was developed by DeepMind, a subsidiary of Google. The program solved 25 geometry problems out of 30 from the International Mathematical Olympiad (IMO) under competition time limits—a performance almost as good as the average human gold medallist. For comparison, the previous AI program, called Wu's method, managed to solve only 10 problems.[1][2]

DeepMind published a paper about AlphaGeometry in the peer-reviewed journal Nature on 17 January 2024.[3] AlphaGeometry was featured in MIT Technology Review on the same day.[4]

Traditional geometry programs are symbolic engines that rely exclusively on human-coded rules to generate rigorous proofs, which makes them lack flexibility in unusual situations. AlphaGeometry combines such a symbolic engine with a specialized large language model trained on synthetic 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

[edit]

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 uses Gemini 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 for autoformalization, i.e. converting a problem in English to a problem in the representation language.[8]

References

[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

AlphaGeometry

View on Grokipedia
from Grokipedia
AlphaGeometry is an artificial intelligence system developed by Google DeepMind for solving Olympiad-level Euclidean geometry problems, employing a neuro-symbolic approach that integrates a neural language model with a symbolic deduction engine, and trained entirely on synthetic data without relying on human demonstrations.[1][2] Announced on January 17, 2024, the system achieved a breakthrough by solving 25 out of 30 geometry problems from the International Mathematical Olympiad (IMO), demonstrating performance comparable to that of human experts and marking a significant advancement in AI-driven mathematical reasoning.[1][2] In July 2024, an enhanced version called AlphaGeometry 2 was released. Combined with AlphaProof, these systems attained silver-medal standard on the 2024 IMO. In February 2025, AlphaGeometry 2 was shown to achieve gold-medalist level performance in solving Olympiad geometry problems, with an 84% success rate (42 out of 50) on IMO geometry problems from 2000–2024, surpassing the average gold medalist performance, and an improved coverage rate of 88%. These advancements resulted from refinements in its language model and integration with systems like AlphaProof for broader mathematical problem-solving.[3][4]

Development

Announcement

AlphaGeometry was publicly announced by Google DeepMind on January 17, 2024, through a blog post detailing its capabilities in solving Olympiad-level geometry problems.[1] The announcement highlighted the system's neuro-symbolic approach, which combines a neural language model with a symbolic deduction engine to achieve performance comparable to human experts.[1] On the same date, the research was published in the journal Nature under the title "Solving olympiad geometry without human demonstrations," with DOI 10.1038/s41586-023-06747-5.[2] The paper emphasized AlphaGeometry's key achievement of solving 25 out of 30 geometry problems from the International Mathematical Olympiad (IMO) from 2000 to 2022, demonstrating its efficacy on challenging, competition-level tasks without relying on human demonstrations.[2][1] In conjunction with the announcement and publication, Google DeepMind released a GitHub repository containing the code to reproduce the DDAR and AlphaGeometry systems, enabling researchers to verify and build upon the work.[5][1]

Research Team

AlphaGeometry was developed by a team at Google DeepMind, a British-American artificial intelligence research laboratory and subsidiary of Alphabet Inc., which has been advancing AI systems for mathematical reasoning, including efforts following its integration with Google Brain in 2023.[1][6][7] The project reflects DeepMind's broader initiatives in AI for mathematics, building on prior efforts to pioneer mathematical reasoning capabilities.[1] The lead researchers on AlphaGeometry were Trieu Trinh and Thang Luong, both affiliated with Google DeepMind, who spearheaded the system's design and implementation.[1] Key contributions came from experts including Yuhuai Wu, Quoc Le, and He He.[1] The team also included collaborators such as Rif A. Saurous, Denny Zhou, and Christian Szegedy from Google DeepMind, alongside support from academic partners.[1] The development involved a collaboration between Google DeepMind and the Computer Science Department of New York University, highlighting interdisciplinary ties between industry and academia.[1] Additional input was received from He He's research group at NYU and external experts like Evan Chen, a former International Mathematical Olympiad gold medalist who evaluated the system's solutions.[1] Google Research played a supporting role, contributing to the foundational work in AI-driven mathematical problem-solving that informed AlphaGeometry.[1] The team's prior work laid the groundwork for AlphaGeometry, including projects like FunSearch for discovering solutions in mathematical sciences and explorations in pure mathematics using AI, demonstrating their expertise in neuro-symbolic approaches to reasoning.[1] This background extended to related initiatives such as AlphaProof, which further advanced AI capabilities in formal mathematical proofs, underscoring the team's ongoing contributions to AI for mathematics.[3] Overall leadership and advisory support came from Google DeepMind executives including Demis Hassabis, Pushmeet Kohli, and Koray Kavukcuoglu, ensuring alignment with the organization's mission in safe and beneficial AI.[1]

Architecture

Neural Language Model

The neural language model in AlphaGeometry is a transformer-based architecture trained from scratch, consisting of 12 layers, an embedding dimension of 1,024, eight attention heads, and a total of 151 million parameters excluding embeddings.[2] This model employs a customized tokenizer with a vocabulary size of 757 and supports a maximum context length of 1,024 tokens using T5-style relative position embeddings.[2] It serializes geometry problems, including premises, conclusions, and proofs, into text strings to enable next-token prediction during training and inference.[2] The primary purpose of the neural language model is to generate candidate auxiliary constructions, such as new points, lines, or circles, to guide the proof search process by expanding the deduction closure when the symbolic engine reaches a limit.[2] These constructions serve as heuristics that address the infinite branching factor in geometry theorem proving, allowing the system to explore promising paths toward solutions for Olympiad-level problems.[2] During operation, the model takes the current proof state as input and predicts multiple candidate auxiliary constructions (up to 512 via beam search) per iteration, which are then verified and evaluated by the symbolic deduction engine.[2] This integration enables the neuro-symbolic system to combine probabilistic generation with deterministic reasoning in a looped manner.[2] A key innovation is the use of constrained decoding via beam search, which generates up to 512 candidate constructions in parallel while ensuring they produce syntactically valid geometry statements compatible with the symbolic engine.[2] This approach limits the search space to feasible, rule-adherent outputs, preventing invalid or irrelevant suggestions that could derail the proof process.[2] The model was pretrained on 100 million unique synthetic proofs to learn deduction patterns and fine-tuned on a subset of 9 million proofs requiring auxiliary constructions, enhancing its ability to propose effective heuristics without relying on human-designed rules.[2]

Symbolic Deduction Engine

The symbolic deduction engine in AlphaGeometry, referred to as DD + AR (deductive database combined with algebraic reasoning), is a rule-based system that applies hand-crafted geometric rules to verify and generate formal proofs for Euclidean geometry problems.[2] It operates deterministically, using forward deduction to iteratively derive new true statements from initial premises until no further inferences are possible, thereby expanding the search space of possible proof steps.[2] This process forms a directed acyclic graph of conclusions based on definite Horn clauses, enabling efficient exploration of geometric relationships.[2] In addition to forward deduction, the engine incorporates backward deduction via a traceback algorithm, which recursively identifies minimal dependencies and proof subgraphs starting from a target conclusion, aiding in proof reconstruction and verification.[2] The engine handles core Euclidean geometry primitives, including points, lines, and circles, within a specialized formal language that supports predicates such as collinearity, concurrency, and cyclicity, along with algebraic reasoning for angles, ratios, and distances.[2] This allows it to model non-degeneracy and topological assumptions typical of Olympiad problems.[1] AlphaGeometry's symbolic engine addresses key limitations of pure symbolic systems, such as slow inference and inflexibility in handling complex auxiliary constructions, by leveraging guidance from the neural language model to suggest relevant additions while maintaining verifiable rule-based reasoning.[1]

Integration Mechanism

AlphaGeometry employs a hybrid neuro-symbolic approach that integrates a neural language model with a symbolic deduction engine to solve complex geometry problems. The neural language model generates proposals for auxiliary constructions, such as adding points, lines, or circles to the diagram, which guide the exploration of potential proof paths. These proposals are then processed by the symbolic deduction engine, which verifies and expands them using formal geometric rules and algebraic reasoning to derive new statements about the diagram. This interaction enables the system to combine the intuitive, pattern-based predictions of the neural component with the rigorous, verifiable logic of the symbolic component.[2][1] The search process in AlphaGeometry utilizes beam search with a beam size of 512 to efficiently navigate the vast space of possible geometric constructs. It explores the top constructions suggested by the neural model across multiple iterations, with a decoding batch size of 32. The algorithm alternates between the two components in a looped manner: the neural language model proposes auxiliary constructions to expand the proof state, after which the symbolic deduction engine performs deduction steps to attempt deriving the theorem conclusion. This process repeats for a maximum of 16 iterations, with parallel computation across GPU and CPU workers, until a valid proof is found or the search limit is reached.[2] Efficiency gains arise from heuristics embedded in the integration, which significantly reduce the exponential search space to a manageable scale. By prioritizing promising neural proposals and pruning unnecessary constructions through techniques like dependency difference analysis and traceback algorithms, the system avoids exhaustive exploration typical of purely symbolic methods. This synergy allows AlphaGeometry to achieve high performance on Olympiad-level problems within time constraints, solving 25 out of 30 International Mathematical Olympiad geometry problems.[2][1]

Training

Synthetic Data Generation

AlphaGeometry's synthetic data generation process represents a key innovation in addressing the scarcity of human-annotated proofs for Olympiad-level geometry problems, enabling the system to train entirely without human demonstrations. This automated approach leverages a symbolic deduction engine to create diverse, high-quality training examples by generating random geometric diagrams and deriving proofs from them, thereby simulating the knowledge-building process of human mathematicians at massive scale. By avoiding reliance on curated human data, which is limited for advanced geometry, this method allows for the production of proofs that are often more complex and longer than typical Olympiad problems, fostering the development of robust reasoning capabilities in the AI system.[2][1] The scale of data generation is substantial, with the process yielding over 100 million unique synthetic theorems and proofs after deduplication, covering a wide range of constructions and deductions. This dataset includes approximately 9 million examples featuring auxiliary constructions, which account for about 9% of the total and are crucial for handling complex proof steps that symbolic engines alone cannot deduce. The effort involved sampling nearly 1 billion theorem premises using highly parallelized computing—running 100,000 CPU workers for 72 hours—to initially produce around 500 million examples before filtering for uniqueness. Many of these synthetic proofs exceed 200 steps in length, with the longest reaching 247 steps and incorporating two auxiliary constructions, providing a rich corpus that surpasses the complexity of real-world Olympiad problems.[2][1] The generation process begins with uniformly random sampling of theorem premises using a constructive diagram builder language, which defines a set of construction actions to create consistent geometric diagrams without self-contradictions. A symbolic deduction engine, combining a deductive database for geometric rules (expressed as definite Horn clauses) and algebraic reasoning via Gaussian elimination on coefficient matrices, then computes the deduction closure—a directed acyclic graph of all reachable conclusions from the premises. For each node in this graph, a traceback algorithm identifies the minimal set of premises and dependencies needed to reach the conclusion, forming a synthetic problem and its corresponding proof graph. To enhance diversity and address limitations in pure deduction, the process incorporates auxiliary construction generation by analyzing "dependency differences"—proof terms independent of the conclusion's objects—and integrating them as additional steps, such as introducing new points or lines. Finally, the data is serialized into a textual format (e.g., premises, conclusion, and proof) and deduplicated by reformatting statements into canonical forms, ensuring a high-quality, diverse dataset for training. This synthetic data is subsequently used in pretraining and fine-tuning the neural language model component of AlphaGeometry.[2][1]

Model Training Process

AlphaGeometry's training process consists of two primary phases: pre-training the neural language model on a large corpus of synthetic data to learn general proof generation, followed by fine-tuning to specialize in generating auxiliary geometric constructions essential for complex problems.[2] The pre-training phase utilizes the full dataset of 100 million synthetically generated theorems and proofs, formatted as serialized text strings in the structure "<premises><proof>", enabling the transformer model to predict next tokens in proof sequences conditioned on problem premises and desired conclusions.[2] This phase employs a cosine learning-rate schedule that decays from an initial rate of 0.01 to 0.001 over 10,000,000 optimization steps, with a batch size of 16 per core on a 4 × 4 slice of TPUv3 hardware.[2] In the fine-tuning phase, the model is further trained on a subset of approximately 9 million synthetic proofs that incorporate auxiliary constructions, such as adding points or lines to expand the geometric state and facilitate deductions.[2] The objective here is to maximize the likelihood of generating valid and useful constructions, achieved through supervised next-token prediction focused on geometry-specific tasks like "construct point X so that ABCX is a parallelogram."[2] Fine-tuning proceeds with a fixed learning rate of 0.001 for an additional 1,000,000 steps on the same TPUv3 configuration, refining the model's ability to propose constructions that align with the symbolic deduction engine's formal logic rules.[2] The synthetic data used for both phases, generated via symbolic deduction on randomly sampled geometric premises, provides a diverse set of examples covering proofs up to 247 steps in length without relying on human demonstrations.[2] During training, the quality of the synthetic dataset serves as an implicit evaluation mechanism, with all generated proofs validated for correctness by the symbolic engine prior to model optimization, ensuring alignment between the neural predictions and verifiable geometric reasoning.[2] This internal validation on synthetic proofs allows for iterative improvements before assessing the integrated system on external benchmarks.[2]

Performance

Benchmark Results

AlphaGeometry was evaluated on the IMO-AG-30 benchmark, consisting of 30 geometry problems selected from International Mathematical Olympiad (IMO) competitions between 2000 and 2022.[1] The system successfully solved 25 of these problems, providing full synthetic proofs within the standard IMO time limit of 4.5 hours per problem, while Wu’s method solved only 10 and the strongest baseline (dynamic deduction with algebraic reasoning and human-designed heuristics) solved 18.[2] This performance included the ability to pass the bronze medal threshold in challenging years such as IMO 2000 and IMO 2015 based on its geometry problem-solving, which represent difficult benchmarks for average human contestants.[1][2] In addition to the IMO-AG-30 set, AlphaGeometry was tested on a broader dataset of 231 diverse geometry problems drawn from textbook exercises, regional olympiads, and famous theorems.[2] It achieved a success rate of 98.7% on this set, surpassing baselines like Wu's method (75%) and a combination of dynamic deduction with algebraic reasoning and human-designed heuristics (92.2%).[2] Regarding time efficiency, the system leverages parallel proof search across GPU and CPU workers, enabling it to generate solutions in minutes for many problems, in contrast to the hours typically required by human solvers.[2] Among the five unsolved problems in the IMO-AG-30 benchmark, IMO 2008 Problem 6 stands out as particularly challenging, with an average human score of just 0.28 out of 7.[2] This problem demands advanced geometric concepts such as the Pitot theorem and homothety, which were not fully supported by AlphaGeometry's symbolic deduction engine at the time, highlighting limitations in handling certain specialized constructs.[2]

Comparison to Human Solvers

AlphaGeometry demonstrates performance approaching that of an average International Mathematical Olympiad (IMO) gold medalist on geometry problems, solving 25 out of 30 geometry problems from the International Mathematical Olympiads between 2000 and 2022, a feat that aligns closely with the success rates of top human competitors, as the average human gold medalist solves 25.9 of these problems.[1] In contrast to human solvers, who typically require hours or days for complex proofs, AlphaGeometry generates solutions in minutes, highlighting its efficiency in processing and deducing geometric constructions.[2] One of AlphaGeometry's key strengths lies in its speed and consistency for routine deductions, where it excels at systematically exploring vast search spaces without fatigue, outperforming humans in scenarios requiring exhaustive verification of intermediate steps. However, it shows limitations in generating novel insights or creative leaps that human experts often employ, such as intuitive geometric visualizations that bypass lengthy formal proofs. For instance, mathematicians have noted that while AlphaGeometry's proofs are logically sound and verifiable, they can sometimes lack the elegance or brevity favored by human contestants, resembling more mechanical derivations than inspired solutions. Human experts have provided positive feedback on the quality of AlphaGeometry's outputs, with IMO gold medalist Evan Chen noting that the system's solutions are impressive because they are both verifiable and clean, using classical geometry rules with angles and similar triangles just as students do, while acknowledging areas where deeper geometric intuition could enhance creativity.[1] Similarly, mathematician Timothy Gowers has commented on advancements in AI proof quality in related systems, praising rigorous and complete approaches, though observing that AI sometimes prioritizes symbolic expansion over the concise insights humans develop through experience. These evaluations underscore AlphaGeometry's parity with expert humans in formal reasoning but highlight the irreplaceable role of human creativity in mathematical innovation. In historical context, AlphaGeometry represents a significant advancement over prior AI systems for geometry solving, such as GeoGebra, which relies heavily on interactive human guidance for problem exploration, or the Lean theorem prover, which demands substantial manual input for formalizing proofs. Unlike these tools, AlphaGeometry operates autonomously, integrating neural and symbolic methods to produce end-to-end solutions with minimal human intervention, thereby closing the gap between machine and human performance in Olympiad-level geometry.

Advancements

AlphaGeometry 2

AlphaGeometry 2 is an enhanced version of the original AlphaGeometry system, released by Google DeepMind on July 25, 2024, alongside AlphaProof to enable participation in the International Mathematical Olympiad (IMO).[3] This upgrade builds on the neuro-symbolic approach of its predecessor by incorporating a larger, Gemini-based language model and employing a symbolic engine that is two orders of magnitude faster, allowing for more sophisticated handling of complex geometry proofs.[3] In the 2024 IMO, AlphaGeometry 2 contributed to the combined system's silver-medal standard performance, solving 4 out of 6 problems overall, including the geometry problem (Problem 4), which it proved in just 19 seconds.[3] Prior to the competition, the system demonstrated strong capabilities by solving 83% of historical IMO geometry problems from the past 25 years.[3] DeepMind has made partial code for AlphaGeometry 2 available to the research community through a GitHub repository, focusing on the symbolic engine and examples for reproducing solutions to select Olympiad geometry problems.[8] This release supports further advancements in AI-driven mathematical reasoning.[8]

Key Improvements

AlphaGeometry 2 introduced significant model scaling over the original system by adopting the Gemini architecture, a sparse mixture-of-experts Transformer-based language model trained from scratch on approximately 300 million synthetic theorems— an order of magnitude more data than the 100 million used for the original AlphaGeometry.[4] This scaling included training multiple model sizes up to 3.3 billion parameters on TPUv4 hardware, enabling larger batch sizes and improved inference efficiency through techniques like top-k sampling with temperature 1.0 and k=32.[4] The enhanced model better handles complex geometric concepts, such as movements of objects and equations involving angles, ratios, or distances.[3] In terms of rule expansion, AlphaGeometry 2 expanded the domain-specific language by incorporating new predicates to cover a broader range of geometric problems, including two for "Find x" questions (e.g., acompute for angles and rcompute for ratios), three for linear equations (e.g., distmeq for distance equality), and 11 locus-type predicates for object movements.[4] This automated expansion via synthetic data generation increased language coverage from 66% to 88% on IMO geometry problems from 2000–2024, while discarding explicit rules for angles and distances in favor of integrated algebraic reasoning, resulting in a more efficient yet expansive symbolic framework.[4] Search enhancements in AlphaGeometry 2 featured the novel Shared Knowledge Ensemble of Search Trees (SKEST) algorithm, which runs multiple parallel beam searches with varied configurations (e.g., different language models and tree depths) and shares knowledge through a common facts database filtered for relevance.[4] An enriched neuro-symbolic interface provides the language model with analysis strings detailing deducible facts, improving auxiliary point suggestions and heuristics for longer proofs compared to the original's simpler beam search.[4] The symbolic engine also became two orders of magnitude faster, enabling rapid deduction for complex problems.[3] These improvements culminated in a substantial performance boost, with AlphaGeometry 2 achieving an 84% success rate (42 out of 50) on all IMO geometry problems from 2000–2024, compared to the original's 54% (27 out of 50), and solving 30 out of 30 formalizable IMO problems from 2000–2024—surpassing average gold medalist performance.[4] On historical IMO geometry problems over the past 25 years, it reached 83% success versus the original's 53%.[3]

Impact

Contributions to AI

AlphaGeometry has significantly advanced the neuro-symbolic paradigm in artificial intelligence, particularly for formal reasoning tasks in domains like mathematics. By integrating a neural language model, which excels at pattern recognition and creative hypothesis generation, with a symbolic deduction engine that ensures logical rigor and verifiability, the system demonstrates how hybrid architectures can tackle complex, structured problems that pure neural or symbolic methods struggle with individually. This combination allows AlphaGeometry to propose promising constructions and proofs while maintaining the precision required for mathematical validity, marking a key step toward more interpretable and reliable AI reasoning systems.[2][1] A core contribution lies in its data efficiency, showcasing the feasibility of training high-performance AI models entirely on synthetic data without any human demonstrations. AlphaGeometry was trained on millions of automatically generated geometry problems and proofs, enabling it to achieve expert-level performance on Olympiad-level tasks, such as solving 25 out of 30 International Mathematical Olympiad geometry problems from 2000 to 2019. This approach addresses longstanding challenges in data scarcity for specialized domains, proving that scalable synthetic data generation can bridge the gap between neural networks' data-hungry nature and the need for domain-specific expertise, thereby influencing broader AI training methodologies.[2][1] The system's innovations have had a notable influence on the AI field, and has been cited in 2025 surveys on AI mathematical reasoning as a benchmark for progress in hybrid systems. By effectively bridging the divide between neural creativity—capable of intuitive leaps—and symbolic rigor—essential for error-free deduction—AlphaGeometry highlights pathways to overcome limitations in current large language models, such as hallucinations and lack of formal guarantees, fostering advancements in verifiable AI for scientific and logical applications.[9][3][10]

Broader Applications

AlphaGeometry's neuro-symbolic approach has shown promise for educational applications, particularly in automating proof generation to aid teaching geometry. Its ability to produce human-readable proofs using classical geometric constructions can serve as an interactive tool for students, enabling personalized learning experiences in mathematics by providing step-by-step explanations of complex problems.[10][11] This aligns with its performance on Olympiad-level problems, which match the difficulty of advanced high school curricula, potentially enhancing comprehension through dynamic, AI-assisted tutoring systems.[11] In terms of software integration, AlphaGeometry's open-sourced code facilitates its incorporation into existing tools, such as symbolic deduction engines and geometry-specific software like JGEX for problem representation.[1][2] This enables potential enhancements in systems where geometric reasoning is essential. Furthermore, its hybrid architecture, combining neural language models with rule-based deduction, offers compatibility with formal theorem provers, supporting advancements in systems like Lean and Coq for verifiable proofs in broader mathematical contexts.[2] Research extensions of AlphaGeometry's framework extend beyond pure mathematics, with adaptability to domains involving spatial reasoning, such as physics simulations. In theoretical physics, its capacity to model complex geometric forms could aid in exploring intricate theories, including those in general relativity or quantum mechanics.[10][11] The general applicability of its synthetic data training method to data-scarce fields further positions it for interdisciplinary innovations in simulation-based research.[2] Ethical considerations surrounding AlphaGeometry emphasize the need for transparency, accountability, and bias mitigation in its deployment within mathematical research. Researchers must disclose AI-generated proofs, avoiding authorship attribution to the system while ensuring human oversight to maintain trust and verify outputs against potential hallucinations or errors.[12] Guidelines recommend explaining AI usage in accessible language to non-experts, promoting community engagement to address impacts on mathematical practice.[12] Regarding accessibility, the open-access nature of related publications and the open-sourcing of AlphaGeometry's components enhance equitable availability for global researchers, including those in developing regions, by lowering barriers to advanced tools and fostering inclusive mathematical education.[12][1]
User Avatar
No comments yet.