Resumen: La demostración automatizada de teoremas en geometría euclidiana, particularmente para problemas de nivel de la Olimpiada Internacional de Matemáticas (OMI), sigue siendo un desafío importante y un importante foco de investigación en Inteligencia Artificial. En este artículo, presentamos un método altamente eficiente para demostrar teoremas de geometría que se ejecuta completamente en CPU sin depender de la inferencia basada en redes neuronales. Nuestro estudio inicial muestra que una estrategia aleatoria simple para agregar puntos auxiliares puede lograr un desempeño humano de nivel de medalla de plata en la OMI. Sobre esta base, proponemos HAGEo, un método basado en heurística para agregar construcciones auxiliares en deducción geométrica que resuelve 28 de 30 problemas en el punto de referencia IMO-30, logrando un rendimiento de nivel de medalla de oro y superando a AlphaGeometry, un enfoque competitivo basado en redes neuronales, por un margen notable. Para evaluar nuestro método y los enfoques existentes de manera más integral, construimos HAGEo-409, un punto de referencia 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 punto de referencia plantea mayores desafíos y proporciona una evaluación más precisa, estableciendo un listón más alto para la demostración de teoremas de geometría.
Publicado originalmente en export.arxiv.org el 1 de diciembre de 2025.
Ver fuente original
