Risoluzione di Problemi di Geometria Olimpica a Livello Medaglia d'Oro con Costruzioni Ausiliarie Euristiche Efficaci
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
November 27, 2025
Autori: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
cs.AI
Abstract
La dimostrazione automatizzata di teoremi di geometria euclidea, in particolare per problemi di livello Olimpiadi Internazionali della Matematica (IMO), rimane una sfida significativa e un importante focus di ricerca nell'ambito dell'Intelligenza Artificiale. In questo articolo, presentiamo un metodo altamente efficiente per la dimostrazione di teoremi geometrici che viene eseguito interamente su CPU senza fare affidamento su inferenze basate su reti neurali. Il nostro studio iniziale dimostra che una semplice strategia casuale per l'aggiunta di punti ausiliari può raggiungere prestazioni pari a quelle umane di livello medaglia d'argento alle IMO. Sviluppando questo concetto, proponiamo HAGeo, un metodo euristico per l'aggiunta di costruzioni ausiliarie nella deduzione geometrica, che risolve 28 dei 30 problemi del benchmark IMO-30, raggiungendo prestazioni di livello medaglia d'oro e superando AlphaGeometry, un competitivo approccio basato su reti neurali, con un margine considerevole. Per valutare il nostro metodo e gli approcci esistenti in modo più completo, abbiamo inoltre costruito HAGeo-409, un benchmark composto da 409 problemi di geometria con livelli di difficoltà valutati da esseri umani. Rispetto al diffusamente utilizzato IMO-30, il nostro benchmark presenta sfide maggiori e fornisce una valutazione più precisa, stabilendo un livello più elevato per la dimostrazione automatizzata di teoremi geometrici.
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.