Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2

Yuri ChervonyiTrieu H. TrinhMiroslav OlskXiaomeng YangHoang H. NguyenMarcelo MenegaliJunehyuk JungJunsu KimVikas VermaQuoc V. Le

article2025JMLR73 citations

Presents AlphaGeometry2, a neuro-symbolic system that surpasses average International Mathematical Olympiad gold medalists by solving 84% of historical Olympiad geometry problems using an expanded formal language, Gemini-powered search, and a faster symbolic reasoning engine.

Listen

Advancing mathematical reasoning remains a core challenge in artificial intelligence, as standard large language models consistently struggle with geometric concepts and rigorous proofs. While early neuro-symbolic systems showed promise, they suffered from restricted formal languages, inefficient symbolic engines, and limited search capabilities. The article introduces and evaluates AlphaGeometry2, a neuro-symbolic system designed to address these deficiencies and solve advanced Euclidean geometry problems at the International Mathematical Olympiad (IMO) standard.

The authors combined an expanded domain-specific language, an optimized symbolic deduction engine written in C++, a specialized Gemini-based language model trained on over 300 million synthetic theorems, and a novel multi-tree search algorithm called Shared Knowledge Ensemble of Search Trees (SKEST). The evaluation was conducted across 45 geometry problems from the 2000–2024 International Mathematical Olympiads, translated into 50 formal benchmarks, as well as an additional set of 30 challenging shortlist problems. The system was benchmarked against previous automated solvers and the historical performance of human medalists.

The findings show that AlphaGeometry2 resolved 84% (42 out of 50) of all formalizable IMO geometry problems spanning 2000 to 2024, significantly outperforming the original AlphaGeometry's 54% solving rate and surpassing the average gold-medalist threshold of 40.9 problems. Key drivers of this improvement included language extensions that increased problem coverage from 66% to 88%, an optimized deduction engine operating over 300 times faster than its predecessor, and the new search architecture, which alone increased the solved count from 38 to 42 problems through collaborative fact sharing across search trees. On the shortlist evaluation set, the system solved 20 out of 30 problems, demonstrating strong generalization.

These results establish that combining neural models for intuitive auxiliary constructions with high-speed symbolic engines for deductive verification provides a dependable path to complex mathematical reasoning without hallucinations. This framework improves computational efficiency and performance while reducing verification risks in automated reasoning. Organizations and researchers developing reasoning systems should prioritize hybrid neuro-symbolic architectures and explore ensembling diverse search strategies over relying solely on pure language model generation.

Future work should focus on expanding the formal language to cover inequalities, non-linear equations, and variable quantities of points, as well as incorporating reinforcement learning to further close the performance gap on the hardest problems. Users should note that current system constraints prevent it from solving problems involving three-dimensional geometry or algebraic inequalities, though confidence remains very high for well-formalized Euclidean geometry tasks.

Brown University Georgia Institute of Technology Google Seoul National University University of Cambridge automated systems communication engine AlphaGeometry2 Olympiad geometry IMO geometry problems

arXiv: 2502.03544 google-deepmind/alphageometry2

Paper: Let's Verify Step by Step, Hunter Lightman et al. (2023). Establishes the foundational paradigm of process-level step-by-step verification to eliminate hallucinations during complex mathematical deduction.
Paper: Magnushammer: A Transformer-Based Approach to Premise Selection, Maciej Mikula et al. (2024). Provides fundamental techniques for neural premise selection and formal lemma retrieval in automated theorem proving environments.
Paper: Training Verifiers to Solve Math Word Problems, Karl Cobbe et al. (2021). Introduces the core concept of utilizing independent verifiers to score and guide candidate mathematical reasoning steps generated by language models.
Paper: Measuring Mathematical Problem Solving With the MATH Dataset, Dan Hendrycks et al. (2021). Introduces the standard benchmark dataset and problem-solving methodology for evaluating language models on competition-level high school mathematics.

Paper: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks, Po-Nien Kung et al. (2026). Expands automated Olympiad theorem proving from domain-specific Euclidean geometry solvers to an agentic framework operating on full formal Lean environments across competition-level mathematics.
Paper: AI Co-Mathematician: Accelerating Mathematicians with Agentic AI, Daniel Zheng et al. (2026). Builds on automated theorem-solving advances by integrating frontier AI reasoning models into an interactive workbench for collaborative research mathematics.

Cover for Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2

Abstract

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 silver-medal standard at IMO 2024 https://dpmd.ai/imo-silver. 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.

Topics

automated systems communication engine geometry knowledge-sharing language model linear equations natural languages search process synthetic data

Keywords

AlphaGeometry2 Olympiad geometry IMO geometry problems geometric reasoning mathematical reasoning algebraic reasoning Euclidean geometry locus-type statements Gemini architecture

1. Introduction
2. More general domain language
3. Stronger and faster symbolic engine
3.1 Handling double points
3.2 Faster algorithm
3.3 Faster implementation
4. Better synthetic training data
5. Novel search algorithm
6. Better language model
6.1 Training setup
6.2 Inference setup
7. Results
8. Conclusions and Future Work
Code availability
Data availability
Acknowledgments
References
Appendix A. Related work
Appendix B. Fine-tuning of math specialized language models on AG data
Appendix C. Multi-modal
Appendix D. Featured AlphaGeometry2 solutions
Appendix E. Additional evaluation on the hardest IMO shortlist problems
Appendix F. Towards generating full proofs with a language model
Appendix G. Automated problem formalization and diagram generation
Appendix H. Inequality rules
H.1 Definitions
H.2 How to write some of the common geometric inequality statements using ω
H.3 Trivial rules
H.4 Rules for relating ω and η
H.5 Basic rules using P in polygon
H.6 Basic rules using ' ∈ O ' and ' / ∈ O '
H.7 Acute and obtuse angles
H.8 Some inequalities
H.9 General ω and η deduction rules

Knowls

Knowl 1 — Benchmark Performance of AlphaGeometry2 on IMO Geometry Problems

data/table

The downstream problem-solving capability of AlphaGeometry2 (AG2) was evaluated on International Mathematical Olympiad (IMO) geometry problems from 2000 to 2024. The evaluation was performed on two benchmarks: IMO-AG-50, consisting of all 45 IMO geometry problems from 2000–2024 translated into 50 formal AlphaGeometry problems, and IMO-AG-30, which is the subset of 30 problems expressible in the domain language of AlphaGeometry 1 (AG1).

System Description	IMO-AG-50 Solved	IMO-AG-30 Solved
OpenAI o1	0	0
Gemini thinking	0	0
AG1 DDAR	14	14
AG2 DDAR	16	15
TongGeometry DD	-	18
Average Bronze Medalist	27.1	19.3
Wu with AG1 DDAR	-	21
Average Silver Medalist	33.9	22.9
AG1 (Trinh et al., 2024)	27	25
Average Gold Medalist	40.9	25.9
Wu + AG1	-	27
TongGeometry w/o value	-	28
AG2 (single search tree)	38	28
TongGeometry full setting	-	30
AG2 full setting (multiple search trees)	42	30

In its full multi-search-tree configuration, AlphaGeometry2 solves 42 out of 50 problems (84%) on IMO-AG-50, surpassing the average gold medalist score threshold of 40.9 problems. On IMO-AG-30, AG2 solves all 30 problems (100%). Six problems in the 2000–2024 set remained unformalizable due to non-linear equations, inequalities, or variable numbers of points, while two formalizable problems (IMO 2018 P6 and IMO 2023 P6) were attempted but not solved within search limits.

Knowl 2 — Shared Knowledge Ensemble of Search Trees (SKEST)
model/method
Shared Knowledge Ensemble of Search Trees (SKEST) is a proof search algorithm for neuro-symbolic geometry theorem proving that coordinates multiple parallel beam searches across diverse language model configurations and search topologies.

Each node in a search tree represents an auxiliary construction proposed by a language model, followed by an execution of the Deductive Database Arithmetic Reasoning (DDAR) symbolic engine. If a node fails to establish the proof goal, DDAR extracts facts proved about the original problem premises (filtering out facts that depend on node-specific auxiliary points) and writes them to a globally shared workspace database.

SKEST executes diverse search tree configurations simultaneously:
1. Classic search tree: Proposes one auxiliary point at each node.
2. Multi-auxiliary search tree: Generates multiple auxiliary points in a single step, increasing effective search depth.
3. Uniform auxiliary type tree: Prompts the language model with prefix tokens specifying distinct geometric predicates (e.g., x00 a : cong, x00 a : coll, x00 a : cyclic, x00 a : perp) to force exploration across construction types.
4. Deep-narrow tree: Configured with beam size 64 and depth 10.
5. Shallow-wide tree: Configured with beam size 512 and depth 4.
Search trees query shared TPUv4 language model servers asynchronously. Language model worker processes populate explored nodes in a database, while a decoupled pool of DDAR worker processes retrieves nodes to perform deduction closures, dynamically reallocating compute resources when individual problems are solved.
Knowl 3 — Domain-Specific Language Extensions in AlphaGeometry2
model/method
AlphaGeometry2 expands the original AlphaGeometry domain-specific language from 9 basic geometric predicates to cover computational queries, linear equations of geometric magnitudes, locus theorems, and non-degeneracy/equivalence conditions, increasing coverage of IMO 2000–2024 geometry problems from 66% to 88%.

The predicate additions comprise:
1. Computational predicates: acompute a b c d (determine directed angle between lines $AB$ and $CD$ ) and rcompute a b c d (determine length ratio $AB/CD$ ).
2. Linear equation predicates:
  - Log-distance relations: $\text{distmeq } a_1 b_1 \dots a_n b_n\ t_1 \dots t_n\ y \iff \sum_{i=1}^n t_i \log(A_i B_i) + y = 0$
  - Linear distance combinations: $\text{distseq } a_1 b_1 \dots a_n b_n\ t_1 \dots t_n \iff \sum_{i=1}^n t_i A_i B_i = 0$
  - Angle linear combinations: $\text{angeq } a_1 b_1 \dots a_n b_n\ t_1 \dots t_n\ y \iff \sum_{i=1}^n t_i d(A_i B_i) + y = 0$ where $d(AB)$ denotes the angle between undirected line $AB$ and the horizontal axis.
3. Locus wildcard syntax: Uses a wildcard token * to express locus statements across 11 geometric motion cases (e.g., ? coll a b * : X asserts that line $AB$ passes through a fixed point, ? cyclic a b c * : X asserts that the circumcircle of $ABC$ passes through a fixed point).
4. Diagram verification and equivalence predicates: sameclock a b c d e f (clock orientation check), noverlap a b ( $A \neq B$ ), lessthan a b c d ( $AB < CD$ ), overlap a b (coincident points $A=B$ ), and cyclic_with_center a1 ... an x (points $a_1 = \dots = a_x$ form the circumcenter of points $a_{x+1}, \dots, a_n$ ).
5. Non-constructive definitions: Points can be specified simultaneously by $\ge 3$ intersecting geometric conditions rather than sequential pairs of intersecting curves.
Knowl 4 — DDAR2 Symbolic Engine and Double-Point Reformulation
model/method
Deductive Database Arithmetic Reasoning 2 (DDAR2) optimizes deduction closure computation and introduces point equivalence reasoning to resolve problems requiring auxiliary point identification.

Double-Point Handling: In geometric proofs where a target point $X$ must be shown to lie on a curve $\omega$ , direct deduction of $X \in \omega$ may be inaccessible. DDAR2 enables proof by coincidence reformulation:
1. The language model constructs an auxiliary point $X'$ defined as the intersection of line $a$ and curve $\omega$ .
2. DDAR2 deduces that $X'$ lies on line $b$ .
3. From $X, X' \in a \cap b$ , the engine concludes $X = X'$ via line intersection uniqueness.
4. From $X = X'$ and $X' \in \omega$ , the engine deduces the goal $X \in \omega$ .
Algorithmic Optimizations: In DDAR1, worst-case candidate matching for similar triangles required $O(N^8)$ operations. DDAR2 hashes the invariant shape profile across all point triples and detects pairs of similar triangles in hash match steps. For cyclic quadrilaterals, DDAR2 hashes the tuple $(A, B, \angle AXB)$ in symbolic normal forms produced by the Arithmetic Reasoning (AR) submodule. Essential deduction rules are hard-coded, reducing sub-engine AR queries to at most $O(N^3)$ .

C++ Engine: Implementing the core Gaussian elimination subroutines in C++ exported to Python via pybind11 achieves a $>300\times$ speedup over DDAR1, reducing execution time across 25 non-DDAR-solvable IMO benchmark problems from $1179.57 \pm 8.06$ seconds down to $3.45 \pm 0.05$ seconds on a 64-core AMD EPYC 7B13 CPU.
Knowl 5 — Neuro-Symbolic Analysis String Interface
equation
In AlphaGeometry2, the prompt fed to the language model before requesting auxiliary point constructions is augmented with structured deduction and numerical validation states. For a given problem, three nested sets of geometric facts are computed:

$S_1 \subset S_2 \subset S_3$

where:
- $S_1$ is the set of all facts deduced by the DDAR symbolic engine from the initial premises.
- $S_2$ is the set of all facts deduced by DDAR given the initial premises assuming the goal predicate is true.
- $S_3$ is the set of all facts that hold numerically to floating-point tolerance on the concrete geometric diagram.
The language model receives a linearized string concatenation:

$\langle\text{problem\_statement}\rangle\ \text{serialized}(S_1)\ \text{serialized}(S_2 \setminus S_1)\ \text{serialized}(S_3 \setminus S_2)$

This explicit division provides the neural proposer with the current baseline deduction state, the backwards consequences of the goal, and empirically valid numerical observations.
Knowl 6 — Greedy Reverse-Topological Point Pruning
algorithm
To extract minimal problem statements and minimal proofs from random synthetic diagrams without exponential subset search over points, AlphaGeometry2 applies a greedy pruning algorithm operating in reverse-topological order of point construction dependencies.
Input: points as the set of geometric points in a sampled diagram, check_provable as a monotonic provability predicate function
Output: pruned as a minimal subset of points closed under dependencies that proves the goal
pruned = set(points)
for p in reverse_topological_order(points):
if check_provable(pruned \setminus {p}):
pruned = pruned \setminus {p}
return pruned
Evaluating candidate point deletions in reverse-topological order ensures that the remaining subset is always closed under construction dependencies, preserving the monotonicity condition ( $A \subseteq B \implies \text{check\_provable}(A) \implies \text{check\_provable}(B)$ ) and finding a minimal set in $O(|V|)$ predicate checks rather than exponential search.
Knowl 7 — Automated Diagram Generation for Non-Constructive Geometry Problems
algorithm
Non-constructive geometry problems specify points simultaneously through arbitrary algebraic and topological constraints rather than constructive ruler-and-compass steps. AlphaGeometry2 synthesizes coordinate diagrams for non-constructive problems through a three-stage numerical optimization method.

Let $\bar{x} \in \mathbb{R}^{2n}$ represent the 2D Cartesian coordinates of all $n$ points. Exact constraints $c \in C_{\text{exact}}$ are defined as nonlinear residual functions $f_c(\bar{x}) = 0$ , inequality topological constraints $c \in C_{<}$ as $g_c(\bar{x}) < 0$ , and non-degeneracy constraints $c \in C_{=0}$ as $h_c(\bar{x}) \neq 0$ .
Input: Problem specification with exact constraints C_exact, topological constraints C_ineq and C_neq, and distinct point pairs
Output: Point coordinate vector x_bar in R^(2n) satisfying all constraints to numerical tolerance
Initialize x_bar across 10 random seeds using circle-line locus sampling
for each initial configuration:
    Minimize L(x_bar) using Adam optimizer for a fixed number of steps:
        L(x_bar) = sum_{c in C_exact} (f_c(x_bar))^2
                   + sum_{c in C_ineq} softplus(g_c(x_bar))
                   + sum_{c in C_neq} softplus(min(h_c(x_bar), -h_c(x_bar)))
                   + lambda_1 * ||x_bar||_2
                   + sum_{distinct (A, B)} lambda_2 / (||A - B||^2 + epsilon)
    if L(x_bar) < threshold and all topological constraints are satisfied:
        Refine x_bar to zero exact residual using the Gauss-Newton-Levenberg method
        if residual norm <= tolerance:
            return x_bar
Restart with new randomized initial configuration
Applied to 44 formalized IMO geometry benchmark problems, this procedure successfully solved valid coordinate diagrams for 43 problems sequentially within 1 hour.
Knowl 8 — Synthetic Generation of Locus Theorems via Movement Dependency Tracking
model/method
To train language models to solve locus problems involving moving geometric objects, AlphaGeometry2 defines a movement dependency function $P(A)$ over points in a random diagram:
- $P(A)$ denotes the minimal set of independent base points that determine the position and movement of point $A$ .
- For a deterministic construct (e.g., $d = \text{midpoint}(a, c)$ with $a = \text{midpoint}(b, c)$ ), $P(d) = \{b, c\}$ .
- For an unconstrained point on a locus (e.g., $a = \text{on\_line}(b, c)$ ), $P(a) = \{a, b, c\}$ .
When the DDAR symbolic engine deduces an invariant relation on a generated diagram, the data generator computes set differences between controlling dependency sets: $X = P(\text{moving\_target}) \setminus P(\text{fixed\_reference})$ If $X \neq \emptyset$ , the relation is converted into a synthetic locus theorem of the form: "When $X$ moves, the moving target satisfies the fixed locus property." 17 distinct predicate deduction patterns are mapped into 11 locus categories, with auxiliary constructions defined as the dependency closure of $X$ .
Knowl 9 — Benchmark Performance on the Hardest IMO Shortlist Problems (IMOSL-AG-30)
empirical result
The generalization of AlphaGeometry2 was evaluated on IMOSL-AG-30, a benchmark of 30 formalized problems selected from the most difficult geometry problems located at the end of IMO Shortlists from 2002 to 2022 that were never chosen for the official competition.

The full multi-tree SKEST AlphaGeometry2 system solved 20 out of 30 problems (66.7%). Four problems (2003-g5, 2011-g6, 2016-g7, 2018-g7) were solved directly by the DDAR2 symbolic deduction closure without requiring auxiliary constructions, while 16 problems required neural auxiliary point proposals discovered via beam search.
Knowl 10 — Invariance of AlphaGeometry Performance to Tokenizer and Formal Language Representations
empirical result
Controlled training ablation experiments on AlphaGeometry2 demonstrate that downstream theorem proving performance on IMO geometry is invariant to tokenizer architecture and language modality:
1. Tokenizer Choice: Training models of identical architecture using a custom domain-specific word-level tokenizer (vocabulary size of a few thousand tokens) versus the standard subword Gemini tokenizer (vocabulary size 300k) resulted in equivalent solve rates on the IMO 2000–2024 geometry benchmark.
2. Natural vs. Formal Language: Translating the entire synthetic training corpus of 300M geometry theorems from the formal AlphaGeometry predicate language into natural English statements produced models that achieved the same downstream IMO solve rates.
3. Pre-training Convergence: A 3.3B parameter Gemini model pre-trained on mathematical text and fine-tuned on AG data converged to the same validation loss and IMO solve rate as a 3.3B model trained on AG data from scratch after $2 \times 10^{11}$ seen tokens, but generated distinct auxiliary point proposals that yielded performance gains when combined in SKEST search ensembles.
4. Multimodal Image Input: Providing diagram images to Gemini 1.5 alongside text problem statements yielded no standalone solve rate gain, attributed to dense visual clutter in IMO diagrams and foundation models' limited precision in atomic visual geometry reasoning.

Coverage note — Omitted the extensive catalogue of explicit inequality deduction rules from Appendix H, step-by-step error taxonomy frequencies for tool-free LM proof generation from Appendix F, and specific step-by-step geometric proof walkthroughs of individual Olympiad problems (IMO 2013 P3, IMO 2014 P3, IMO 2024 P4, IMOSL 2009 G7) from Appendix D, as they represent reference listings, exploratory analyses, or illustrative case studies rather than core system methods and aggregate benchmark findings.

References

1.Hyunsik Chae, Seungwoo Yoon, Chloe Yewon Chun, Gyehun Go, Yongin Cho, Gyeongmin Lee, and Ernest K. Ryu. Decomposing complex visual comprehension into atomic visual skills for vision language models. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. URL https://openreview.net/forum?id=nFU4xCyoe0.
2.Xinyun Chen, Maxwell Lin, Nathanael Sch¨arli, and Denny Zhou. Teaching large language models to self-debug. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview.net/forum?id=KuPixIqPiq.
3.S-C Chou, X-S Gao, and J-Z Zhang. Automated production of traditional proofs for constructive geometry theorems. In [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pages 48–56. IEEE, 1993.
4.Shang-Ching Chou. Proving and discovering geometry theorems using Wu’s method. The University of Texas at Austin, 1985.
5.Shang-Ching Chou, Xiaoshan Gao, and Jing-Zhong Zhang. Machine proofs in geometry: Automated production of readable proofs for geometry theorems, volume 6. World Scientific, 1994.
6.Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. Automated generation of readable proofs with geometric invariants: I. multiple and shortest proof generation. Journal of Automated Reasoning, 17(3):325–347, 1996.
7.Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3):219–246, 2000.
8.Bj¨orn Deiseroth, Manuel Brack, Patrick Schramowski, Kristian Kersting, and Samuel Weinbach. T-free: Tokenizer-free generative llms via sparse representations for memoryefficient embeddings, 2024. URL https://arxiv.org/abs/2406.19223.
9.Gemini Team. Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context. arXiv preprint arXiv:2403.05530, 2024.
10.Yushi Hu, Weijia Shi, Xingyu Fu, Dan Roth, Mari Ostendorf, Luke Zettlemoyer, Noah A. Smith, and Ranjay Krishna. Visual sketchpad: Sketching as a visual chain of thought for multimodal language models. In NeurIPS 2024 Workshop on Behavioral Machine Learning, 2024. URL https://openreview.net/forum?id=prJ4b0GMSB.
11.Jie Huang, Xinyun Chen, Swaroop Mishra, Huaixiu Steven Zheng, Adams Wei Yu, Xinying Song, and Denny Zhou. Large language models cannot self-correct reasoning yet. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview.net/forum?id=IkmD3fKBPQ.
12.Wenzel Jakob, Jason Rhinelander, and Dean Moldovan. pybind11 – seamless operability between c++11 and python, 2017. https://github.com/pybind/pybind11.
13.Piyush Jha, Prithwish Jana, Pranavkrishna Suresh, Arnav Arora, and Vijay Ganesh. Rlsf: Reinforcement learning via symbolic feedback, 2024. URL https://arxiv.org/abs/2405.16661.
14.Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023.
15.Deepak Kapur. Geometry theorem proving using hilbert’s nullstellensatz. In Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, pages 202–208, 1986a.
16.Deepak Kapur. Using gr¨obner bases to reason about geometry problems. Journal of Symbolic Computation, 2(4):399–408, 1986b.
17.Ryan Krueger, Jesse Michael Han, and Daniel Selsam. Automatically building diagrams for olympiad geometry problems. In CADE, pages 577–588, 2021.
18.Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang, and Xiaoxing Ma. Proving olympiad inequalities by synergizing LLMs and symbolic reasoning. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=FiyS0ecSm0.
19.Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview.net/forum?id=v8L0pN6EOi.
20.Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self-feedback. In Thirty-seventh Conference on Neural Information Processing Systems, 2023. URL https://openreview.net/forum?id=S37hOerQLB.
21.Spyridon Mouselinos, Henryk Michalewski, and Mateusz Malinowski. Beyond lines and circles: Unveiling the geometric reasoning gap in large language models. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Findings of the Association for Computational Linguistics: EMNLP 2024, pages 6192–6222, Miami, Florida, USA, November 2024. Association for Computational Linguistics. doi: 10.18653/v1/2024. findings-emnlp.360. URL https://aclanthology.org/2024.findings-emnlp.360/.
22.Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing euclidean geometry. In Forty-first International Conference on Machine Learning, 2024. URL https://openreview.net/forum?id=bylZbZOsGA.
23.Shuai Peng, Di Fu, Yijun Liang, Liangcai Gao, and Zhi Tang. GeoDRL: A self-learning framework for geometry problem solving using reinforcement learning in deductive reasoning. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki, editors, Findings of the Association for Computational Linguistics: ACL 2023, pages 13468–13480, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10.18653/v1/2023. findings-acl.850. URL https://aclanthology.org/2023.findings-acl.850/.
24.Auguste Poiroux, Gail Weiss, Viktor Kunˇcak, and Antoine Bosselut. Improving autoformalization using type checking. arXiv preprint arXiv:2406.07222, 2024.
25.Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020. URL https://arxiv.org/abs/2009.03393.
26.Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik R Narasimhan, and Shunyu Yao. Reflexion: language agents with verbal reinforcement learning. In Thirty-seventh Conference on Neural Information Processing Systems, 2023. URL https://openreview.net/forum?id=vAElhFcKW6.
27.Aaditya K. Singh and DJ Strouse. Tokenization counts: the impact of tokenization on arithmetic in frontier llms, 2024. URL https://arxiv.org/abs/2402.14903.
28.Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, and Matthias Bethge. Wu’s method can boost symbolic ai to rival silver medalists and alphageometry to outperform gold medalists at imo geometry, 2024. URL https://arxiv.org/abs/2404.06405.
29.Kaya Stechly, Karthik Valmeekam, and Subbarao Kambhampati. On the self-verification limitations of large language models on reasoning and planning tasks. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=4O0v4s3IzY.
30.Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pages 3–20. Springer, 2020.
31.Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476, 2024.
32.Barbara Tversky and Masaki Suwa. Thinking with sketches. In Tools for Innovation, pages 75–84. Oxford University Press, November 2009.
33.Xiaofeng Wang, Yiming Wang, Wenhong Zhu, and Rui Wang. Do large language models truly understand geometric structures? In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=FjQOXenaXK.
34.Chenrui Wei, Mengzhou Sun, and Wei Wang. Proving olympiad algebraic inequalities without human demonstrations. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. URL https://openreview.net/forum?id=8kFctyli9H.
35.Wen-ts¨un Wu. On the decision problem and the mechanization of theorem-proving in elementary geometry. In Selected Works Of Wen-Tsun Wu, pages 117–138. World Scientific, 2008.
36.Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022. URL https://arxiv.org/abs/2205.12615.
37.Yang Yan, Yu Lu, Renjun Xu, and Zhenzhong Lan. Do phd-level llms truly grasp elementary addition? probing rule learning vs. memorization in large language models, 2025. URL https://arxiv.org/abs/2504.05262.
38.Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu, and SongChun Zhu. Proposing and solving olympiad geometry with guided tree search. arXiv preprint arXiv:2412.10673, 2024.
39.Lunjun Zhang, Arian Hosseini, Hritik Bansal, Mehran Kazemi, Aviral Kumar, and Rishabh Agarwal. Generative verifiers: Reward modeling as next-token prediction. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=Ccwp4tFEtE.

Citation

MLA

Chervonyi, Y., et al. “Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2”. Journal of Machine Learning Research, vol. 26, no. 241, 2025, pp. 1–9, https://www.jmlr.org/papers/v26/25-1654.html.

APA

Chervonyi, Y., Trinh, T. H., Olšák, M., Yang, X., Nguyen, H. H., Menegali, M., Jung, J., Kim, J., Verma, V., Le, Q. V., & Luong, T. (2025). Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. Journal of Machine Learning Research, 26(241), 1–39. https://www.jmlr.org/papers/v26/25-1654.html

Chicago

Chervonyi, Y., T. H. Trinh, M. Olšák, et al. 2025. “Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2”. Journal of Machine Learning Research 26 (241): 1–39. https://www.jmlr.org/papers/v26/25-1654.html.

Harvard

Chervonyi, Y. et al. (2025) “Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2”, Journal of Machine Learning Research, 26(241), pp. 1–39. Available at: https://www.jmlr.org/papers/v26/25-1654.html.

Vancouver

1. Chervonyi Y, Trinh TH, Olšák M, et al (2025) Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. Journal of Machine Learning Research 26:1–39

BibTeX

@article{JMLR:v26:25-1654,
  author  = {Yuri Chervonyi and Trieu H. Trinh and Miroslav Ol{\v{s}}{{\'a}}k and Xiaomeng Yang and Hoang H. Nguyen and Marcelo Menegali and Junehyuk Jung and Junsu Kim and Vikas Verma and Quoc V. Le and Thang Luong},
  title   = {Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2},
  journal = {Journal of Machine Learning Research},
  year    = {2025},
  volume  = {26},
  number  = {241},
  pages   = {1--39},
  url     = {http://jmlr.org/papers/v26/25-1654.html}
}

Metadata:DOI registry

Source Code

This paper has an official code repository available. Click below to access the source code.

View Repository

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF

License: https://creativecommons.org/licenses/by/4.0/

Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2

Abstract

Topics

Keywords

Table of Contents

Knowls

Knowl 1 — Benchmark Performance of AlphaGeometry2 on IMO Geometry Problems

Knowl 2 — Shared Knowledge Ensemble of Search Trees (SKEST)

Knowl 3 — Domain-Specific Language Extensions in AlphaGeometry2

Knowl 4 — DDAR2 Symbolic Engine and Double-Point Reformulation

Knowl 5 — Neuro-Symbolic Analysis String Interface

Knowl 6 — Greedy Reverse-Topological Point Pruning

Knowl 7 — Automated Diagram Generation for Non-Constructive Geometry Problems

Knowl 8 — Synthetic Generation of Locus Theorems via Movement Dependency Tracking

Knowl 9 — Benchmark Performance on the Hardest IMO Shortlist Problems (IMOSL-AG-30)

Knowl 10 — Invariance of AlphaGeometry Performance to Tokenizer and Formal Language Representations

References

Citation

BibTeX

Source Code

Access the Paper