Goldmedaillen-Niveau der Olympiade-Geometrie: Lösung mit effizienten heuristischen Hilfskonstruktionen
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
Automatisches Theorembeweisen in der euklidischen Geometrie, insbesondere für Probleme auf dem Niveau der Internationalen Mathematik-Olympiade (IMO), bleibt eine große Herausforderung und ein wichtiger Forschungsschwerpunkt in der künstlichen Intelligenz. In diesem Artikel stellen wir eine hocheffiziente Methode für geometrische Theorembeweise vor, die vollständig auf CPUs läuft und ohne neuronale Netzwerk-Inferenz auskommt. Unsere erste Studie zeigt, dass eine einfache Zufallsstrategie zum Hinzufügen von Hilfspunkten menschliche Leistungen auf Silbermedaillen-Niveau bei der IMO erreichen kann. Darauf aufbauend schlagen wir HAGeo vor, eine heuristikbasierte Methode zum Hinzufügen von Hilfskonstruktionen bei geometrischen Deduktionen, die 28 von 30 Problemen im IMO-30-Benchmark löst und damit Leistungen auf Goldmedaillen-Niveau erreicht. Diese Methode übertrifft AlphaGeometry, einen konkurrenzfähigen, auf neuronalen Netzen basierenden Ansatz, um einen bemerkenswerten Vorsprung. Um unsere Methode und bestehende Ansätze umfassender zu bewerten, erstellen wir weiterhin HAGeo-409, einen Benchmark, der aus 409 Geometrieproblemen mit von Menschen bewerteten Schwierigkeitsgraden besteht. Im Vergleich zum weit verbreiteten IMO-30 stellt unser Benchmark größere Herausforderungen dar und ermöglicht eine präzisere Bewertung, wodurch er eine höhere Messlatte für das geometrische Theorembeweisen setzt.
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.