技術要約：Leanにおけるエージェンティックな定理証明器のコスト・品質トレードオフの最適化

問題提起

大規模言語モデル（LLM）は、エージェンティックなワークフローを採用することで、Lean証明支援システム内での自動定理証明において著しい進歩を遂げている。これらのワークフローは通常、複雑な問題をより小さな補題へと分解し、多数の証明試行を生成し、コンパイラのフィードバックを利用して探索をガイドする。このアプローチは、PutnamBenchのような難易度の高いベンチマークにおいて高い性能を発揮する一方で、法外な計算コストという課題を抱えている。現在のシステムは、問題の難易度に関わらず、分解と証明生成に対して固定された事前指定の予算をすべての問題に割り当てる「固定ステップ」ポリシーを採用している。この手法は、エージェントが実現不可能な問題や、成功の見込みが低い誤った定式化された命題に対して多大な計算資源を浪費してしまうため、大幅な無駄を生じさせる。本研究が取り組む核心的な課題は、既存のエージェントにおける動的なコスト意識の欠如であり、これが計算支出と証明成功率の間のトレードオフを最適化できていない点にある。

メソドロジー

著者らは、静的なポリシーを動的でデータ駆動型のルーティング決定に置き換えるために設計された、新しい**アクション・ルーティング・エージェント（Action Routing Agent）**アーキテクチャを提案している。このシステムは概念的に以下の2つのプレーンに分かれている。

1. データプレーン（証明生成）

先行研究（例：Chen et al., 2025c; Varambally et al., 2025）に着想を得たデータプレーンは、実際の証明生成を担う。これは4つのモジュールを通じて動作する：

• 分解モジュール（Breakdown Module）： 汎用モデル（GPT-OSS-20B）が、元の問題を自然言語の補題と証明のスケッチへと分解する。
• 定式化器（Formalizer）： エージェントは、構文エラーや型エラーなしにコンパイルできる最良の候補を選択しながら、GOEDEL-FORMALIZER-V2-8Bを用いてこれらの補題をLeanコードへと定式化する。
• 形式的分解証明器（Formal Breakdown Prover）： システムは、自然言語のスケッチに基づいたガイドの下、定式化された補題を公理として使用し、トップレベルの定理の証明を試みる。
• 補題証明器（Lemma Prover）： 分解が証明されると、エージェントはスタックに新しい依存関係をプッシュしながら、証明に必要な個々の補題を再帰的に証明しようと試みる。

2. コントロールプレーン（コスト・品質ルーティング）

コントロールプレーンは、失敗した証明試行の軌跡を観察し、現在のターゲットに対する試行を継続するか、あるいは現在の分解を破棄して新しい分解による再試行を行うかを決定する。これは、コスト・品質のトレードオフに基づいた軽量なルーティング・ポリシーを利用する：

• 状態 ($s$)： 証明試行、コンパイル結果、エラーメッセージ、および出力の長さを含む、失敗した試行の履歴を要約したもの。
• アクション空間： $\{ \text{ATTEMPT (試行)}, \text{TERMINATE (終了)} \}$。エージェントは、現在のターゲットに対して別の証明をサンプリングするか、現在の分解を破棄するかを選択する。
• 効用関数： ルーターは、効用スコア $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$ を計算する。ここで：
  • $\hat{q}(s)$ は、次の試行における成功予測確率（Quality/品質）である。
  • $\hat{c}(s)$ は、次の試行における予測コスト（LLMの生成トークン数/SFLOPsで測定）である。
  • $\lambda$ は、計算コストへのペナルティを制御するハイパーパラメータである。
• 決定規則： もし $\tau(s) > 0$ であれば、エージェントは継続し、そうでなければ現在の軌跡を終了する。

推定器：

• コスト推定器： 試行コストは独立同一分布であると仮定し、軌跡内における過去の試行の平均コストを使用する。
• 品質推定器： 軌跡の特徴（特に以下の項目）に基づいて成功確率を予測するように訓練されたロジスティック回帰モデルである：
  • 証明の類似度（Proof Similarity）： 正規化された証明の平均ペアワイズ・ファジー文字列比率（低すぎる類似度は混乱を示唆する）。
  • エラーの多様性（Error Diversity）： ユニークなコンパイルエラーの総数に対する全エラーの割合（低い多様性は、持続的な失敗モードを示唆する）。
  • 試行回数（Attempt Count）： 過去の試行回数。

主な貢献

1. 非効率性の特定： 本論文は、Leanエージェントにおける固定ステップのスケーリングが極めて非効率であり、不要な試行を減らすことが優れたコスト・品質トレードオフを実現するために不可欠であることを特定している。
2. 新しいアーキテクチャ： オンラインかつ適応的なコスト・品質ルーターを備えた、補題形式のLean証明器の開発。これは、追加の計算の限界効用を動的に評価する。
3. 実証的検証： 提案されたルーターが、計算資源の割り当てのための有用なシグナルとして、失敗した軌跡が実際に機能することを示し、失敗した軌跡から精度を維持しつつ計算資源の無駄を大幅に削減できることを実証した。

実験結果

システムは、固定ステップのベースラインおよびグラウンドトゥルースの成功確率にアクセスできる「オラクル（Oracle）」エージェントと比較しながら、PutnamBenchの85問のサブセットを用いて評価された。

• コスト削減： 同等の精度において、提案されたエージェントは、固定ステップのベースラインと比較して、必要な予算を平均で 25.8% 削減した。
• 精度の向上： 同等のコストにおいて、エージェントは解決率で 7.8% の向上を達成した。
• 具体的なトレードオフ：
  • 約43.6%の解決率を達成するために、固定ステップのベースラインは31.6 M SFLOPsを必要としたのに対し、ルーティング・エージェントはわずか22.6 M SFLOPsで済んだ（28.4%のコスト削減）。
  • 中程度の予算領域（約41.6%の解決率）において、エージェントはコストを29.6%削減した（17.5 M vs. 24.9 M SFLOPs）。
• アブレーション研究：
  • 特徴量の重要度： 「エラーの多様性」が品質推定において最も重要な特徴量であることが判明した。
  • データプレーンの影響： 補題形式の分解アーキテクチャ自体が、同じ8Bモデルを用いた全証明生成アプローチよりも解決率をほぼ100%向上させ、32Bモデルの性能に迫る結果となった。
  • オラクルとの差： ルーティング・エージェントは固定ベースラインを大幅に上回ったものの、オラクル・エージェント（59.9%のコスト削減を達成）との間には依然として差が存在しており、特徴量エンジニアリングや推定器のアーキテクチャに改善の余地があることを示唆している。

意義と主張

本論文は、失敗したLeanの軌跡が、エージェンティックな定理証明におけるコストを考慮したリソース割り当てのための、実行可能なシグナルを提供すると主張している。静的な固定ステップ・ポリシーから動的なルーティングへと移行することで、エージェントはパフォーマンスを損なうことなく、計算の無駄を大幅に削減できる。著者らは、本研究を形式的な数学的証明における「コストを考慮した制御（cost-aware control）」への基礎的な一歩として位置付けており、将来のエージェントは、推論予算を静的に割り当てるのではなく、観察された進捗や失敗パターンに基づいて計算を動的に割り当てるべきであると示唆している。結果は、固定ステップ・ポリシーには効率改善の余地が多分に残されていること、そしてルーティング戦略が不要なコストを効果的に軽減できることを示している。