Source-linked AI summary
Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, Thang Luong
TL;DR
AlphaGeometry2 addresses limitations in AI systems’ geometric reasoning and in the original AlphaGeometry language. It expands the language and proof-search system, achieving an 84% solve rate on 2000–2024 IMO geometry problems versus 54% for AG1, while remaining limited on several problem types.
Problem
AI systems, including AG1, struggle with geometric objects and interactions, while AG1’s language covers only 66% of 2000–2024 IMO geometry problems and mainly supports constructive problems.
Method
AG2 combines an expanded domain language, a faster symbolic engine, a Gemini-based language model, and Shared Knowledge Ensemble of Search Trees for proof search.
Results
84% solve rate on 2000–2024 IMO geometry problems, compared with 54% for AG1, surpassing an average IMO gold medalist.
Takeaways & Limitations
AG2 substantially advances automated Olympiad geometry solving and demonstrates progress toward systems that solve geometry problems from natural-language input.
Takeaways & Limitations
AG2’s domain language still excludes variable numbers of points, non-linear equations, and inequalities, and some advanced techniques are not implemented.
Abstract
from arXiv · showhide
We present AlphaGeometry2 (AG2), a significantly improved version of AlphaGeometry introduced in (Trinh et al., 2024), which has now surpassed an average gold medalist in solving Olympiad geometry problems. To achieve this, we first extend the original AlphaGeometry language to tackle problems involving movements of objects, and problems containing linear equations of angles, ratios, and distances. This, together with support for non-constructive problems, has markedly improved the coverage rate of the AlphaGeometry language on International Math Olympiads (IMO) 2000-2024 geometry problems from 66% to 88%. The search process of AG2 has also been greatly improved through the use of Gemini architecture for better language modeling, and a novel knowledge-sharing mechanism that enables effective communication between search trees. Together with further enhancements to the symbolic engine and synthetic data generation, we have significantly boosted the overall solving rate of AG to 84% on all geometry problems over the last 25 years, compared to 54% previously. AG2 was also part of the system that achieved the silver-medal standard at IMO 2024 https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/. Finally, we report progress towards using AG2 as a part of a fully automated system that reliably solves geometry problems from natural language input. Code: https://github.com/google-deepmind/alphageometry2.
1. Introduction
AG2 builds on AlphaGeometry’s neuro-symbolic approach to address broader Olympiad geometry challenges. It combines expanded language coverage, stronger search and modeling, and improved automation, achieving substantially higher solving performance.
- Motivation and background: AG1 combines a neural language model that suggests insights with a symbolic engine that formally derives geometric properties.The system was trained on 100M synthetically generated examples and solved IMO-level geometry problems.
- AG2 contributions: AG2 expands the domain language, strengthens the symbolic engine, improves language modeling, and introduces the SKEST search algorithm.SKEST uses multiple search trees with knowledge sharing to explore auxiliary construction strategies more broadly and efficiently.
- AG2 contributions: AG2 also advances fully automated geometry solving by translating natural-language problems into the AlphaGeometry language and generating diagrams automatically.
- Results: 84% solving rate was achieved on all 2000-2024 IMO geometry problems, compared with 54% for AG1, surpassing an average IMO gold medalist.
2. More general domain language
AG2 generalizes AlphaGeometry’s domain language beyond constructive problems and basic predicates. The extensions raise coverage on 2000-2024 IMO geometry problems while leaving several problem classes outside scope.
- Limitations of AG1: 66% was the coverage of AG1’s language on 2000-2024 IMO geometry problems, limited by its inability to express linear equations, movements, and some computational questions.
- Language extensions: AG2 adds predicates for computing angles and ratios, expressing linear equations of angles, distances, and log-distances, representing movements, and checking topological conditions.The language includes acompute, rcompute, distmeq, distseq, angeq, locus syntax, and explicit non-degeneracy predicates.
- Non-constructive problems: AG2 permits points defined by at least three predicates, enabling non-constructive problems whose diagram construction is non-trivial.
- Coverage: 88% coverage was reached on all 2000-2024 IMO geometry problems, up from 66%; the remaining 12% includes 3D geometry, inequalities, non-linear equations, and arbitrarily many points.
3. Stronger and faster symbolic engine
AG2 improves DDAR, AlphaGeometry’s symbolic deduction engine, in logical coverage and computational efficiency. These changes support more extensive data generation and proof search.
- Symbolic engine role: DDAR computes the deduction closure by iteratively applying fixed rules until no additional facts can be derived.It supports both language-model training-data generation and test-time proof search, where speed enables broader search.
- DDAR improvements: AG2 adds double-point handling, a faster algorithm, and a faster implementation to DDAR.
- Double points: Double-point reformulation lets the system construct an auxiliary intersection X′, prove it lies on the second line, and conclude X = X′.This converts a difficult direct incidence proof into a potentially easier equivalent argument.
- Algorithmic acceleration: DDAR2 accelerates searches for similar triangles and cyclic quadrilaterals by hashing symbolic geometric shapes and repeated angle or segment values.The arithmetic-reasoning submodule reduces linear expressions involving angles, distances, and log-distances to normal forms.
- Implementation: The C++ implementation of core Gaussian-elimination computation is over 300 times faster than DDAR1.The benchmark used 25 IMO problems that DDAR could not solve and repeated each test 50 times.
4. Better synthetic training data
AG2 retains synthetic data generation from random diagrams while broadening theorem types, scaling diagram and proof complexity, and improving minimal-problem extraction. These changes produce more diverse training data for the upgraded system.
- Synthetic-data pipeline: AG2 continues generating synthetic examples by sampling random diagrams, deducing facts, and tracing each fact back to premises, auxiliary points, and proof steps.
- Scale and distribution: AG2 explores random diagrams at twice the size, generates theorems up to 2x more complex, and produces proofs with up to 10x more steps than AG1.The data distribution is also rebalanced across question types and problems with or without auxiliary points.
- Theorem types: AG2 generates locus theorems involving moving points, lines, and circles, supported by movement dependencies recorded through P(A).P(A) denotes the points controlling the movement of A.
- Data-generation efficiency: A greedy procedure replaces AG1’s exhaustive exponential search for the smallest provable point subset.The implementation iterates through points in reverse topological order and removes a point when provability remains.
5. Novel search algorithm
AG2 replaces AG1’s single beam-search approach with parallel, differently configured search trees that share problem-relevant facts. SKEST combines multiple tree strategies and language models while coordinating asynchronous proof-search components.
- Shared Knowledge Ensemble of Search Trees: SKEST runs several differently configured beam searches in parallel and lets them help one another through shared knowledge.The method is designed as a novel alternative to AG1’s simple beam search.
- Search-tree configurations: Different language models are used for each search-tree configuration to improve robustness.The ensemble varies both search behavior and model choice.
- Knowledge sharing: Each failed tree node records symbolic-engine facts in a shared database after filtering out auxiliary-point-specific facts.The retained facts are relevant to the original problem and can support other searches.
- Search-tree configurations: AG2 includes classic search, multi-auxiliary-point search, and other tree strategies within the ensemble.The multi-point tree can generate as many auxiliary points as it wants at a node because the language model is trained on full proofs.
- System design: LM and DDAR workers operate asynchronously, while explored nodes and deduction attempts are coordinated through a database.The implementation uses TPUv4 replicas and asynchronous workers for language-model inference and symbolic deduction.
6. Better language model
AG2 introduces a new Gemini-based language model and trains it on large synthetic theorem data using several training configurations. Its evaluation emphasizes IMO solve rate because perplexity is only a proxy for downstream proof success.
- Language-model design: AG2’s new language model is based on the Gemini architecture and uses a simplified one-phase unsupervised training setup.The model is a sparse mixture-of-expert Transformer trained on AG2 data.
- Training configurations: AG2 considers training from scratch with a custom domain tokenizer, fine-tuning math-specialized Gemini models, and multimodal training with diagram inputs.These are presented as alternative training configurations.
- Training and evaluation data: The training data include around 300 million synthetic theorems and three evaluation sets: eval, eval_aux, and imo_eval.The evaluation sets cover synthetic problems with different auxiliary-point conditions and previously solved IMO problems.
- Evaluation metric: Perplexity is treated as a proxy because inference uses only predicted auxiliary points and a problem can have multiple valid proofs.The main downstream metric is solve rate on IMO problems, using beam search followed by DDAR.
- Scaling behavior: Perplexity loss decreases as Gemini model size increases on the train, eval, and IMO evaluation sets.Figure 5 compares models by parameter count, including million- and billion-parameter scales.
- Inference setup: Inference uses top-k sampling with temperature t=1.0 and k=32, while greedy decoding solves only two of 26 problems requiring auxiliary constructions.The paper states that high temperature and multiple samples are essential for these IMO problems.
- Neuro-symbolic interface: AG2 feeds DDAR-derived fact sets S1, S2, and S3 to the language model through an analysis string before auxiliary constructions are proposed.The sets represent deducible facts under original premises, deducible facts assuming the goal, and numerically correct diagram facts.
7. Results
AG2 solves 42 of 50 translated IMO geometry problems, surpassing the average gold-medalist benchmark. Results also show early solving progress, while remaining failures reflect unsupported problem types and missing geometric machinery.
- Main benchmark: 42 out of 50 IMO-AG-50 geometry problems are solved by AG2, surpassing an average gold medallist for the first time.IMO-AG-50 translates 45 geometry problems from IMO 2000–2024 into 50 AlphaGeometry problems.
- Training efficiency: AG2 solves 27 out of 50 problems after 250 training steps, corresponding to around 200 million seen tokens.This result uses one language model coupled with DDAR through classical tree search.
- Inference ablations: The optimal single-tree inference configuration uses beam size 128, beam depth 4, and 32 samples.More samples or a larger beam search do not solve additional problems in this ablation.
- Limitations: AG2’s remaining unsolved IMO problems include six unformalizable cases involving inequalities, variable numbers of points, or other unsupported language constructs.Two additional unsolved problems require techniques such as inversion, projective geometry, or radical axis that are not implemented in DDAR.
- Comparison context: The paper notes that an earlier gold-medalist claim was made on only a subset of IMO problems.This qualification accompanies the comparison with prior work.
8. Conclusions and Future Work
AG2 substantially improves AlphaGeometry’s geometry-solving performance through broader language coverage, stronger modeling and search, and symbolic-engine enhancements, while leaving important scope gaps.
- 84% solve rate on 2000-2024 IMO geometry problems, compared with 54% for AlphaGeometry’s predecessor.
- AG2 combines a larger and more diverse training dataset, a more powerful language model, a faster symbolic engine, an expanded domain language, and a new proof-search algorithm.
- AG2 studies tokenizer choice, training language, pretrained mathematical models, proof generation, and fully automated natural-language geometry solving.
- The domain language still excludes variable numbers of points, nonlinear equations, and inequalities, and AG2 has not solved every IMO and IMOSL problem.
Code availability
The authors provide the Python implementation of the DDAR2 symbolic engine and examples of proven IMO problems, while withholding infrastructure-dependent training and search code.
- Python code for the DDAR2 symbolic engine will be shared with multiple examples of proven IMO problems.
- The repository includes implementation materials for reproducing symbolic-engine examples.
- Training Gemini models and running the full multi-model tree search require internal Google infrastructure, so that code is not provided.
Data availability
The repository makes a curated set of IMO geometry problems available in AlphaGeometry’s language, together with diagrams and solutions.
- 27 IMO problems are translated into the AlphaGeometry language.
- The shared problem set includes diagrams and solutions.
- The examples are located in the repository’s test.py file.
B. Fine-tuning of math specialized language models on AG data
The study examines whether tokenizer choice, training language, and mathematical pretraining affect AlphaGeometry models, including fine-tuning pretrained models on AlphaGeometry data.
- Tokenizers: The authors compare models using custom small-vocabulary tokenizers with models using Gemini’s large tokenizer.
- Tokenizers: AlphaGeometry’s domain language uses point names, geometric predicates, numbers, predicate-reference tokens, and reserved control tokens.
- Tokenizers: Performance stays the same across different tokenizers on the 2000-2024 IMO geometry problems.
- Domain-specific language: The authors translate AlphaGeometry2 training data into natural language and compare it with training on the original domain-specific language.
- Fine-tuning: A 3.3B-parameter Gemini model pretrained on public mathematics datasets is fine-tuned unsupervised on AlphaGeometry data.
C. Multi-modal
AG2’s multimodal extension trains models on both problem text and diagram images, but image input alone does not improve downstream solve rates. The paper also illustrates AG2’s auxiliary constructions and evaluates its robustness beyond IMO problems.
- Multi-modal: Diagram-aware models take problem text and the corresponding diagram image as input.This extends the Gemini-based AG2 system toward multimodal reasoning.
- Multi-modal: Multimodal models alone do not improve solve rates on downstream IMO problems.When combined with other models through knowledge sharing, their different auxiliary-point proposals boost overall performance.
- Additional evaluation: 20 out of 30 selected IMO shortlist geometry problems are solved by the full AG2 system.The IMOSL-AG-30 set contains formalized problems nominated by experts but not selected for the IMO.
- Proof verification: The proof verifier classifies generated steps using checks including grammar, theorem names, references, point validity, numerical stability, and logical verification.A step is marked verified only when all checks pass without detected errors.
- Natural-language automation: AG2 is being developed into a system that maps natural-language geometry problems to full proofs and automatically constructed diagrams.The system solved IMO 2025 geometry problem P2 from natural language in 20 seconds.