Goudenmedaille-niveau Olympische Meetkunde Oplossen met Efficiënte Heuristische Hulpconstructies
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
November 27, 2025
Auteurs: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
cs.AI
Samenvatting
Geautomatiseerd stellingenbewijzen in de Euclidische meetkunde, met name voor problemen op het niveau van de Internationale Wiskunde Olympiade (IMO), blijft een grote uitdaging en een belangrijk onderzoeksfocus binnen de Kunstmatige Intelligentie. In dit artikel presenteren we een zeer efficiënte methode voor het bewijzen van meetkundestellingen die volledig op CPU's draait zonder gebruik te maken van op neurale netwerken gebaseerde inferentie. Onze eerste studie toont aan dat een eenvoudige willekeurige strategie voor het toevoegen van hulppunten een menselijke prestatie op zilverenmedaille-niveau van de IMO kan bereiken. Voortbouwend hierop stellen we HAGeo voor, een heuristiek-gebaseerde methode voor het toevoegen van hulpconstructies in meetkundige deductie, die 28 van de 30 problemen op de IMO-30 benchmark oplost. Hiermee bereikt het een prestatie op goudenmedaille-niveau en overtreft het AlphaGeometry, een competitieve op neurale netwerken gebaseerde aanpak, met een aanzienlijke marge. Om onze methode en bestaande benaderingen uitgebreider te evalueren, construeren we verder HAGeo-409, een benchmark bestaande uit 409 meetkundeproblemen met door mensen beoordeelde moeilijkheidsgraden. In vergelijking met de veelgebruikte IMO-30 biedt onze benchmark grotere uitdagingen en voorziet deze in een nauwkeurigere evaluatie, waarmee een hogere lat wordt gezet voor geautomatiseerd stellingenbewijzen in de meetkunde.
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.