技術要約：マルチエージェントによる証明の自動形式化のための効率的なテスト時最適化

1. 問題提起

完全な証明の自動形式化（Full-proof autoformalization）とは、広範な自然言語による数学的証明を、Leanのような証明助手内で検証可能な推論へと翻訳することを目指すものである。単一の定理に焦点を当てたステートメントレベルの形式化とは異なり、完全な証明の自動形式化は、長期的なホライゾン（long-horizon）を伴う課題である。これは、グローバルに検証可能な全体を構築するために、多数の証明ステップにわたる主張、文脈、および依存関係を調整することを要求する。

既存のアプローチには、主に2つの制限がある：

1. 高コストな学習： 多くの手法は大規模な教師あり微調整（SFT）に依存しているが、証明レベルのペアとなる教師データが不足しているため、これは困難である。
2. 非効率なテスト時最適化： 既存の推論時手法は、パイプライン全体に対して過度で、かつガイドのない修復や反復的な洗練を適用することが多い。完全な証明の設定では、検証器からのフィードバック（例：Leanのエラー）は長い生成チェーンの後にのみ到着するため、どの先行する決定が失敗の原因となったのかを特定することが極めて困難である。これにより、限られたテスト時計算資源を、無計画な再試行ではなく、ターゲットを絞った改善へと導くことが難しくなっている。

2. メソドロジー：TOMAPフレームワーク

著者らは、タスクをDecomposer-Formalizer-Prover（分解器・形式化器・証明器）のパイプラインとして構造化したTOMAP（Test-time Optimization for Multi-Agent Proof autoformalization）を導入している。その核心的な革新は、システムの決定的なボトルネックを特定し、そこを標的にする効率的なテスト時最適化戦略である。

2.1 マルチエージェント・パイプライン

システムは、以下の3つの特化したエージェントで構成される：

• Decomposer ($D$): 非形式的な証明を、明示的な依存関係を持つ、原子的で自己完結したサブ命題（証明ユニット）に分割する。
• Formalizer ($F$): 各自然言語のサブ命題を、形式的なLeanステートメントへと翻訳する。
• Prover ($P$): 各形式化されたゴールを証明するためのタクティクススクリプトを生成する。
• Verifier ($V$): 組み立てられた証明ファイルを検証する外部のLeanチェッカー。

2.2 ウィークリンク分析（Weak-Link Analysis）

最適化を行う前に、著者らはテスト時計算が最も高いリターンをもたらす箇所を判断するために「ウィークリンク分析」を行う。他のステージを固定した状態で、各ステージ（Decomposer、Formalizer、Prover）を個別に介入させ、エンドツーエンドの検証成功の回復可能性を測定する。

• 知見： Decomposerが決定的なボトルネックである。形式的なステートメント（Formalizer）や証明スクリプト（Prover）を修正する場合と比較して、自然言語による証明ユニットの仕様（主張、仮定、依存関係）を修正することは、最終的な検証成功率において著しく高い利得（51.1%の精度）をもたらす。
• 示唆： 高品質で原子的かつ自己完結した証明ユニットは、後続の形式化および証明のタスクを、FormalizerとProverの能力範囲内のローカルなタスクへと軽減させる。

2.3 テスト時最適化戦略

TOMAPは、FormalizerとProverを固定された下流の実行器として扱い、すべてのテスト時計算をDecomposerの洗練に集中させる。この最適化は、GEPAスタイル（反射的プロンプト進化）のループに従う：

1. 候補プール： 与えられた入力に対する候補となる分解案のプールを維持する。
2. ルーブリック・スコアリング： 高価なLean検証器を即座に呼び出す代わりに、候補をLLMベースの「ルーブリック・ジャッジ（評価基準判定器）」によって3つの次元でスコアリングする：
   • 意味的忠実性（Semantic Faithfulness）： 元の自然言語の証明との整合性。
   • 証明可能性（Provability）： 各ユニットが自己完結しており、論理的に完全であるかどうか。
   • Leanへの親和性（Lean Friendliness）： 仮定の明快さ、明示性、および曖昧さの回避。
3. パレート誘導型進化（Pareto-Guided Evolution）： 候補は、ルーブリック・スコアに基づくパレート・フロント上で評価される。反射的なLLMプロポーザーが、高パフォーマンスな候補を選択し、ルーブリックのフィードバックに基づいてそれらを批判し、修正された分解案を提案する。
4. 検証ゲート（Verification Gating）： 高品質な閾値（ルーブリック・ゲートを通過したもの）を満たす候補のみが、高価なグラウンドトゥルースとしてのLean検証のために、下流のFormalizer-Proverパイプラインへとコミットされる。

この二段階設計は、探索を導くための安価で密なプロキシ・フィードバック（ルーブリック）と、有望な候補のみに限定された高価で忠実な検証（検証器）とのバランスをとっている。

3. 主な貢献

• ボトルネックの特定： 著者らは、ウィークリンク分析を通じて、証明の分解の質が完全な証明の自動形式化における成功の主要な決定要因であることを実証的な証拠とともに示し、最適化の焦点をパイプライン全体からDecomposerのインターフェースへとシフトさせた。
• TOMAPフレームワーク： 検証から探索を切り離した新しいテスト時最適化手法を提案する。これは、マルチオブジェクティブなルーブリック・フィードバックとパレート選択を用いて証明の分解を進化させ、探索フェーズにおける高価なLean呼び出しへの依存を大幅に削減する。
• 効率性と性能： 大規模な学習を必要とせず、代わりに効率的な推論時最適化に頼ることで、最先端（SOTA）の結果を達成している。

4. 実験結果

実験は、PROOFFLOWBENCH（184の学部レベルの問題）およびminiF2F（244の高校レベルの問題）を用いて行われた。

• 性能： TOMAPは、学習ベースのベースライン（例：ProofBridge）および学習フリーのベースライン（例：PROOFFLOW, Monotonic）の両方を上回る。
  • PROOFFLOWBENCHにおいて、TOMAP（Gemini3-Proを使用）は、最良の従来手法と比較して、構文的正当性と意味的忠実性の結合スコアを**19.0%**向上させた。
  • miniF2Fにおいて、結合指標で**8.2%**の向上を達成した。
• 意味的忠実性： TOMAPは、元の証明の意味構造を保持する能力においてモノリシックな生成器を大きく上回り、他の手法に見られる「意味的には誤っているが、構文的には正しいLeanコードを生成してしまう」傾向を回避している。
• コスト効率： TOMAPはナイーブなベースラインよりも多くのテスト時計算を必要とするが、パイプライン全体の広範な反復試行に依存する方法と比較して、より低い総コストで高い成功率を実現している。
• スケーリング分析： アブレーション研究により、ほとんどの性能向上は分解の進化における最初の数回のイテレーション内で発生することが明らかになり、テスト時予算を選択するための実践的な指針を提供している。

5. 意義と主張

本論文は、完全な証明の自動形式化は根本的に分解の質の問題であると主張している。Decomposerが最もフィードバックによる回復が容易なステージであることを特定することで、著者らは、形式化や証明を繰り返し試行するのではなく、自然言語による証明構造の洗練にリソースを集中させることで、効率的なテスト時最適化が可能であることを示している。

TOMAPの意義は、以下の点にある：

1. 自然言語の証明と形式的な検証の間のギャップをより忠実に埋めることにより、検証可能な数学的推論の天井を引き上げる。
2. 複雑な微調整アプローチに代わる、スケーラブルで学習を必要としない代替手段を提供する。
3. 因果分析を通じて特定された「弱点」を優先することで、マルチエージェント・システムにおける限られたテスト時計算資源の割り当てに関する実用的なフレームワークを提供する。

著者らは、ベンチマーク規模の証明に限定されていること、および入力される非形式的な証明が正しいという仮定に基づいていることを限界として挙げている。誤った証明ステップの検出と修復については、今後の課題としている。