**Lean4Agent：使用依赖类型形式语言对智能体工作流与轨迹进行形式化建模与验证**

_Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory_

> Lean4Agent 是首个利用 Lean4 这一依赖类型形式语言对智能体行为进行建模与验证的框架。它推出了 FormalAgentLib，一个可扩展的 Lean4 库，用于在显式假设下形式化建模和验证智能体工作流的语义一致性，并能定位执行失败的原因。在此基础上，LeanEvolve 进一步利用验证结果修订工作流以提升能力。在 SWE-Bench-Verified 和 ELAIP-Bench 的困难子集上针对 5 个主流 LLM 的广泛实验表明，通过验证的工作流平均性能比未通过验证的高出 11.94%，而 LeanEvolve 平均将 SWE 性能再提升 7.47%。该工作为使用表达性依赖类型形式语言来形式化建模和验证智能体行为的新领域奠定了基础。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：ai-models
- **发布时间**：2026-06-09 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2606.06523)