Lean4Agent：エージェントワークフローと軌道のための形式モデリングと検証
本論文は、依存型形式言語Lean4を使用してLLMエージェントの動作をモデル化し検証する初めてのフレームワークLean4Agentを提案する。FormalAgentLibライブラリとLeanEvolve最適化ツールを含み、実験では検証に合格したワークフローは不合格よりも平均11.94%優れており、LeanEvolveによってソフトウェアエンジニアリング性能がさらに7.47%向上した。
大規模言語モデル（LLM）に信頼性の高いマルチステップワークフローを実行させることは、人工知能分野における中心的な課題となっている。LLMのエージェント能力は近年飛躍的に向上しているものの、ほとんどのエージェントシステムはワークフローや実行軌跡を仕様化、検証、デバッグする形式的な手法を欠いている。この課題は数学における長年の問題、すなわち自然言語の曖昧さが形式言語の発展を促した構図と似ている。このパラダイムに触発され、研究チームはLean4Agentを提案する。これは、依存型形式言語Lean4を使用してエージェントの動作をモデル化し検証する、我々の知る限り初めてのフレームワークである。
Lean4Agentの核となるのはFormalAgentLibであり、これは拡張可能なLean4ライブラリで、エージェントワークフローの形式的モデリングと、明示的な仮定の下での意味的一貫性の検証を可能にする。さらに、実行軌跡によって明らかになった実行時障害の局所化もサポートする。FormalAgentLibに基づいて、研究チームはLeanEvolveも開発した。これはFormalAgentLibの検証結果を適用してワークフローを修正し、能力を強化するツールである。
SWE-Bench-Verifiedの困難サブセットとELAIP-Benchのサブセットを用いて、GPT-4、Claudeを含む5つの主要LLMに対して広範な実験を実施した。その結果、検証に合格したワークフローは不合格のものよりも平均11.94%高い性能を示し、LeanEvolveによる修正でソフトウェアエンジニアリング（SWE）性能が平均7.47%さらに向上した。これらの結果は、形式手法がエージェントワークフローの最適化において大きな可能性を持つことを示している。
Lean4Agentは、表現力豊かな依存型形式言語を使用してエージェントの振る舞いを形式モデリング・検証する新たな分野の基盤を確立する。今後、このフレームワークはより複雑なマルチエージェント協調シナリオに拡張され、他の形式ツールと統合されることで、信頼性の高いAIシステムの構築に貢献することが期待される。本論文は2026年6月2日にarXivに提出された。