基于高效启发式辅助构造的奥林匹克几何金 medal 解题方法
人工智能
2025-12-02 v1 计算几何
摘要
欧几里得几何自动定理证明，尤其是针对国际数学奥林匹克 (IMO) 水平问题，仍然是人工智能领域的重大挑战和重要研究焦点。本文提出了一种完全在 CPU 上运行的高效几何定理证明方法，无需依赖神经网络推理。我们的初始研究表明，一种简单的随机策略用于添加辅助点即可在 IMO 上达到银 medal 人类水平。基于此，我们提出了 HAGeo，即在几何推演中添加辅助构造的启发式方法，该方法在 IMO-30 基准测试的 28 个问题中取得金 medal 级别的成绩，显著优于 AlphaGeometry 等竞争性神经网络方法。为更全面地评估我们的方法和现有方法，我们进一步构建了 HAGeo-409，包含 409 个经人类评估难度水平的几何问题的基准。与广泛使用的 IMO-30 相比，我们的基准提出更大挑战，提供更精确的评估，为几何定理证明设定更高的标准。
引用
@article{arxiv.2512.00097,
title = {Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions},
author = {Boyan Duan and Xiao Liang and Shuai Lu and Yaoxiang Wang and Yelong Shen and Kai-Wei Chang and Ying Nian Wu and Mao Yang and Weizhu Chen and Yeyun Gong},
journal= {arXiv preprint arXiv:2512.00097},
year = {2025}
}