금메달급 올림피아드 기하 문제 풀이: 효율적인 발견적 보조 구성법

초록

유클리드 기하학에서의 자동 정리 증명, 특히 국제수학올림피아드(IMO) 수준의 문제에 대한 증명은 인공지능 분야의 주요 과제이자 중요한 연구 초점으로 남아 있습니다. 본 논문에서는 신경망 기반 추론에 의존하지 않고 오로지 CPU만으로 실행되는 매우 효율적인 기하학 정리 증명 방법을 제시합니다. 우리의 초기 연구에 따르면, 단순한 무작위 보조점 추가 전략으로도 IMO에서 은메달 수준의 인간 성과를 달성할 수 있음을 보여줍니다. 이를 바탕으로 우리는 HAGeo를 제안합니다. 이는 기하학적 추론에서 보조 구도를 추가하기 위한 휴리스틱 기반 방법으로, IMO-30 벤치마크의 30개 문제 중 28개를 해결하여 금메달 수준의 성능을 달성하고 신경망 기반 접근법인 AlphaGeometry를 상당한 차이로 능가합니다. 우리의 방법과 기존 접근법을 보다 포괄적으로 평가하기 위해, 우리는 인간이 평가한 난이도를 가진 409개의 기하학 문제로 구성된 벤치마크인 HAGeo-409를 추가로 구축했습니다. 널리 사용되는 IMO-30과 비교할 때, 우리의 벤치마크는 더 큰 도전 과제를 제시하고 더 정밀한 평가를 제공함으로써 기하학 정리 증명 분야에 더 높은 기준을 설정합니다.

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.

금메달급 올림피아드 기하 문제 풀이: 효율적인 발견적 보조 구성법

Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions

초록

Support