Решение олимпиадных задач по геометрии высшего уровня с эффективными эвристическими вспомогательными построениями
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
November 27, 2025
Авторы: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
cs.AI
Аннотация
Автоматическое доказательство теорем в евклидовой геометрии, особенно для задач уровня Международной математической олимпиады (ММО), остается серьезной проблемой и важным направлением исследований в области искусственного интеллекта. В данной статье представлен высокоэффективный метод доказательства геометрических теорем, который полностью выполняется на центральных процессорах без использования выводов на основе нейронных сетей. Наше первоначальное исследование показывает, что простая случайная стратегия добавления вспомогательных точек позволяет достичь уровня человеческой производительности, соответствующего серебряной медали на ММО. Основываясь на этом, мы предлагаем HAGeo — эвристический метод добавления вспомогательных построений в геометрическом выводе, который решает 28 из 30 задач на тестовом наборе IMO-30, достигая уровня производительности золотой медали и значительно превосходя 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.