Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

タイトル: 平坦なエージェント型定理証明者と階層的なエージェント型定理証明者の間における指数関数的なサンプル複雑性の分離

著者: Sho Sonoda, Shunta Akiyama, Yuya Uezato
所属: CyberAgent, RIKEN AIP
日付: 2026 年 5 月 7 日

1. 問題定義

近年のエージェント型定理証明者は、戦術レベルの探索に着手する前に、中間補題の生成、証明スケッチ、またはサブゴールの分解などの分解戦略を採用することが多い。古典的な証明論では、補題が導出を短縮しうることが示唆されているが、これらの中間ステップを発見し証明することの統計的学習コストは未解決の課題である。具体的には、補題を証明すること自体が困難である場合、なぜ学習された証明者はそれに労力を費やすべきなのかという問いが生じる。

本論文は、再利用可能な証明構造（階層的）を学習することが、完全にインライン化された証明トレース（平坦）から学習する場合と比較して、固定された探索予算内で検証済みの証明を見つける確率を高めるかどうかという統計的学習問題に取り組む。著者らは、すべての数式に対する最悪ケースの証明複雑性ではなく、初期定理状態と成功した検証済み証明トレースからなる「教師」証明者が誘発するデータ分布に焦点を当てる。

2. 手法

著者らは、定理証明を、状態が証明状態であり、行動が戦術、推論規則、または高レベルの分解移動である決定論的有限時間マルコフ決定過程（MDP）としてモデル化する。そして、3 つの異なる設定下での成功した教師トレースからのオフライン模倣学習を分析する。

• 設定 1（平坦）: 教師は完全にインライン化された低レベルの証明トレースを生成する。学生はグラフ予測やメモ化なしにこれらのトレースを模倣する。繰り返される部分証明は、訓練データとテストデータにおいて、個別にコピーされた出現として現れる。
• 設定 2（階層的）: 教師は、ノードが再利用可能な証明ブロックを表す高レベルの証明有向非巡回グラフ（DAG）を構築する。学生は、高レベルのグラフ行動（ブロックの選択、展開、再利用）と低レベルの局所解決のためのグラフ予測器と方策を学習する。訓練データはインライン化されたトレースで構成され、学生は潜在的な証明 DAG 構造を推論する必要がある。
• 設定 3（比較）: 平坦な学生と階層的な学生の両方が、階層的な教師によって生成された同じソースデータ（インライン化されたトレース）で訓練される。平坦な学生は潜在的なグラフ構造を破棄するのに対し、階層的な学生はそれを推論する。この設定は、表現がサンプル複雑性に与える影響を孤立させる。

分析は、以下の 3 つの主要な量に依存する。

1. $L$（平均長さ）: 成功した証明における決定の平均数。
2. $\eta$（本質的探索損失）: 教師の次の行動が学生のトップ-$k$候補リストに含まれていないために失われる確率質量（局所的な予測可能性）。
3. $e$（模倣誤差）: 学生の方策と教師の方策との間のカルバック・ライブラー（KL）ダイバージェンス。

著者らは、模倣誤差をトップ-$k$省略確率に変換するために Tsybakov 型のマージン条件を仮定し、教師の行動が学生のトップ-$k$リストに含まれている場合、探索が完全であると仮定する。

3. 主要な貢献

• 定式化: 本論文は、検証器に導かれた定理証明を有限時間 MDP として定式化し、「統計的証明可能性」を、初期状態の分布における予算内で検証済みの証明を見つける平均確率として定義する。
• 成功保証: 著者らは、インライン化されたトレースで訓練された平坦な学生と、再利用可能な DAG の予測を訓練された階層的な学生の両方に対して、有限サンプルの成功限界を導出する。これらの限界は、決定の数、本質的なトップ-$k$損失、学習されたランキング誤差を明示的に分離する。
• 指数関数的な分離: 主要な理論的結果は、十分なサンプル複雑性における指数関数的な分離である。再利用可能な証明 DAG が木に平坦化されると、同一の部分証明が指数関数的に多数回複製される。本論文は、同じデータソースで訓練された場合でも、階層的学習者に対する十分なサンプル証明書は、平坦な学習者に対するそれよりも指数関数的に小さくなりうることを証明する。
• 潜在グラフ学習: 本論文は、EM スタイルの事後重み付けアプローチを用いてインライン化されたトレースから潜在的な証明 DAG を推論しなければならない階層的な学生に対する学習率を提供し、グラフ予測誤差と事後の不一致を考慮する。

4. 結果

核心的な結果は定理 6に示されており、これは目標失敗レベル $\delta$ を達成するために平坦な学生と階層的な学生に必要とされる認証済み十分なサンプル数（$\bar{N}$）を比較する。

• 平坦な限界: $\bar{N}_{flat}(\delta) \propto (L_{flat}/\delta)^{1/(p\gamma)}$
• 階層的な限界: $\bar{N}_{hier}(\delta) \propto \max(L_{hi}, L_{lo}/\delta)^{1/(p\gamma)}$

ここで、$L_{flat}$ は展開されたトレースの長さであり、$L_{hier} = L_{hi} + L_{lo}$ は階層的表現の長さである。

本論文は、サイズ/深さパラメータ $D$ でインデックス付けられた定理の族において、平坦化プロセスにより証明長が指数関数的に成長する場合（$L_{flat}/L_{hier} = \exp(\Omega(D))$）、必要なサンプルの比率も指数関数的に成長することを示している。
$$\bar{N}_{flat}(\delta) / \bar{N}_{hier}(\delta) \geq \exp(\Omega(D))$$

この分離は、平坦な学習者が同じ困難な局所的な論証をすべての出現に対して独立して学習しなければならないのに対し、階層的な学習者は共有されたブロックを一度学習して再利用するから生じる。本論文は、中間補題を除去する（平坦化する）ことが証明サイズを指数関数的に爆発させ、それによって平坦な学習者のサンプル複雑性を増大させる例として、カット除去の例（付録 G）を用いて説明している。

5. 意義と主張

本論文は、最悪ケースの証明複雑性の議論とは区別される、階層的証明がなぜ役立つのかを説明する具体的な統計的メカニズムを提供すると主張している。その意義は、分解の利点が単に論理的な導出を短縮することではなく、学習者に対する統計的負担を軽減することにあると特定されている点にある。

• データ分布への意識: この結果は、学習の効率性がデータ分布の構造に依存することを浮き彫りにする。成功した証明が中間的な論証を再利用する場合、階層的な表現はこの共有を捉えるが、平坦な表現はそれを破壊し、冗長な学習タスクにつながる。
• 限界: 著者らは主張について控えめである。これは最悪ケースの下限ではなく、明示的な階層なしに同一の部分問題を完全に認識する（完全な正規化を達成する）平坦な学習者を否定するものではないと述べている。この分離は、平坦化が再利用可能な証明構造を破壊し、データ分布にそのような共有が prevalent な証明が含まれる場合に特に成立する。
• 実用的な含意: この知見は、検証器ベースの定理証明において、再利用可能な証明構造（補題、サブゴール）の予測を学習することは、グラフ予測器が教師の証明書を高い確率でカバーできる限り、所定の成功確率を達成するために必要なサンプル複雑性を指数関数的に削減しうることを示唆している。

本論文は、それらの補題が再利用可能である場合、補題を証明するという「高価な迂回」は統計的に正当化されると結論づけている。なぜなら、それらを一度学習するコストは、平坦な枠組みの中でそれらを繰り返し再発見するコストよりもはるかに低いためである。