金牌级奥数几何解题：高效启发式辅助构造法

摘要

欧几里得几何的自动定理证明，特别是针对国际数学奥林匹克竞赛（IMO）级别的问题，仍然是人工智能领域的重大挑战和重要研究方向。本文提出一种完全在CPU上运行、不依赖神经网络推理的高效几何定理证明方法。我们的初步研究表明，简单的随机添加辅助点策略即可在IMO问题上达到银牌级别的人类表现。基于此，我们提出HAGeo——一种基于启发式规则的几何演绎辅助构造方法，该方法在IMO-30基准测试中成功解决30道题中的28道，达到金牌级别表现，并以显著优势超越基于神经网络的竞争方法AlphaGeometry。为更全面评估本方法及现有技术，我们进一步构建了HAGeo-409基准数据集，包含409道经人工评估难度等级的几何问题。与广泛使用的IMO-30相比，该基准提出了更大挑战，能提供更精确的评估，为几何定理证明领域设立了更高标准。

English

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.

金牌级奥数几何解题：高效启发式辅助构造法

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

摘要

Support