技術的概要：OProver：エージェント型形式定理証明のための統合フレームワーク

問題定義

形式定理証明、特に Lean 4 エコシステム内での最近の進展は、大規模な証明生成と検証器を考慮したトレーニングを活用し、MiniF2F や PutnamBench などのベンチマークにおける性能向上を実現してきた。しかし、重要な限界が依然として存在する：エージェント型証明能力（検索、コンパイラフィードバック、反復的修復）は、通常、固定された証明器に適用される推論時のヒューリスティックとして扱われ、トレーニングプロセスに統合された学習された方策として扱われていない。

これにより、トレーニングと推論の不一致が生じる。主に完成した成功証明に基づいてトレーニングされたモデルは、コンパイラフィードバックや検索された文脈に、最適化されたことのない分布であるデプロイ時でのみ遭遇する。さらに、既存の形式コーパスは、最終成果物（ステートメントと検証済み証明）に焦点を当てており、証明の修復方法を学習するために不可欠な、失敗した試行、検索された文脈、コンパイラ診断を含む多回対話履歴を省略している。その結果、実際の証明修復を駆動する教師信号は、モデルトレーニングにおいてほとんど活用されていない。

手法

本論文は、検索、コンパイラフィードバック、反復的修復を、共進化トレーニングパイプラインを通じて証明器の方策に直接統合するOProverという統合フレームワークを提示する。

1. OProver フレームワーク

OProver は、定理証明を有界な多回反復の洗練ループとして扱う。各ラウンド $t$ において、方策 $\pi$ はコンパクトな状態 $X_t = (s, R_t, p_{t-1}, f_{t-1})$ に条件付けられる。ここで：

• $s$：対象の定理ステートメント。
• $R_t$：メモリ $M$ から検索されたトップ-$k$ のコンパイラ検証済み証明。
• $p_{t-1}$：直前の証明試行。
• $f_{t-1}$：Lean 4 検証器からの生テキスト形式のコンパイラフィードバック（診断）。

方策は修正された試行 $p_t$ を生成する。検証が失敗した場合、生フィードバックは次のラウンドのために方策へ戻される。重要なのは、方策が最も最近の試行とフィードバックのみに条件付けられ、局所的な修正信号を保持しつつ状態をコンパクトに保つ点である。

2. OProofs：統合トレーニングコーパス

このフレームワークをサポートするため、著者らはエージェント型証明のために特別に設計された大規模コーパスOProofsを構築する。最終証明のみを保持する先行データセットとは異なり、OProofs は以下のシリアライズされた軌跡を記録する：

• 検索された文脈。
• 失敗した試行。
• 生コンパイラフィードバック。
• 後続の修復。

OProofs は、公開の Lean リソース、大規模な証明合成（自動形式化＋検証）、および OProver 自身のエージェント型証明からのトレースの 3 つのソースから構築される。これには、177 万個の一意な Lean ステートメントと 686 万個のコンパイラ検証済み証明、および 107 万個のエージェント型軌跡がペアリングされている。

3. 共進化トレーニングパイプライン

トレーニングプロセスは、証明器とコーパスが共進化する反復ループ（アルゴリズム 1）に従う：

1. 継続的事前トレーニング（CPT）：ベースモデルを Lean コード、数学、長文脈推論データの混合でトレーニングし、OProver-Baseを作成する。
2. 反復的ポストトレーニング：
   • エージェント型ロールアウト：現在の方策が定理プール上で多回反復証明を実行し、現在のメモリ $M_k$ から検索し、Lean コンパイラで検証する。
   • データ収集：新たに検証された証明はコーパスに追加され、検索メモリにインデックス付けされる。失敗した試行と成功した修復は、ラウンドレベルの例 $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$ に分解される。
   • 教師あり微調整（SFT）：収集された修復例を使用してモデルを更新する。
   • 強化学習（RL）：グループシーケンス方策最適化（GSPO）を、検証成功と形式の正しさに基づく報酬信号を用いて、より困難な未解決ケースに適用する。
   • 再循環：更新されたコーパスとメモリが次の反復にフィードされ、方策が自身の改善された証明から学習することを可能にする。

主要な貢献

1. エージェント型証明のための統合フレームワーク：OProver は、検索、フィードバック、反復的修復を単一の学習された方策に統合し、これらの信号を外部ヒューリスティックではなく中核戦略の一部として使用するようにモデルをトレーニングすることで、トレーニングと推論の不一致を排除する。
2. OProofs コーパス：失敗した試行や生コンパイラフィードバックを含む多回対話履歴を明示的に保持する大規模コーパス（177 万ステートメント、686 万証明）の構築。これにより、形式データセットで以前は利用不可能だった教師信号が提供される。
3. 共進化パイプライン：証明器が生成した新しいデータ（検証済み証明と修復軌跡）が即座にトレーニングコーパスと検索メモリに組み込まれ、自己改善ループを創出するトレーニング手法。
4. 最先端の性能：OProver は、オープンウェイトの全体証明器の中でトップクラスの成果を達成し、エージェント型洗練戦略がはるかに大規模なモデルを上回る性能を発揮しうることを実証する。

実験結果

OProver は、MiniF2F、MathOlympiadBench、ProofNet、ProverBench、PutnamBench の 5 つの Lean 4 ベンチマークで評価された。

• 性能：OProver-32Bモデルは、3 つのベンチマーク（MiniF2F：93.3%、ProverBench：58.2%、PutnamBench：11.3%）で最良の Pass@32 スコアを達成し、残りの 2 つ（MathOlympiad：22.8%、ProofNet：33.2%）で 2 位を記録した。
• 効率性：OProver-32B（320 億パラメータ）は、はるかに少ないパラメータ数にもかかわらず、ほとんどのベンチマークで 6710 億パラメータの DeepSeek-Prover-V2 や 5600 億パラメータの LongCat-Flash-Prover（TIR 付き）を上回った。80 億パラメータ変種さえも、すべてのベンチマークで 320 億パラメータの Goedel-Prover-V2 を上回った。
• 推論時スケーリング：計算予算の増加（より多くのサンプルまたは洗練ラウンド）に伴い性能は一貫して向上したが、限界効用逓減が見られた。洗練の深さとサンプリング幅の間の最適な配分は、ベンチマークの難易度によって異なった。
• アブレーション研究：多回対話コンパイラフィードバックを除去すると、最も顕著な性能低下が生じ、反復的洗練が利益の主要な駆動因子であることが確認された。検索拡張を除去しても、一貫して（ただしより小さな）低下が生じ、検索によるグラウンディングの補完的価値が浮き彫りになった。

意義と主張

本論文は、エージェント型形式定理証明が、分離された推論時モジュールから組み立てるのではなく、統合された方策として効果的に学習しうることを OProver が実証していると主張する。証明の構築、失敗、修復の完全な軌跡に基づいてトレーニングすることで、モデルはコンパイラフィードバックや検索された文脈を推論プロセスの内在的な一部として活用することを学習する。

著者らは、性能向上が単にモデルの規模の結果ではなく、検索拡張グラウンディングとコンパイラガイド反復的洗練の相乗効果に由来すると強調する。OProver 方策と OProofs コーパスの共進化により、システムは自身の成功と失敗の試行から学習して証明能力を継続的に向上させることを可能にし、形式推論システムのトレーニングにおける新たなパラダイムを確立する。