Lean4Agent 是研究者提出的一套全新框架，旨在用形式化方法为大型语言模型（LLM）的智能体行为建模与验证。该论文于 2026 年 6 月 2 日提交至 arXiv，编号为 arXiv:2606.06523v1，作者为 Ruida Wang 等共六人，隶属于人工智能（cs.AI）、机器学习（cs.LG）、计算机科学逻辑（cs.LO）与软件工程（cs.SE）等交叉领域。
论文指出了一个核心痛点：尽管 LLM 的智能体能力近来进步显著，能够执行多步骤工作流，但绝大多数智能体系统仍缺乏用于规定、验证和调试其工作流及执行轨迹的形式化手段。作者将这一困境类比为数学领域的长期问题——自然语言（NL）的歧义促使人们发展出形式语言（FL），受此启发，他们提出用 Lean4 这一依赖类型的形式语言来建模和验证智能体行为，并称 Lean4Agent 是首个此类框架。
在具体构成上，Lean4Agent 首先推出 FormalAgentLib，这是一个可扩展的 Lean4 库，能够在显式假设下对智能体工作流的语义一致性进行形式化建模与验证，并支持定位由执行轨迹暴露出的运行时失败。在此基础之上，研究团队进一步开发了 LeanEvolve，它利用 FormalAgentLib 中的验证结果来修订工作流，从而增强智能体的能力。
实验方面，作者在 SWE-Bench-Verified 的困难问题子集以及 ELAIP-Bench 的一个子集上，针对 5 个领先的 LLM 进行了评估。结果显示，通过验证的工作流平均比未通过验证的工作流表现高出 11.94%；而 LeanEvolve 进一步把 SWE 性能平均提升了 7.47%。这些数据表明，形式化验证结果与智能体实际表现之间存在可量化的关联。
论文还强调，Lean4Agent 为利用表达力强的依赖类型形式语言来形式化建模与验证智能体行为这一新领域奠定了基础，其意义不仅限于单一系统的性能提升，更在于为智能体的可靠性与可调试性提供了一套可复用的方法论框架。