Resolução de Geometria Olímpica de Nível Medalha de Ouro com Construções Auxiliares Heurísticas Eficientes
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
November 27, 2025
Autores: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
cs.AI
Resumo
A prova automática de teoremas em geometria euclidiana, particularmente para problemas de nível da Olimpíada Internacional de Matemática (IMO), continua a ser um grande desafio e um foco de pesquisa importante na Inteligência Artificial. Neste artigo, apresentamos um método altamente eficiente para prova de teoremas geométricos que é executado inteiramente em CPUs, sem depender de inferência baseada em redes neurais. Nosso estudo inicial mostra que uma estratégia aleatória simples para adicionar pontos auxiliares pode atingir o desempenho humano de nível medalha de prata na IMO. Com base nisso, propomos o HAGeo, um método heurístico para adicionar construções auxiliares na dedução geométrica que resolve 28 dos 30 problemas do benchmark IMO-30, alcançando desempenho de nível medalha de ouro e superando a AlphaGeometry, uma abordagem competitiva baseada em redes neurais, por uma margem notável. Para avaliar nosso método e as abordagens existentes de forma mais abrangente, construímos ainda o HAGeo-409, um benchmark composto por 409 problemas de geometria com níveis de dificuldade avaliados por humanos. Em comparação com o amplamente utilizado IMO-30, nosso benchmark apresenta desafios maiores e fornece uma avaliação mais precisa, estabelecendo um padrão mais alto para a prova automática de teoremas geométricos.
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.