通过高效启发式辅助构造实现金牌级别的奥数几何解题 / Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
1️⃣ 一句话总结
这篇论文提出了一种名为HAGeo的高效几何定理证明方法，它不依赖神经网络，仅通过启发式策略添加辅助点线，就在国际数学奥林匹克级别的几何题上达到了金牌选手的解题水平，并超越了之前的神经网络方法。
🤖 系统
Abstract - Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
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.