不依赖神经网络，用启发式方法解决国际奥数几何题
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
- 基于启发式规则添加辅助点，无需神经网络
- 在IMO-30上解出28道题，达金牌水平
- 自建HAGeo-409新基准，难度更高更精准
欧氏几何自动定理证明，尤其是国际数学奥林匹克（IMO）级别的题目，仍是人工智能领域的重要挑战。本文提出一种完全运行在CPU上的高效几何定理证明方法，不依赖神经网络推理。初步研究发现，仅用随机策略添加辅助点即可达到人类银牌水平。在此基础上，我们提出HAGeo——一种基于启发式的几何推导中辅助构造方法，在IMO-30基准上成功解决28道题，实现金牌水平表现，并显著超越以AlphaGeometry为代表的神经网络方法。为更全面评估现有方法，我们进一步构建了HAGeo-409基准，包含409道具有人类标注难度等级的几何题，相比广泛使用的IMO-30更具挑战性，为几何定理证明设立了更高标准。
原文摘要 · Abstract (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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。