Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions

Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, and Yeyun Gong, in ACL, 2026.

Code

Download the full text

Abstract

Automated theorem proving in Euclidean geometry, particularly for International Mathematical Olympiad (IMO) level problems, remains a major challenge and an important research focus in Artificial Intelligence. In this paper, we present a highly efficient method for geometry theorem proving that runs entirely on CPUs without relying on neural network-based inference. Our initial study shows that a simple random strategy for adding auxiliary points can achieve silver-medal level human performance on IMO. Building on this, we propose HAGeo, a Heuristic-based method for adding Auxiliary constructions in Geometric deduction that solves 28 of 30 problems on the IMO-30 benchmark, achieving gold-medal level performance and surpassing AlphaGeometry, a competitive neural network-based approach, by a notable margin. To evaluate our method and existing approaches more comprehensively, we further construct HAGeo-409, a benchmark consisting of 409 geometry problems with human-assessed difficulty levels. Compared with the widely used IMO-30, our benchmark poses greater challenges and provides a more precise evaluation, setting a higher bar for geometry theorem proving.

Source Code

Bib Entry

@inproceedings{duan2026gold,
  title = {Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions},
  author = {Duan, Boyan and Liang, Xiao and Lu, Shuai and Wang, Yaoxiang and Shen, Yelong and Chang, Kai-Wei and Wu, Ying Nian and Yang, Mao and Chen, Weizhu and Gong, Yeyun},
  booktitle = {ACL},
  year = {2026}
}

Related Publications

OpenThoughts: Data Recipes for Reasoning Models, ICLR, 2026
OpenVLThinker: Complex Vision-Language Reasoning via Iterative SFT-RL Cycles, NeurIPS, 2025
When To Solve, When To Verify: Compute-Optimal Problem Solving and Generative Verification for LLM Reasoning, COLM 2025, 2025
MathVerse: Does Your Multi-modal LLM Truly See the Diagrams in Visual Math Problems?, ECCV, 2024
MathVista: Evaluating Mathematical Reasoning of Foundation Models in Visual Contexts, ICLR, 2024