Résolution de géométrie olympique de niveau médaille d'or avec constructions auxiliaires heuristiques efficaces
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
November 27, 2025
papers.authors: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
cs.AI
papers.abstract
La démonstration automatisée de théorèmes en géométrie euclidienne, particulièrement pour les problèmes de niveau Olympiade Internationale de Mathématiques (OIM), reste un défi majeur et un axe de recherche important en intelligence artificielle. Dans cet article, nous présentons une méthode hautement efficace pour la démonstration de théorèmes géométriques qui s'exécute entièrement sur des processeurs sans recours à l'inférence par réseaux neuronaux. Notre étude préliminaire montre qu'une simple stratégie aléatoire d'ajout de points auxiliaires peut atteindre des performances humaines de niveau médaille d'argent aux OIM. Sur cette base, nous proposons HAGeo, une méthode heuristique pour l'ajout de constructions auxiliaires dans la déduction géométrique, qui résout 28 des 30 problèmes du benchmark IMO-30, atteignant des performances de niveau médaille d'or et surpassant notablement AlphaGeometry, une approche compétitive basée sur les réseaux neuronaux. Pour évaluer plus complètement notre méthode et les approches existantes, nous construisons ensuite HAGeo-409, un benchmark comprenant 409 problèmes de géométrie avec des niveaux de difficulté évalués par des humains. Comparé au largement utilisé IMO-30, notre benchmark présente des défis plus importants et fournit une évaluation plus précise, établissant une barre plus haute pour la démonstration de théorèmes géométriques.
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.