技術的概要：なぜエージェント型定理証明機が機能するのか

問題定義

近年、大規模言語モデル（LLM）と検索、探索、証明アシスタント検証器を組み合わせるエージェント型定理証明機は、検証済みの数学的証明を生成する上で経験的な成功を収めている。しかし、既存の理論的枠組みはこの成功を説明することに苦慮している。古典的な証明論は証明の「存在」に焦点を当て、複雑性理論は「最悪ケース」の困難さに焦点を当てる。どちらの理論も、実務で遭遇する特定の偏った定理分布（例えば、ライブラリ定理やベンチマークファミリー）において、固定された計算予算内で特定のアルゴリズムがなぜ高確率で成功するのかを十分に説明できていない。

本論文は以下の問いに答える：「指定された定理インスタンスのストリームにおいて、固定された予算内で、特定のエージェント型証明機が検証器に受理される証明を生成する確率とは何か？」 著者らは、この「統計的証明可能性」を理解することが、古典的な決定不能性や最悪ケースの下限と矛盾することなく、検索、検証器フィードバック、分解などのコンポーネントが性能を向上させる理由を説明するために不可欠であると主張する。

手法

1. 到達性 MDP としての定式化

著者らは、形式的証明探索を決定論的ダイナミクスを持つ**有限地平線到達性マルコフ決定過程（MDP）**としてモデル化する：

• 状態（$X$）： 現在の証明義務（例：Lean における未解決ゴールのリスト）および検証器フィードバック。
• 行動（$A$）： 証明機の移動（タクティクス、推論規則、または検索コマンドなど）。
• 遷移（$F$）： 決定論的な検証器更新マップ $F: X \times A \to X$。無効な行動は失敗状態にマッピングされ、有効な行動は新しい証明状態へ遷移する。
• ゴール（$G$）： 解決済み状態の集合（空のゴールリスト）。

この定式化は、検証器の操作意味論を遷移カーネルとして扱う。著者らは、忠実な状態抽象化の下では、最適 MDP 成功確率が同一の予算内における通常の構文論的証明可能性と完全に一致することを証明しており、これにより論理的整合性を保ちつつ統計的分析を可能にしている。

2. 統計的証明可能性の定義

核心となる指標は統計的証明可能性（$SP^\pi_B(q_0)$）であり、これは初期定理分布 $q_0$ と証明機の内部ランダム性に対して平均化された、証明機の方針 $\pi$ が $B$ 回の検証器呼び出し以内に検証済み証明に到達する確率として定義される。これは最適成功確率 $SP^*_B(q_0)$ と対比される。

著者らはまた、平均切り詰め証明長さ（$Len^\pi_B(q_0)$）も追跡する。これは成功または予算の枯渇までの検証器呼び出し数の期待値として定義される。この指標は、彼らの境界における重要な解釈可能性のハンドルとして機能する。

3. 学習パイプライン分析

本論文は、現在の実践と整合するパイプラインを分析する：

1. オフライン行動価値回帰： 訓練分布における検証器支援付きロールアウト（シミュレートされた証明）から、深さごとの行動価値関数（$Q^*_t$）を学習する。
2. テスト時貪欲証明： 学習されたスコアを用いて、テスト時に最良の行動を貪欲に選択する。

この分析は仮定 3.1に依存しており、以下を前提とする：

• 訓練とテストが行われるコンパクトな集中集合（$C_t$）。
• 最適価値関数と仮説クラスのリップシッツ連続性。
• 探索分布による状態 - 行動空間の十分なカバレッジ。
• ノイズを低減するための、クエリごとの複数の独立したロールアウトラベルの利用可能性。

主要な貢献と結果

1. 主要定理（統計的証明可能性の境界）

中心的な結果（定理 3.1）は、学習された証明機の成功確率と最適証明機の成功確率との間のギャップを境界づける。この境界は、一様行動価値誤差の占有重み付き和である：

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

ここで：

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$ は、ステップ $s$ において学習された証明機がまだ問題を解決していない確率（未解決質量曲線）である。
• $\epsilon_t$ は、深さ $t$ における学習された行動価値推定量の一様誤差境界である。

誤差項（$\epsilon_t$）の解釈：
誤差は以下の 3 つの構成要素に分解される：

1. 近似誤差： 仮説クラスが真の価値関数を表現できないことによる誤差。
2. カバレッジ/幾何学的誤差： 訓練分布の有効局所次元（$d_t$）とカバレッジ定数（$c_t$）に依存する誤差。
3. ロールアウトノイズ： 回帰に使用されるモンテカルロラベルの有限数（$m_t$）に起因する分散。

2. 平均証明長さの役割

重要な洞察として、境界における主要な複雑性乗数は、学習された証明機の平均切り詰め証明長さ（$Len^{\hat{\pi}}_B(q_0)$）である。
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
これは、証明を短縮するメカニズム（効果的な分解、補題の導入など）が、局所的な価値推定誤差（$\bar{\epsilon}_B$）が一定であっても、エンドツーエンドの損失を直接減少させることを意味する。

3. マージン条件と高速収束率

マージン条件（最良の行動価値と次善の行動価値のギャップが、高確率で十分に大きい場合）の下では、境界は高速収束率に改善される：
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
これは、行動ギャップを改善すること（正しい動きを誤った動きよりも明確に優位にすること）が、収束を大幅に加速させることを示唆している。

4. スケーリング則

本論文は、サンプル複雑性のヒューリスティクスを導出する。対数因子を無視すると、誤差は $n^{-1/(d+2)}$ としてスケーリングする。ここで $n$ は検証器ラベルの予算、$d$ は有効局所次元である。これは、「テスト時スケーリング」の利益が以下の要因から生じ得ることを明確にする：

• 有効地平線の短縮（より短い証明）。
• 有効幾何学的次元の低減（より良い検索/表現）。
• 行動ギャップマージンの増大。

意義と主張

本論文は、偏ったワークロードにおいてエージェント型定理証明機が機能する理由について、コンポーネントに敏感な説明を提供すると主張する。これは、古典的論理と統計的学習の間のギャップを埋めるものであり、以下の点を示すことで実現される：

1. 検証器フィードバック： 近似誤差を減少させ、カバレッジを改善し、行動ギャップを増大させることで証明可能性を向上させる。
2. 検索と表現： 価値関数を平滑化し、状態空間を低次元領域に集中させ、悪い選択を剪定してマージンを増大させることで貢献する。
3. 証明短縮： 分解などのメカニズムは、境界における誤差の主要な乗数である「占有重み」（平均証明長さ）を減少させる。

著者らは、この理論が最悪ケースの困難性と矛盾しないことを強調する。むしろ、証明が短く、ギャップが大きく、カバレッジが良い実務で見られる特定の構造化された定理分布（ライブラリ定理、ベンチマーク）において、なぜエージェント型システムが成功するのかを説明するものである。この枠組みは、検証器を情報チャネルとして、証明機を限られた予算下で有用な情報を抽出する統計的学習者として扱い、現代のエージェント型システムで一般的な工学的選択（検索、分解、検証器ループ）に対する厳密な正当化を提供する。