Resolución de Problemas de Geometría Olímpica a Nivel Medalla de Oro mediante Construcciones Auxiliares Heurísticas Eficientes
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
November 27, 2025
Autores: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
cs.AI
Resumen
La demostración automática de teoremas en geometría euclidiana, particularmente para problemas de nivel de la Olimpiada Internacional de Matemáticas (IMO), sigue siendo un gran desafío y un importante foco de investigación en Inteligencia Artificial. En este artículo, presentamos un método altamente eficiente para la demostración de teoremas geométricos que se ejecuta completamente en CPU sin depender de inferencia basada en redes neuronales. Nuestro estudio inicial muestra que una simple estrategia aleatoria para añadir puntos auxiliares puede alcanzar un rendimiento humano a nivel de medalla de plata en la IMO. Sobre esta base, proponemos HAGeo, un método heurístico para añadir construcciones auxiliares en la deducción geométrica que resuelve 28 de 30 problemas en el benchmark IMO-30, logrando un rendimiento a nivel de medalla de oro y superando por un margen notable a AlphaGeometry, un enfoque competitivo basado en redes neuronales. Para evaluar nuestro método y los enfoques existentes de manera más integral, construimos además HAGeo-409, un benchmark que consta de 409 problemas de geometría con niveles de dificultad evaluados por humanos. En comparación con el ampliamente utilizado IMO-30, nuestro benchmark plantea mayores desafíos y proporciona una evaluación más precisa, estableciendo un listón más alto para la demostración automática de teoremas geométricos.
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.