金メダル級オリンピック幾何学：効率的な発見的補助構図を用いた解法

要旨

ユークリッド幾何学における自動定理証明、特に国際数学オリンピック（IMO）レベルの問題に対するそれは、人工知能における主要な課題かつ重要な研究焦点であり続けている。本論文では、ニューラルネットワークベースの推論に依存せず、CPU上で完全に動作する、極めて効率的な幾何学定理証明法を提案する。我々の予備調査では、補助点を追加する単純なランダム戦略が、IMOにおいて銀メダルレベルに相当する人間の性能を達成し得ることが示されている。これを発展させ、我々はHAGeo（Heuristic-based method for adding Auxiliary constructions in Geometric deduction）を提案する。この手法は、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