大規模言語モデル（LLM）に複数のステップから成る信頼性の高いワークフローを実行させることは、現在の人工知能研究における中心的な課題となっています。LLMのエージェント機能は急速に進化していますが、ほとんどのエージェントシステムはワークフローや実行軌跡を仕様化、検証、デバッグするための形式手法を欠いているのが現状です。 この問題は数学分野における長年の課題を反映しており、自然言語の曖昧性が形式言語の開発を促進してきた歴史と類似しています。こうした背景から、研究チームは**Lean4Agent**という革新的なフレームワークを提案しました。これは従属型形式言語であるLean4を使用してエージェント挙動をモデル化・検証する初の試みです。 **Lean4Agent**の核となるのは**FormalAgentLib**という拡張可能なLean4ライブラリです。このライブラリは、明示的な仮定の下でエージェントワークフローの意味的一貫性を形式的にモデル化・検証し、実行時に顕現する障害を特定することを可能にします。さらに、**LeanEvolve**という手法が開発されました。これは**FormalAgentLib**の検証結果を活用してワークフローを改善し、エージェントの能力を向上させます。 SWE-Bench-Verifiedの困難な問題部分集合とELAIP-Benchの部分集合に対して、5つの主要LLMを用いた広範な実験が実施されました。その結果、検証に合格したワークフローは不合格のものを平均11.94%上回るパフォーマンスを示し、**LeanEvolve**はさらにSWEタスクの性能を平均7.47%改善しました。本研究は、表現力豊かな従属型形式言語を用いてエージェント挙動を形式的にモデル化・検証する新しい研究分野を確立する基礎となります。