Goedel-Prover-V2：自己修正と段階的データ合成による効率的な自動定理証明の新展開
3つの要点
✔️ Goedel-Prover-V2は小規模でも高性能な自動定理証明を実現する新しいオープンソースモデル
✔️ Scaffolded Data Synthesisや自己修正、モデル平均化を組み合わせた学習手法を提案
✔️ MiniF2FやPutnamBenchで従来の大規模モデルを超える性能を達成し、効率性を実証
Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
written by Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin
(Submitted on 5 Aug 2025)
Comments: 24 pages, 10 figures, 4 tables
Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI)
概要
本論文は、自動定理証明（Automated Theorem Proving, ATP）の新しい基盤モデル「Goedel-Prover-V2」を提案しています。
従来の研究では、極めて大規模なモデル（数百B規模のパラメータ）や膨大な推論計算を必要とし、オープンソースモデルの性能は制約されてきました。
そこで著者らは、効率的かつ高性能な定理証明を実現するために、新しい学習手法とデータ生成戦略を導入。
具体的には、難易度を段階的に調整した合成問題を生成する「Scaffolded Data Synthesis」、Leanコンパイラからのフィードバックを活用する「Verifier-guided Self-Correction」、さらに出力の多様性を維持する「Model Averaging」を組み込みました。
その結果、わずか32B規模のモデルであっても、従来の671Bモデルを凌駕する性能を達成。
MiniF2Fベンチマークでは88.1%（自己修正込みで90.4%）、PutnamBenchでは86問を解くことに成功し、オープンソースモデルの新たな最高水準を樹立しています。
これにより、膨大な計算資源に依存せずとも、効率的に高度な数学的推論を行えることが実証されました。
提案手法
提案手法の核心は、長いchain-of-thoughtを用いた定理証明に「自己修正」と「段階的データ合成」を融合させた点です。
まず、Verifier-guided Self-Correctionは、モデルが生成した証明をLeanコンパイラにかけ、そのエラーメッセージを解析し、修正版を生成させる仕組みです。
これにより、人間が証明を推敲するように、失敗から学びながら証明を完成させる能力を獲得します。
次に、Scaffolded Data Synthesisでは、難問に失敗した際に得られる未解決の部分課題や、より簡単な変種問題を合成し、モデルに効率的な学習信号を与えます。
これにより、難易度の階層構造を利用した効果的なトレーニングが可能となりました。
さらに、Model Averagingを導入し、異なる学習段階で得られたモデルを重み平均することで、多様性の欠落を防ぎつつ性能を向上させています。
最終的には、SFT（教師あり微調整）、RL（強化学習）、モデル平均を組み合わせた一貫した学習パイプラインが設計され、高効率で堅牢な定理証明モデルが実現しました。
実験
評価は主にMiniF2FとPutnamBenchで行われ、提案モデルの性能が従来法を大きく上回ることが確認されました。
MiniF2F（高校数学～国際数学オリンピック水準）において、Goedel-Prover-V2-32Bはpass@32で88.1%、自己修正モードでは90.4%に到達し、DeepSeek-Prover-V2-671Bを超える成果を挙げました。
さらにPutnamBench（大学レベルの数学競技問題）では、従来の47問から大幅に改善し、86問を解くことに成功しています。
また、8Bモデルでさえ、MiniF2Fにおいて671Bモデルを上回る性能を発揮し、効率性を強く示しました。
加えて、自己修正の効果は定量的に示されており、pass@32で平均2ポイントの向上を達成。
スケーリング分析では、少数のサンプル生成で高精度を実現できる「サンプル効率の高さ」も確認されています。
これらの実験結果は、提案手法が小規模モデルでも最先端の定理証明能力を可能にすることを示し、今後の数理AI研究の基盤としての有用性を裏付けています。
この記事に関するカテゴリー
