より挑戦的なIMO問題の解決に向けた分離推論と証明

要旨

形式言語における自動定理証明（ATP）は、AIにとって基礎的な課題である。大規模言語モデル（LLM）が著しい進歩を遂げている一方で、その強力な非形式的推論能力と弱い形式的証明性能との間には依然として大きな隔たりが存在する。最近の研究によると、非形式的な正答率は80％を超えるのに対し、PutnamBenchなどのベンチマークにおける形式的な成功率は8％未満にとどまっている。この隔たりが持続する理由として、現在の最先端の証明器は推論と証明を密接に結合しており、深い推論を犠牲にして浅い戦略ベースの手法を優先するような訓練パラダイムが採用されていることが挙げられる。この根本的な隔たりを埋めるため、我々は高水準の推論と低水準の証明生成を分離する新しいフレームワークを提案する。このアプローチでは、多様で戦略的なサブゴール補題を生成するための強力な汎用推論モデル（Reasoner）と、それらを厳密に検証するための効率的な証明モデル（Prover）という2つの専門化されたモデルを活用する。このモジュール設計により、モデルの持つ完全な推論能力を解放し、エンドツーエンド訓練の落とし穴を回避することが可能となる。我々はこの手法を、2000年以降の国際数学オリンピック（IMO）問題の難問セットに対して評価した。この問題セットでは、これまでオープンソースの証明器が成功を報告した例はない。我々の分離型フレームワークは、これらの問題のうち5つを成功裏に解決し、極めて困難な数学的課題に対する自動推論に向けた重要な一歩を示した。今後の研究を促進するため、我々は幅広いIMO問題に対して生成および検証された補題の完全なデータセットを公開し、https://tencent-imo.github.io/ で利用可能とした。

English

Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remains between their powerful informal reasoning capabilities and their weak formal proving performance. Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench. We argue this gap persists because current state-of-the-art provers, by tightly coupling reasoning and proving, are trained with paradigms that inadvertently punish deep reasoning in favor of shallow, tactic-based strategies. To bridge this fundamental gap, we propose a novel framework that decouples high-level reasoning from low-level proof generation. Our approach utilizes two distinct, specialized models: a powerful, general-purpose Reasoner to generate diverse, strategic subgoal lemmas, and an efficient Prover to rigorously verify them. This modular design liberates the model's full reasoning potential and bypasses the pitfalls of end-to-end training. We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success. Our decoupled framework successfully solves 5 of these problems, demonstrating a significant step towards automated reasoning on exceptionally difficult mathematical challenges. To foster future research, we release our full dataset of generated and verified lemmas for a wide range of IMO problems, available at https://tencent-imo.github.io/ .

より挑戦的なIMO問題の解決に向けた分離推論と証明

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

要旨

Support