Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909933419626496 |
|---|---|
| author | Duan, Boyan Liang, Xiao Lu, Shuai Wang, Yaoxiang Shen, Yelong Chang, Kai-Wei Wu, Ying Nian Yang, Mao Chen, Weizhu Gong, Yeyun |
| author_facet | Duan, Boyan Liang, Xiao Lu, Shuai Wang, Yaoxiang Shen, Yelong Chang, Kai-Wei Wu, Ying Nian Yang, Mao Chen, Weizhu Gong, Yeyun |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_00097 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions Duan, Boyan Liang, Xiao Lu, Shuai Wang, Yaoxiang Shen, Yelong Chang, Kai-Wei Wu, Ying Nian Yang, Mao Chen, Weizhu Gong, Yeyun Artificial Intelligence Computational Geometry 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. |
| title | Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions |
| topic | Artificial Intelligence Computational Geometry |
| url | https://arxiv.org/abs/2512.00097 |