Lean4Agent：面向智能体工作流与轨迹的形式化建模与验证
本文提出Lean4Agent，据我们所知，这是首个使用依赖类型形式语言Lean4来建模和验证大语言模型智能体行为的框架。它包含FormalAgentLib库和LeanEvolve优化工具，实验表明通过验证的工作流性能平均提升11.94%，LeanEvolve进一步将软件工程任务性能提升7.47%。
近年来，大语言模型（LLM）在多步工作流执行中的可靠性成为人工智能领域的核心挑战。尽管LLM的智能体能力不断进步，但大多数智能体系统仍缺乏用于指定、验证和调试工作流及执行轨迹的形式化方法。这一困境与数学中长期存在的问题相似——自然语言的歧义性推动了形式语言的发展。受此启发，来自多所机构的研究人员提出了Lean4Agent，据我们所知，这是首个使用依赖类型形式语言Lean4来建模和验证智能体行为的框架。
Lean4Agent的核心组件是FormalAgentLib，这是一个可扩展的Lean4库，能够对智能体工作流进行形式化建模，并在显式假设下验证其语义一致性。更重要的是，该库可以定位执行轨迹中揭示的运行时故障，为开发者提供清晰的调试方向。基于FormalAgentLib，研究团队进一步开发了LeanEvolve，该工具利用验证结果自动修订工作流，从而增强智能体的整体能力。
为了评估Lean4Agent的有效性，研究者在SWE-Bench-Verified的困难子集和ELAIP-Bench子集上进行了大量实验，涉及5种主流LLM，包括GPT-4、Claude等。结果显示，通过形式化验证的工作流相比未通过的版本性能平均高出11.94%。此外，应用LeanEvolve进行工作流修订后，软件工程任务（SWE）性能平均进一步提升7.47%。这些数据充分证明了形式化方法在智能体工作流优化中的巨大潜力。
Lean4Agent的提出为使用表达能力丰富的依赖类型形式语言来形式化建模和验证智能体行为奠定了坚实基础，开辟了一个全新的研究方向。未来，这一框架有望被扩展以处理更复杂的多智能体协作场景，并与其他形式化工具集成，从而推动可靠AI系统的构建。该论文于2026年6月2日提交至arXiv，标志着依赖类型形式语言在AI智能体验证领域的重要突破。