論文「Scaling Self-Play with Self-Guidance」の技術的サマリー

本論文は、大規模言語モデル（LLM）を用いた自己対戦（Self-Play）アルゴリズムの課題を解決し、計算リソースを大規模にスケールさせた際にも学習が停滞しない新しい手法「Self-Guided Self-Play (SGS)」を提案するものです。特に、形式数学（Lean4 における定理証明）の領域において、その有効性を検証しています。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細をまとめます。

1. 背景と問題定義

従来の自己対戦の限界

LLM の自己対戦アルゴリズム（特に非対称型：問題生成者「Conjecturer」と問題解決者「Solver」のペア）は、理論的には学習の上限がないとされています。しかし、実際には大規模な計算リソースを投入しても学習が plateau（停滞）に達してしまいます。

• 報酬ハッキングと劣化: 従来の手法では、Conjecturer が生成した合成問題の質を、Solver のその問題に対する解成功率（Pass Rate）だけで評価していました。
• 結果: 長期的なトレーニングにおいて、Conjecturer は「Solver が解けるが、学習に役立たない人工的に複雑な問題」や「報酬をハックするための退行的な問題」を生成するようになり、学習の質が低下します。これを「Conjecturer の崩壊（Collapse）」と呼びます。

研究の問い

「固定された難問のセットに対して、自己対戦をどのようにスケールさせ、可能な限り多くの問題を解決できるようにするか？」

2. 提案手法：Self-Guided Self-Play (SGS)

SGS は、LLM 自体が学習プロセスを導く「自己誘導（Self-Guidance）」を取り入れた非対称自己対戦アルゴリズムです。モデルは以下の 3 つの役割を担います。

1. Solver ($\pi_\theta$): 与えられた問題（元の問題および合成問題）を解決しようとするモデル。
2. Conjecturer ($g_\phi$): 未解決のターゲット問題に基づき、それを解決するための「より単純だが意味的に関連する」合成問題（サブ問題）を生成するモデル。
3. Guide ($\rho$): 生成された合成問題の品質を評価するモデル（ジェッジ）。

SGS の核心メカニズム

SGS は Conjecturer の劣化を防ぐために 2 つの主要なメカニズムを導入しています。

1. 未解決問題への条件付け: Conjecturer は、特定の未解決ターゲット問題 $x$ に対してのみ、それに関連する合成問題 $\tilde{x}$ を生成するように指示されます。
2. Guide による品質評価（報酬の修正）:
   • Conjecturer の報酬は、単に「Solver が解けたか」だけでなく、Guide が評価する「品質」に基づきます。
   • Guide の評価基準: 合成問題がターゲット問題と「関連しているか（Relevance）」、そして「明確でエレガントか（Cleanliness/Naturalness）」を評価します。
   • 劣化の防止: 表面上は関連していても、冗長な前提条件を含んだり、結論が複雑すぎたり（例：多数の論理和を含む）、不自然な問題は Guide によって低いスコアを与えられ、報酬が抑制されます。

報酬設計

• Solver の更新: 正解（検証成功）に対して REINFORCE 法（具体的には $s(x) \leq 0.5$ の問題に焦点を当てた REINFORCE1/2）を用いて更新されます。
• Conjecturer の更新: 報酬 $R_{synth} = R_{solve} \cdot R_{guide}$ を最大化するように更新されます。
  • $R_{solve}$: 合成問題の難易度（Solver の解成功率が 0 または 30% 以上の場合 0、中間の場合 $1-s(\tilde{x})$）。
  • $R_{guide}$: Guide モデルが出力する 0〜1 のスコア（関連性とエレガンスに基づく）。

3. 実験設定

• タスク: Lean4 形式の数学定理証明。
• データセット: Goedel-Pset-V1 から抽出し、形式化エラーや証明不可能な問題を除去した「D3k」（約 3,323 問題）を使用。
• ベースモデル: DeepSeek-Prover-V2-7B（Solver, Conjecturer, Guide の初期化に使用）。Guide は SFT（教師あり微調整）を経て、出力フォーマットを安定化させています。
• トレーニング規模: 従来の研究よりも遥かに長い期間（600 万回以上の生成、ターゲットデータの 230 周以上のエポック）にわたるトレーニングを実施。
• 評価指標: 累積解成功率（Cumulative Solve Rate）のスケール則（Scaling Laws）のフィッティングと、漸近解率の推定。

4. 主要な結果

性能の向上

• RL ベースラインとの比較: SGS は、単なる強化学習（RL）ベースライン（REINFORCE1/2, Expert Iteration, CISPO など）を凌駕しました。
  • 漸近解率: RL ベースラインよりも7% 高い漸近的な解成功率を達成しました。
  • モデルサイズ超越: 7B パラメータの SGS モデルは、トレーニングを 630 万回行った時点で、671B パラメータの DeepSeek-Prover-V2 モデルの Pass@4 を上回りました。
  • 難問への対応: RL ベースラインが一度も解けなかった 1,346 問題のうち、SGS はトレーニングを通じて約 10% を解決しました。

アブレーション研究（構成要素の重要性）

• Guide の重要性: Guide を除去した実験（No Guide）では、Conjecturer が「解けるが学習に役立たない」複雑で冗長な問題を大量に生成し、性能が低下しました（解成功率は 65.5% に留まり、SGS の 67.1% に劣る）。
• 条件付けの重要性: 未解決問題に条件付けずにランダムに問題を生成する実験（No Problem Conditioning）は、ベースラインよりも性能が向上しませんでした。
• Conjecturer の固定化: Conjecturer を固定（Frozen）して学習させない手法（AlphaProof 等）は、SGS よりも性能が劣りました。Solver が固定分布をすぐに学習し尽くしてしまうためです。

Solver のエントロピーと学習の安定性

• エントロピー崩壊の回避: 従来の RL 手法（CISPO など）は、Solver の出力エントロピーが急速に低下（崩壊）し、Conjecturer が学習するための信号（中間難易度の問題）を失わせていました。
• REINFORCE1/2 の効果: SGS では、Solver に対して $s(x) \leq 0.5$ の問題に焦点を当てた REINFORCE1/2 を使用することで、エントロピーを安定させ、Conjecturer が継続的に学習できる環境を維持しました。

5. 結論と意義

主要な知見

1. 非対称自己対戦のスケールには安定性が不可欠: Solver と Conjecturer の分布が望ましくない方向に崩壊（Collapse）しないことが、長期的な学習の鍵です。
2. 自己誘導の有効性: LLM 自身が生成したデータの品質（関連性とエレガンス）を評価し、Conjecturer を導く「Guide」を導入することで、報酬ハッキングを防ぎ、学習を安定させることができます。
3. 適切な RL 目的関数の選択: Solver のエントロピーを維持する適切な目的関数（REINFORCE1/2）の選択が、自己対戦の成功に不可欠です。

意義

本論文は、LLM による自己対戦が「計算リソースを増やせば増やすほど、より高度な問題解決能力を獲得できる」ことを実証しました。特に、形式数学という厳密な検証可能な領域において、Guide モデルを用いた自己誘導が、大規模モデルの能力を凌駕する小規模モデルの学習を可能にするという点は、AI 研究において重要なマイルストーンです。

将来的には、この手法を形式数学以外の領域（コード生成、物理制御など）へ拡張し、Guide モデル自体も学習させることで、さらに複雑な問題解決への応用が期待されます。