技術要約：Leanを用いた定理証明のためのプロセス検証型強化学習

問題提起

自動定理証明（ATP）は、数学的定理の形式的な証明を生成することを目指している。大規模言語モデル（LLM）は推論タスクにおいて進歩を遂げているが、強化学習（RL）においては通常、自然言語（NL）やバイナリの結果報酬（正解/不正解）に依存している。ここに以下の乖離が生じる：

1. 疎なフィードバック: 標準的なRLアプローチは、最終的なバイナリ信号（証明の通過/失敗）のみを使用することが多く、これはクレジット割り当て（credit assignment）を疎にし、長い推論鎖を通じてモデルを導くことを困難にする。
2. 非構造化 vs 構造化: 型理論に基づいたステップごとの微細な検証を提供する記号的証明助手（Lean, Coq, Isabelleなど）とは異なり、LLMはスカラー報酬を持つトークンシーケンスとして訓練される。
3. プロセス報酬モデル（PRM）: 近年の研究では、ステップレベルの報酬を提供するためにPRMが使用されているが、これらは大規模な注釈付きデータセットを必要としたり、自然言語による思考の連鎖（CoT）の監督に依存したりしており、記号的検証の厳密な健全性を欠いている。

対処すべき核心的な課題は、外部の、潜在的にノイズを含むPRMや人間による注釈に頼ることなく、どのようにして記号的証明助手（Lean）からの豊かで構造化されたフィードバックをLLMの訓練に活用するかである。

手法

本論文は、Leanの記号的フィードバックをGroup Relative Policy Optimization（GRPO）の目的関数に直接統合するフレームワークである、プロセス検証型強化学習を提案している。この手法は、主に3つのコンポーネントで構成される。

1. 記号的プロセス・オラクル（Symbolic Process Oracle）

著者らは、Leanを単なる最終的な検証器として扱うのではなく、訓練中のプロセス・オラクルとして利用している。

• パース（解析）: 生成された証明は、抽象構文木（AST）に基づいてタクティクスのシーケンス（$T_1, \dots, T_N$）へとパースされる。
• 検証: Leanの精緻化（elaboration）プロセスは、2種類の信号を提供する：
  • 結果信号（Outcome Signal）: 証明全体が有効であるかを示すグローバルなバイナリスコア $g(Y) \in \{0, 1\}$。
  • プロセス信号（Process Signal）: 各タクティクスに対する微細なフィードバックであり、局所的に妥当なステップと、最初のエラーが発生した具体的な箇所を特定する。

2. クレジット割り当て戦略

記号的フィードバックとトークンレベルのRLの間の溝を埋めるために、著者らは特定の割り当てルールを導入している：

• 最初のエラーの伝播（First-Error Propagation）: もしタクティクス $T_j$ が失敗した場合、それ以降のすべてのタクティクス（$k \ge j$ である $T_k$）は誤りとして扱われる。これは、証明の因果関係（不適切な接頭辞は、その後の推論鎖全体を無効にする）を反映している。
• タクティクスレベルのスコアリング ($\phi$):
  • 証明が通過した場合（$g(Y)=1$）、すべてのタクティクスは正のスコア（1）を受け取る。
  • 証明が失敗した場合（$g(Y)=0$）：
    • 最初のエラーより前のタクティクスは、部分的なスコア（$d_1$）を受け取る。
    • 最初のエラーとなったタクティクスおよびそれ以降のすべてのタクティクスは、ペナルティスコア（$d_2$）を受け取る。
• トークンレベルのマッピング: タクティクスのレベルでのアドバンテージは、各タクティクスの最初のトークン（例：intro や apply といったキーワード）に対してのみ割り当てられる。これは、証明戦略が決定される意味的な決定点に合わせている。

3. RL目的関数（GRPOの統合）

本フレームワークは、結果のアドバンテージとプロセスのアドバンテージを単一のGRPO目的関数に組み合わせる：

• 結果のアドバンテージ ($A_{outcome}$): グループの平均に対する、グローバルなパス/フェイルのステータスに基づいて計算される。
• プロセスのアドバンテージ ($A_{process}$): 問題の難易度を考慮するため、グループの平均結果報酬によって正規化された、タクティクスレベルのスコアに基づく。
• 結合されたアドバンテージ: レスポンス $i$ におけるタクティクス $j$ の最初のトークンに属するトークン $t$ について：
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  非最初のトークンについては、結果のアドバンテージのみが適用される。この定式化は、検証器のグラウンドトゥルース（正解）のみに依存することで、価値モデルや補助的なPRMを必要としない。

主な貢献

1. 記号的フィードバックの定式化: 著者らは、Leanのタクティクスレベルのフィードバックをスカラーの訓練信号へと定式化し、自然言語によるガイダンスなしに、微細なトークンレベルのクレジット割り当てを可能にした。
2. 記号的検証器による誘導型RL: 彼らは、結果のみのRLよりも密度が高く、検証可能なクレジット割り当てを提供するために、Leanから直接得られる結果およびタクティクスレベルの報酬をRLフレームワークに統合した。
3. 安定したベンチマークの改善: このアプローチは、MiniF2FおよびProofNetベンチマークにおいて一貫した改善を示し、外部のPRMや自然言語による表記を必要とせずに、結果のみのRLやバニラなベースラインを上回った。

実験結果

実験は、STP-LeanおよびDeepSeek-Prover-V1.5（7Bモデル）を用いて、MiniF2F-TestおよびProofNet-Testベンチマークに対して行われた。

• 性能向上:
  • STP-Lean: 提案手法は、MiniF2Fのpass@64を**+2.5%（56.7%から59.2%へ）、ProofNetのpass@32を+1.4%**向上させた。
  • DeepSeek-Prover-V1.5: すべての設定において、一貫した（ただし僅かな）改善が見られた。
• ベースラインとの比較:
  • 本手法は、「結果のみ」のGRPOを上回った。後者は不安定であり、一部の構成においてProofNetでの改善に失敗した。
  • 大規模な推論時探索予算を必要とするシングルショット生成アプローチを用いながら、強力な木探索ベースライン（例：InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS）に対して競争力のある結果を達成した。
• アブレーション研究:
  • トークン割り当て: クレジットをタクティクスの最初のトークンに割り当てることが、全トークンに分散させる場合や最後のトークンに割り当てる場合と比較して、最も安定した結果をもたらした。
  • 最初のエラーの伝播: このルールを削除すると性能が著しく低下し、エラーの後に続くステップを無効として扱うことの必要性が確認された。
  • タイムアウト: 15秒の検証タイムアウトが、複雑だが妥当な証明を破棄することなく簡潔な証明を促すという、最適なバランスを提供した。

意義と主張

本論文は、記号的証明助手が単なる評価ツールとしてではなく、訓練中の能動的なプロセスレベルの報酬オラクルとして見なされるべきであると主張している。記号的検証に備わった「豊かで微細な構造化されたフィードバック」を活用することで、著者らは、LLMの拡張性と記号的検証の信頼性を組み合わせるRLフレームワークへの道筋を示している。

研究は以下の点を強調している：

• 高密度で検証可能な信号: プルーバー自身のエラーログや精緻化ツリーを使用することで、疎なバイナリ結果や学習されたPRMよりも優れた、健全で密度の高い報酬信号が得られる。
• 安定性: グローバルな結果報酬とローカルなタクティクス報酬の組み合わせは、タクティクスのみの訓練で見られる早期収束や、結果のみの訓練で見られる疎性の問題を防ぎ、訓練を安定させる。
• 効率性: このアプローチは、木探索の計算オーバーヘッドや、個別のPRMを訓練するためのデータ要件を必要とせずに、最先端または競争力のある性能を実現する。

著者らは、自らの手法の限界についても謙虚に述べており、現在の手法は学習されたアドバンテージ推定器ではなく固定された報酬スコア（$d_1, d_2$）に依存しており、現在はCoTを含まない純粋なLean証明に焦点を当てていること、そして長文の自然言語推論のための報酬設計は未解決の課題であることを指摘している。