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, Yeyun Gong
2025-12-03
Summary
This paper focuses on creating a computer program that can automatically prove geometry theorems, specifically those at the very difficult level seen in the International Mathematical Olympiad (IMO). It's about making AI better at solving geometry problems.
What's the problem?
Automated theorem proving in geometry is really hard, even for computers. Existing methods often rely on complex neural networks which require a lot of computing power. The challenge is to create a program that can solve these complex geometry problems efficiently and accurately, without needing those resource-intensive neural networks. Current benchmarks, like the IMO-30, aren't challenging enough to really push the limits of these programs.
What's the solution?
The researchers developed a method called HAGeo, which stands for Heuristic-based method for adding Auxiliary constructions in Geometric deduction. Essentially, the program tries to solve problems by strategically adding extra lines, points, or shapes to the diagram – these are called 'auxiliary constructions'. HAGeo uses smart rules (heuristics) to decide *where* to add these constructions. They also created a new, much larger and harder benchmark called HAGeo-409 with 409 geometry problems to better test the program's abilities. HAGeo outperformed a previous state-of-the-art AI called AlphaGeometry on the IMO-30 benchmark.
Why it matters?
This work is important because it shows that powerful AI for geometry doesn't necessarily require huge neural networks. HAGeo’s success demonstrates that clever algorithms and strategic problem-solving can achieve excellent results, potentially making this technology more accessible and efficient. The new HAGeo-409 benchmark provides a more rigorous test for future AI geometry solvers, pushing the field forward and helping to create even smarter programs.
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.