大規模言語モデル（LLM）に信頼性の高い多段階ワークフローを実行させることは、人工知能における中心的な課題となっています。LLMのエージェント能力は近年進歩しているものの、ほとんどのエージェントシステムは、ワークフローと実行軌跡を仕様化・検証・デバッグするための形式的手法を欠いています。この課題は、自然言語の曖昧さが形式言語の開発を動機付けてきた数学における長年の問題と類似しています。このパラダイムに触発され、研究者らはLean4Agentを提案しました。これは、依存型形式言語であるLean4を用いてエージェントの動作をモデル化・検証する、知る限り初のフレームワークです。
Lean4Agentの中核はFormalAgentLibです。これは、明示的な仮定の下でエージェントワークフローの意味的一貫性を形式的にモデル化・検証し、実行軌跡から明らかになる実行時障害の特定を可能にする、拡張可能なLean4ライブラリです。このFormalAgentLibに基づき、研究者らはLeanEvolveを開発しました。これはFormalAgentLibの検証結果を活用してワークフローを修正し、その能力を強化します。
フレームワークの有効性を評価するため、研究者らはSWE-Bench-Verifiedの困難な問題のサブセットとELAIP-Benchのサブセットにおいて、5つの主要LLMを対象に広範な実験を行いました。その結果、検証に合格したワークフローは不合格のものより平均11.94%高い性能を示し、LeanEvolveはSWE性能を平均7.47%さらに向上させました。これらの結果は、エージェントワークフローの信頼性向上における形式的検証の可能性を強調しています。
Lean4Agentは、表現力豊かな依存型形式言語を用いてエージェントの動作を形式的にモデル化・検証するという新分野の基盤を確立します。この研究はarXiv（番号2606.06523）に2026年6月2日に投稿され、Ruida Wangら6名の著者によるもので、人工知能、機械学習、計算機論理、ソフトウェア工学などの分野にまたがっています。