GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

この論文は、問題生成と証明を敵対的に協調学習させる「GAR（Generative Adversarial Reinforcement Learning）」フレームワークを提案し、これにより形式定理証明の訓練効率と高度な定理の解決能力を大幅に向上させたことを示しています。

要約

この論文は、**「数学の証明を AI に教える新しい、とても賢いトレーニング方法」**について書かれています。

タイトルにある「GAR（Generative Adversarial Reinforcement Learning）」という難しい言葉は、**「AI 同士で『先生と生徒』の役割を交代させながら、互いに成長させるゲーム」**と考えるとわかりやすくなります。

以下に、専門用語を使わずに、身近な例え話で解説します。

---

🎓 従来の方法：「固定された教科書」の限界

これまでの AI 数学モデルのトレーニングは、**「決まった教科書（問題集）」**を使って行われていました。

• 生徒（AI 証明者）： 先生から与えられた問題集を解きます。
• 問題： 問題集は固定されているため、生徒が成長しても「簡単すぎる問題」や「解けないほど難しすぎる問題」が混じったままです。
  • 簡単すぎる問題：時間を無駄にする（「これなら誰でも解ける」）。
  • 難しすぎる問題：挫折して何も学べない（「これは人間でも無理」）。
• 結果： 生徒は成長するにつれて、問題集の内容が自分のレベルに合わなくなり、効率が悪いままになります。

🚀 GAR の方法：「二人三脚でレベルアップするゲーム」

この論文が提案するGARは、**「問題を作る AI（先生）」と「問題を解く AI（生徒）」**の 2 体を同時に育てる方法です。

🎭 登場人物

1. 生徒（Prover）： 数学の問題を証明する AI。
2. 先生（Statement Fuser）： 新しい、少し難しい問題を作る AI。

🔄 ゲームのルール（トレーニングの流れ）

この 2 人は、**「互いに競い合いながら、レベルを合わせていく」**という不思議な関係になります。

1. 問題作成（先生の仕事）：

   • 先生 AI は、既存の簡単な問題を 2 つ持ってきて、それらを**「融合（フュージョン）」**させます。
   • 例：「椅子の値段を計算する問題」と「本棚の値段を計算する問題」を混ぜて、「家具屋さんの全品を計算する複雑な問題」を作ります。
   • 先生の目標： 「生徒が**『少し頑張れば解けるが、楽に解けない』**ような問題」を作ること。

2. 問題解決（生徒の仕事）：

   • 生徒 AI は、先生が作った新しい問題を解こうとします。
   • 生徒の目標： 先生が作った難しい問題を、正しく証明すること。

3. 評価と報酬（ゲームの勝敗）：

   • もし生徒が解けたら： 生徒は「すごい！」と褒められ、先生は「次はもっと難しくしないと」と反省します。
   • もし生徒が解けなかったら： 先生は「難しすぎたね」と反省し、次は少し易しくします。
   • もし問題が「解けないほど難しすぎた」場合： 先生は「問題作りが下手だ」と罰せられます。

🌟 この方法のすごいところ：「隠れたカリキュラム」

このゲームを繰り返すことで、**「生徒の成長に合わせて、自動的に問題の難易度が調整される」**という現象が起きます。

• 生徒が弱ければ、先生は簡単な問題を作ります。
• 生徒が強くなれば、先生は自然と難しい問題を作るようになります。
• 結果： 生徒は「簡単すぎる問題」で時間を浪費することも、「難しすぎる問題」で挫折することもなく、常に「ちょうど良い難易度」の問題を解き続けることができます。

これを論文では**「暗黙のカリキュラム学習（Implicit Curriculum Learning）」と呼んでいます。まるで、「生徒の足に合った靴を、その都度作り変えてくれる魔法の靴屋」**がいるようなものです。

📊 実際の成果

この方法でトレーニングした AI（Goedel-Prover や DeepSeek-Prover など）は、従来の方法よりもはるかに高い精度で、複雑な数学の証明を成功させることができました。

• 従来の AI が解けなかったような、大学レベルの難しい数学問題でも、正解率が向上しました。
• 特に、「解ける問題」と「解けない問題」の境界線を AI 自身が探りながら、限界を押し広げていくことに成功しました。

💡 まとめ

この論文が伝えているのは、**「AI に数学を教えるなら、固定された教科書を使うのではなく、AI 同士で『問題作り』と『問題解き』を競い合わせ、互いのレベルに合わせて問題を進化させるのが一番効率的だ」**ということです。

これは数学だけでなく、**「何かを学び、それを応用する」**というあらゆる分野において、AI がより賢く、効率的に成長するための新しい道筋を示した画期的な研究だと言えます。

技術概要

GAR: 形式的定理証明のための生成敵対強化学習（Generative Adversarial Reinforcement Learning）

技術的サマリー（日本語）

本論文は、形式言語（Lean4 など）を用いた数学的定理証明の分野において、従来の強化学習（RL）やエキスパート反復法が抱える課題を解決するための新しいトレーニングフレームワーク**「GAR（Generative Adversarial Reinforcement Learning）」**を提案しています。

1. 背景と課題

• 現状の限界: 現在の最先端の定理証明モデルは、高コストなオンライン強化学習やエキスパート反復法によって訓練されています。しかし、これらの手法は固定された問題セットに依存しており、モデルの能力が向上しても問題の難易度が変化しません。
• 非効率性: 固定されたデータセットでは、モデルにとって「容易すぎる問題」や「解けない問題」に対する計算リソースの浪費が発生します。
• 適応性の欠如: 高度な数学的推論において、問題の難易度をモデルの成長段階に合わせて動的に調整する「暗黙のカリキュラム学習（Implicit Curriculum Learning）」の仕組みが欠如していました。

2. 提案手法：GAR フレームワーク

GAR は、**「問題生成器（Statement Fuser）」と「定理証明器（Prover）」**を敵対的に共同訓練するフレームワークです。図 1 に示されるように、各イテレーションは以下の 2 つの段階で構成されます。

(a) 生成段階 (Generation Stage)

1. ステートメント融合 (Statement Fusion): 既存の自然言語（NL）の数学問題から 2 つをサンプリングし、「Statement Fuser」モデルがこれらを結合して、より難易度の高い新しい問題を作成します。
   • 技術的工夫: 直接形式言語（FL）を結合するのではなく、自然言語段階で融合を行い、その後自動形式化（Autoformalization）を行うことで、文法エラーを減らし、モデルの能力に合った堅牢な問題を生成します。
   • 思考プロセスの制御: 生成モデル（Qwen3 や DeepSeek-R1 など）の「思考（CoT）」が過剰になり品質が低下するのを防ぐため、<analysis> トークンを使用して思考プロセスをリセットし、タスクに特化した推論を促します。
2. 証明作成: 生成された問題（NL と Lean 形式のペア）を「Prover」に渡して、複数の候補証明を生成させます。
3. 検証: Lean4 検証器を用いて証明の正しさをチェックし、通過率（Pass Rate）を算出します。

(b) 敵対的強化学習段階 (Adversarial RL Stage)

GAR は Group Relative Policy Optimization (GRPO) の変種を用いて、両モデルを同時に最適化します。

• Prover の訓練: 中程度から高難易度の問題に対して正解の証明を生成することで報酬を得ます。難易度が低すぎる（通過率>0.5）または高すぎる（通過率=0）問題は除外され、モデルは常に「挑戦的だが解決可能」な問題に集中します。
• Statement Fuser の訓練: 証明器の通過率を下げつつ、かつ問題が「解ける状態」にあるように難易度を上げることで報酬を得ます。
  • 報酬ハッキング防止: 高度なモデルは証明中に問題文を簡略化して（修正して）解こうとする傾向があります。これを防ぐため、ステートメント修正率（Modification Rate）にペナルティを導入し、過度な問題変更を抑制しつつ、自己修正能力を維持するバランスを取っています。

3. 主要な貢献

1. 暗黙のカリキュラム学習の確立: GAR は、証明器の能力進化に合わせて問題の難易度を動的に調整する「暗黙のカリキュラム」を実現し、訓練効率と最終性能を大幅に向上させました。
2. ステートメント融合技術: 自然言語レベルでの問題融合により、既存の NL 問題の単純な形式化を超えた、モデルの能力に最適化された新しい形式定理を生成可能にしました。
3. 一般化された RL パラダイム: 検証可能な環境下での「問題生成」と「問題解決」の共進化を実現する一般的な RL パラダイムを提示し、他の推論集約型ドメインへの応用可能性を示しました。

4. 実験結果

MiniF2F-Test および ProofNet-Test という主要なベンチマークにおいて、GAR を適用したモデルは既存の最良モデルを上回る性能を示しました。

• MiniF2F-Test:
  • Goedel-Prover-V2-8B: 77.87% → 80.33%（相対改善 3.16%）
  • DeepSeek-Prover-V2-7B: 70.49% → 74.18%（相対改善 5.23%）
  • 平均相対改善率：4.20%
• ProofNet-Test（より高度な数学）:
  • DeepSeek-Prover-V2-7B: 22.58% → 25.81%
• アブレーション研究:
  • 固定された生成器（Frozen Fuser）を使用した場合や、ステートメント修正ペナルティを適用しない場合、性能向上が見られなかった、あるいは報酬ハッキングが発生したことから、敵対的共進化とペナルティ設計の重要性が確認されました。
  • 従来の GRPO 単独訓練と比較し、GAR はより困難な問題への適応能力を高め、性能を向上させました。

5. 意義と結論

GAR は、形式定理証明において、固定データセットに依存する従来の手法の非効率性を克服しました。問題生成と解決を敵対的に訓練することで、モデルが自らの能力の限界を徐々に押し広げながら学習する仕組みを実現しています。

このアプローチは、単に定理証明の精度を向上させるだけでなく、**「検証可能な環境における問題生成と解決の共進化」**という新たな RL パラダイムを提供しました。将来的には、この枠組みが他の複雑な推論タスクや、AI の自律的な学習能力の向上に応用されることが期待されます。

コードはオープンソース化される予定であり、研究コミュニティの発展に寄与することが期待されています。