技術的サマリー：強化学習で訓練された Lean 定理証明器における推論時の多様性

問題定義

近年のニューラル定理証明器、特に強化学習（RL）と検証可能な報酬（RLVR）を用いて訓練されたものは、miniF2F などの形式的証明ベンチマークで高い性能を達成している。 prevailing な仮説は、十分な RL 訓練と推論時計算量の増加（i.i.d. サンプリングを介して）により、モデルが形式的証明に必要な構造的な事前分布を内部化できるとするものである。

本論文はこの仮説に異議を唱え、RL 訓練済み Lean 証明器における推論時のモード崩壊（mode collapse）という現象を診断する。具体的には、著者らはサンプリング予算（$k$）を増加させても、期待よりも遥かに早く収穫逓減が生じることを観察した。DeepSeek-Prover-V1.5-RL による miniF2F-test ベンチマークにおいて、サンプリング予算を $k=32$ から $k=64$ に倍増させても、解決された定理の数は 0 件増加し（42/244 で停滞）、モデルは狭い証明戦略のセットに収束し、追加の確率的サンプルが提供された場合でも代替案を探求できない。

手法

本研究は、DeepSeek-Prover-V1.5-RL とその非 RL ベース変種を用いた制御された診断フレームワークを採用し、DeepSeek-Prover-V2-7B（RL）および Goedel-Prover（SFT のみ）とのクロスモデル比較も行っている。

1. スケルトンスケジュール介入

プラトーが計算量の不足ではなく構造的な多様性の欠如によるものかどうかをテストするため、著者らは15 個の固定的かつ決定論的なタクティクススケルトンのスケジュールを導入した。

• 構造: 15 個の手動選択された Lean タクティクススケルトン（例：simp, intro, constructor, aesop）と 8 個のゴールヒントコメント（自然言語による提案）を組み合わせ、$15 \times 8 = 120$ のグリッドを構成する。
• 実行: 予算 $k$ に対して、モデルはこのグリッドの最初の $k$ 個のエントリを試行する。これにより、モデルはランダムなサンプリングに依存するのではなく、特定の戦略的な開始で証明を開始することを強制される。
• アブレーション: 改善の源泉を特定するため、著者らは以下の条件を比較した。
  • **B-RL **(Skeleton): 構造化された 15 スケルトンスケジュール。
  • **C1 **(Paraphrase): 16 個の意味的に等価な指示のパラフレーズ（タクティクス構造なし）。
  • **C2 **(Irrelevant Comments): 16 個の内容のない Lean コメント。
  • **C3 **(NL-only): タクティクス接頭辞なしの自然言語ヒントのみに特化した条件。

2. 難易度層別化

著者らは、leave-one-out 構成を用いた経験的形式的化難易度スコア（$\sigma$）を定義した。対象定理について、$\sigma$ は他のベースラインモデル（Goedel-Prover, V2-7B）が介入なしで解決する数をカウントする。これにより、定理を Frontier（他モデル未解決）、Hard、Medium、Easy、Trivial のバケットに層別化する。

3. 直接的な分布測定

行動上のプラトーを超えて分析するため、著者らは 13,159 個の確率的サンプルにおける先頭タクティクスヘッドの多様性を分析した。各定理に対して生成された異なる先頭タクティクス識別子（例：have, rw, norm_num）の数をカウントする。

主要な結果

1. 構造的ガイダンスによるプラトーの打破

• ベースラインの崩壊: i.i.d. サンプリングを用いた DeepSeek-Prover-V1.5-RL は、$k=16$ で 38 定理、$k=32$ で 42 定理を解決し、$k=64$ でも 42 で留まる。
• スケルトンの有効性: 固定的なスケルトンスケジュールはこのプラトーを打破し、$k=16$ で55 定理（相対的に 45% の改善）を解決し、$k=64$ まで新たな証明を見出し続ける（合計 60 件）。
• アブレーションの知見:
  • 構造対多様性: 指示のパラフレーズ（C1）はベースラインと同じ pass@16（38/244）しか示さなかったが、無関係なコメント（C2）は性能を 25/244 に低下させた。これは、改善が単なるプロンプトの多様性ではなく、構造的ガイダンスによって駆動されていることを確認する。
  • 自然言語対タクティクス: NL のみの条件（C3）は 48/244 を解決し、ベースラインと完全なスケルトンの中間となった。これは、自然言語ヒントがギャップの約 58% を回復させ、残りをリテラルなタクティクス接頭辞が補完することを示唆している。

2. 改善の局在化

構造的な改善は、Easy および Trivial バケット（他のオープンソース証明器では解決可能だが V1.5-RL の i.i.d. サンプリングでは見逃された定理）に集中している。

• 統合された Easy+Trivial の列において、スケルトン介入はネット +15 の利益をもたらしたが、パラフレーズは 0、無関係なコメントは -14 だった。
• どの摂動も「Frontier」バケット（いかなるベースラインでも未解決の定理）を解き放たず、この介入は能力の拡大ではなく、既知の解決可能問題の探索不足を remedy していることを示唆している。

3. モード崩壊の RL 特異性

• ベースモデルとの対比: DeepSeek-Prover-V1.5-Base（非 RL）は、いかなる条件（i.i.d. またはスケルトン）下でも0 件の定理しか証明しない。これは、RL が証明能力を創出する段階であると同時に、その能力を狭い方策に崩壊させる段階であることを確立する。ベースモデルは有効な証明を生成する能力を欠いており、RL 段階が能力を創出するが、それを狭い方策に崩壊させる。
• クロスモデル対比:
  • V2-7B (RL): 平坦な集計利益（+1）を示すが、いかなる i.i.d. ベースラインでも到達不可能だった+3 の Frontier 定理を解き放つ。
  • Goedel-Prover (SFT): スケルトンにより負の利益（-10.0 $\pm$ 4.4）を示す。SFT 訓練済みモデルは既にタクティクスステムの広範なセットを探求しているように見え、固定的なスケルトンスケジュールは冗長か制限的である。

4. 崩壊の直接的証拠

分布分析により、中央値の定理は 64 個のサンプルを通じてわずか2 個の異なる先頭タクティクスヘッドしか受けず、ベンチマークの 49% が決定論的な単一の戦略的開始を受け取ることが明らかになった。観測されたシャノンエントロピーは理論容量の $\le 8\%$ であり、深刻なモード崩壊を確認する。

意義と主張

本論文は、「タクティクススケルトンが性能を向上させる」という物語を、**「RL 訓練済み証明器は推論時にタクティクス空間を著しく過少探索している」**という物語へと再構成する。

• 二重の役割としての RL: 著者らは、RL は二重の役割を果たすと主張する。すなわち、ベースモデルが何の能力も持たない中で証明能力を創出する段階であると同時に、その能力を狭い方策に崩壊させる段階でもある。
• 推論時のスケーリング: 結果は、i.i.d. サンプリングを介した推論計算量の単純なスケーリングが、想定よりも遥かに早く収穫逓減に陥ることを示唆する。構造的な多様性（プロンプトを介した証明戦略の変化）は、スケーリングにとってより効率的な軸である。
• 回復可能性: モード崩壊は RL 訓練済みモデルに特異的である。SFT 訓練済みモデルは構造的ヒントを介して同様の回復可能な崩壊を示さず、むしろそれによって被害を受ける。これは、将来の介入（訓練時エントロピー正則化または推論時スケルトン検索）が、能力創出と多様性維持の間のトレードオフを navigat する必要があることを示唆している。

本研究は、「モード崩壊」が形式的検証ドメインにおける RL 微調整プロセスに固有の、パイプラインに依存する現実の現象であり、固定的な構造的介入が追加の訓練を必要とせずに失われた探索を効果的に回復し得ることを結論づける。