Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

提供されたテキストに基づき、論文**「Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory」**の技術的要約を以下に記します。

概要

本論文は、依存型形式言語（FL）であるLean4を利用して、大規模言語モデル（LLM）エージェントのワークフローおよび実行軌跡（trajectory）を統一的にモデリング、検証、および洗練させるための初のフレームワークであるLean4Agentを紹介するものである。著者らは、自然言語の曖昧さがハルシネーション、論理的不整合、および実行失敗を引き起こしやすいマルチステップ・エージェント・システムにおいて、信頼性を確保するという極めて重要な課題に取り組んでいる。形式定理証明のパラダイムを借用することで、Lean4Agentはエージェントの振る舞いに対して数学的に証明可能な保証を提供する。

核心的な貢献

本フレームワークは、主に以下の2つのコンポーネントで構成される：

1. FormalAgentLib: エージェントのワークフローを形式的にモデリングし、検証するための拡張可能なLean4ライブラリ。
2. LeanEvolve: 検証結果を利用してワークフローを自動的に改善する、実行時の洗練（refinement）手法。

手法：3層の検証システム

FormalAgentLibは、3つの異なる正当性のレイヤー上で動作する。

レイヤー1：構造的検証（Structural Verification）

• 目的: コンパイラのチェックと同様に、ワークフローの構文的および構造的な適格性を検証する。
• メカニズム: 変数、実行ノード、およびグラフ遷移のための型システムを定義する。以下の項目をチェックする：
  • ノードの到達可能性。
  • エッジの妥当性（逐次、分岐、ループ）。
  • 読み書きの一貫性（Read/Write Consistency）: ノードが、初期パラメータまたは到達可能な先行ノードによって生成された変数のみを読み取っていることを保証する。
• 結果: スコープ内で生成されていないデータにアクセスしようとするステップなどの「未解決の読み取り（unresolved reads）」といった構造的エラーを検出する。

レイヤー2：静的意味論的検証（Static Semantic Verification）

• 目的: 明示的な仮定（具体的には、LLMExec仮定：LLMステップが前提条件を満たす状態で開始された場合、事後条件を満たす状態を生成する）の下での意味論的な自己整合性を検証する。
• メカニズム:
  • 述語システム（Predicate System）: 曖昧な自然言語の指示を、具体的かつ決定可能な述語（例：isValidJson, matchesJsonSchema, nameExists）に変換する。
  • ホーア論理（Hoare-Style Logic）: 各エージェントのステップを、前件条件（pre-condition）と後件条件（post-condition）のペアとしてモデル化する。
  • 意味論的ワークフローグラフ: これらの契約（contracts）をワークフローグラフ全体に伝播させ、あるステップの出力が次のステップの入力要件を満たしていることを確認する。
  • 暗黙的な変数（Implicit Variables）: 情報の流れとコンテキスト管理を追跡し、人間が見落とす可能性のあるエラー（例：並列ブランチにおけるコンテキストの分離）を検出する。
• 結果: 実行前に、ワークフローが意味論的に自己完結しているかどうかを特定する。

レイヤー3：実行軌跡の検証（Execution Trajectory Verification）

• 目的: 実際の実行実行におけるLLMExec仮定を検証し、失敗箇所を特定する。
• メカニズム:
  • Leanを使用して決定可能な述語を評価する。
  • 外部ツール（例：Pythonバリデーター）を使用して、実行時のチェック（例：URLの接続性）を行う。
  • 非決定的な特性については、環境からのフィードバック（例：テストケースのエラー）を活用し、LLM-as-a-Judgeを用いる。
• 結果: 軌跡が期待される後件条件から逸脱した正確なステップを特定し、標的を絞ったデバッグを可能にする。

LeanEvolve: 形式的ガイダンスによる洗練

ワークフローが静的検証を通過したにもかかわらず、実行中に失敗した場合、LeanEvolveが用いられる：

• 形式的ガイダンス・モード（Formal-Guided Mode）: レイヤー3の診断を使用して、特定の違反された述語と失敗したステップを特定する。その後、LLMに対して、この正確なエラーの局所化に基づいてワークフローの仕様を修正するようプロンプトを出す。
• 純粋LLMモード（Pure-LLM Mode）: 形式的なガイダンスなしに、広範な探索と試行錯誤による修正を行うフォールバックまたはアドオンであり、形式的なフィードバックが乏しいタスクに有用である。
• 結果: システムは、タスクを解決するまでワークフローを反復的に進化させる。

実験結果

著者らは、5つの主要なLLM（GPT-5.2、GLM-5、Kimi-K2.5などを含む）を用いて、2つの困難なベンチマークでLean4Agentを評価した：

1. SWE-Bench-Verified (Hard Subset): コード生成とデバッグを含む、現実世界のソフトウェアエンジニアリングタスク。
2. ELAIP-Bench: 複雑な推論と証拠の検索を必要とする、AI論文の理解タスク。

主な知見:

• 検証の影響: レイヤー2の検証を通過したワークフローは、通過できなかったものよりも平均で11.94%（SWEでは14.80%、ELAIPでは9.07%）高い性能を示した。これは、形式的検証が欠陥のあるワークフローを効果的にフィルタリングできることを示している。
• 洗練の影響: LeanEvolveを使用することで、検証済みのワークフローはSWEタスクにおいて平均**7.47%**の追加的な改善を達成した。
• 形式的 vs 純粋LLM: 形式的ガイダンスを用いた進化は、純粋LLMによる進化よりも、最初に失敗したケースの修正において平均で**7.00%**上回った。これは、正確なエラーの局所化が、盲目的な試行錯誤よりも優れていることを証明している。
• モデルの感度: 小規模なモデルはワークフローの品質に対してより高い感度を示し、大規模なモデルよりも検証による恩恵を多く受けた。

結論

Lean4Agentは、検証可能なAIの新しいパラダイムを確立する。依存型形式言語をエージェントシステムに適用することで、ヒューリスティックな評価を超え、数学的に根拠のある保証を提供する。本フレームワークは、タスクのパフォーマンスを向上させるだけでなく、高リスクな領域において、自己改善し信頼性の高い自律型エージェントを開発するための基礎を提供する。著者らは、この分野の研究を促進するためにコードをオープンソース化する予定である。