論文要約：Lean 形式化のためのツール拡張エージェントの理解：因子分析

この論文は、自然言語で記述された数学を、厳密な形式言語である Lean 4 のコードへ自動的に翻訳するタスクにおける課題と解決策を扱っています。大規模言語モデル（LLM）の確率的な性質と、形式数学が要求する絶対的な確実性の間のギャップを埋めるため、ツール拡張エージェント（Tool-Augmented Agents）の有効性を体系的に検証し、その構成要素ごとの寄与を因子分析（Factorial Analysis）によって定量化しました。

以下に、問題設定、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題設定 (Problem)

自然言語の数学を Lean 4 に翻訳する際、従来の「ワンショット（一度きり）」のプロンプトや静的データセットへのファインチューニングには以下の根本的な課題があります。

• ハルシネーション: 学習データが不足しているため、モデルが存在しない定理や記号を捏造（ハルシネーション）し、コンパイルエラーを引き起こす。
• 意味的乖離: 集合論的な直感（教科書）と、依存型理論に基づく Lean の厳密な構文の間に深い不一致がある。
• 動的なライブラリ: Mathlib 4 はコミュニティによって頻繁に更新されるため、静的スナップショットで学習したモデルは、廃止された定義や存在しない記号を参照するコードを生成しがち。
• 構文と意味の不一致: 構文的に正しい（コンパイル通る）コードであっても、元の数学的命題と意味的に等価でない（空疎な記述など）場合がある。

これらの課題に対し、静的な生成ではなく、「試行錯誤と反復的改善」を行うエージェントフレームワークの導入が提案されました。

2. 手法 (Methodology)

2.1 エージェントアーキテクチャ

中央の LLM オーケストレーター（GPT-5.2）が、以下の 3 種類のツールを駆使して、ドラフト作成、検証、修正のループを回す構造を採用しています。

1. Expert Drafting (翻訳): 専門的にファインチューニングされたモデル（Herald）からの翻訳ドラフトの取得。
2. Knowledge Search (知識検索): Mathlib からの記号定義や型情報の検索（lean inspect name など）。
3. Compiler Feedback (コンパイラフィードバック): Lean REPL 経由でのコンパイル実行とエラーメッセージの取得。

2.2 実験デザイン：完全因子設計 (Full Factorial Design)

ブラックボックス化されがちなエージェントの性能向上要因を解明するため、3 つのツール（T: 翻訳、F: フィードバック、S: 検索）の有無を組み合わせ、$2^3 = 8$ 通りの構成（000 から 111）で実験を行いました。

• ベースライン: ツールなしのワンショット生成（Herald, GPT-5.2, Gemini-2.5-Pro）。
• 評価指標:
  1. コンパイル成功率: Lean 4 でコンパイルが通るか。
  2. 忠実度 (Faithfulness): 生成された Lean コードが元の自然言語の数学的意味と論理的に等価か（0-10 点評価、9 点以上を合格）。
  • 評価には 2 つの LLM ジャッジ（GPT-5.2 と Gemini-2.5-Pro）を用い、両者の合意（Consensus）を厳格な基準として採用しました。

2.3 データセット

4 つの数学分野（実解析、複素解析、位相幾何、代数学）から選定された、大学院レベルの定理 400 題（各分野 100 題）からなるベンチマークを作成しました。

3. 主要な結果 (Key Results)

3.1 パフォーマンスの劇的向上

• ワンショットベースライン: 最高でもコンパイル成功率 26.2%、忠実度 28.0% にとどまりました。
• フルエージェント（全ツール有効）: コンパイル成功率 89.5%、忠実度 60.5% まで向上しました。
• 結論: 反復的な改善プロセスが、静的な生成を大幅に凌駕する性能をもたらすことが示されました。

3.2 因子分析による寄与の定量化

各ツールの寄与を主効果（Main Effect）と交互作用（Interaction Effect）として分析した結果、以下のような構造が明らかになりました。

ツール	主効果 (忠実度への寄与)	役割と解釈
Compiler Feedback (F)	+32.3 ポイント	決定的な能力ドライバー。REPL フィードバックがあるかないかで、性能が「低成功領域」から「高成功領域」へ劇的にシフトします。これが最も重要な要素です。
Knowledge Search (S)	+6.8 ポイント	安定化要因。ハルシネーションを減らし、記号解決を助けます。ただし、フィードバック（F）が有効な場合、その追加効果は小さくなります（交互作用が負）。
Expert Drafting (T)	+0.9 ポイント	ほぼ不要。汎用性の高いオーケストレーター（GPT-5.2）が既に強力なため、専門モデルからのドラフトは冗長であり、場合によっては修正ループを妨げることもあります。

• 交互作用の洞察:
  • F と S の負の交互作用: コンパイラフィードバックがある場合、記号検索ツールは「コンパイルエラーからの推測」を「事前の記号確認」に置き換えることで、試行錯誤の回数を減らす（効率化）効果がありますが、最終的な忠実度そのものを劇的に上げるわけではありません。
  • F と T の負の交互作用: フィードバックがある場合、専門家のドラフトは「アンカリング効果」を起こし、最適解への収束を阻害する可能性があります。

3.3 効率性とドメイン別分析

• ステップ数: 複素解析は最も少ないステップ数（平均 6.88 回）で解決され、実解析が最も困難（平均 9.84 回）でした。
• コスト対効果: ステップ数 14 回程度で性能の大部分が飽和し、それ以上の計算コストは対してリターンが得られないことが示されました。
• モデル一般性: オーケストレーターを GPT-5.2 から Claude や Gemini に変更しても、同様の性能向上（60-65% 範囲）が得られ、この効果がモデル固有のものではなく、アーキテクチャ（特にフィードバックループ）によるものであることが確認されました。

4. 主要な貢献 (Key Contributions)

1. 体系的な因子分析: ツール拡張エージェントの性能向上要因を「ブラックボックス」として扱わず、3 つの主要ツール（翻訳、検索、フィードバック）の因果的寄与と交互作用を定量化しました。
2. 新しいベンチマーク: 400 題の大学院レベルの数学定理からなる、自然言語から Lean 4 への翻訳タスク用データセットと評価プロトコルを公開しました。
3. 設計原則の提示: 「実行環境（コンパイラフィードバック）が LLM の推論の主要な足場（Scaffold）となり、検索はそれを安定化・加速する」という、形式推論エージェントの新しい設計原則を提唱しました。
4. 再現性の確保: ベンチマーク、エージェント実装、評価スクリプト、およびエージェントのツール呼び出しログのオープンソース化を約束しています。

5. 意義と結論 (Significance)

この研究は、形式数学の自動化において、**「パラメータの専門化（ファインチューニング）よりも、検証を伴う反復的プロセス（実行と検索）」**が重要であることを実証しました。

• 静的な知識の限界: 急速に進化する形式ライブラリ（Mathlib）に対して、静的なデータセットでのみ学習したモデルは陳腐化しやすいことが示されました。
• 実行フィードバックの重要性: 誤りを即座に検知し修正する「コンパイラフィードバック」こそが、信頼性の高い形式化を実現する鍵です。
• 将来への示唆: 将来的には、これらの反復修正ループのログを用いて強化学習（RL）を適用し、エージェントが REPL 呼び出しのコストを削減しつつ、フィードバックのダイナミクスを内部化させることが期待されます。

結論として、自然言語の数学知識と機械検証可能な証明を橋渡しする未来のシステムにおいては、**「高精度な実行環境を基盤とし、検索を補助的に用いる」**というパラダイムが中心的な役割を果たすと考えられます。