arXiv cs.AI· Ruida Wang, Jerry Huang, Pengcheng Wang, Xuanqing Liu, Luyang Kong, Tong Zhang·· 12 小时前AI 评分39
Lean4Agent：用 Lean4 对智能体工作流与轨迹进行形式化建模与验证
Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
AI 导读
Lean4Agent 是首个用依赖类型形式语言 Lean4 建模并验证智能体行为的框架，包含可扩展的 Lean4 库 FormalAgentLib 和基于其修正工作流的 LeanEvolve。
正文 · AI 翻译
摘要：让大型语言模型（LLM）能够执行可靠的多步骤工作流，已成为人工智能领域的一项核心挑战。尽管 LLM 的智能体能力近期取得了进展，但大多数智能体系统仍缺乏用于指定、验证和调试其工作流与执行轨迹的形式化方法。这一挑战与数学领域一个长期存在的问题相呼应：自然语言（NL）的歧义性促使人们开发形式语言（FL）。受这一范式启发，我们提出了 **Lean4Agent**，据我们所知，这是首个使用依赖类型形式语言 Lean4 来建模和验证智能体行为的框架。**Lean4Agent** 推出了 **FormalAgentLib**，这是一个可扩展的 Lean4 库，用于在明确假设下对智能体工作流的语义一致性进行形式化建模与验证，并能够定位由轨迹揭示的执行时故障。在 **FormalAgentLib** 的基础上，我们进一步开发了 **LeanEvolve**，它应用 **FormalAgentLib** 中的结果来修订工作流，以增强其能力。在 SWE-Bench-Verified 的一个困难问题子集和 ELAIP-Bench 的一个子集上，针对 5 个领先 LLM 的大量实验表明，通过验证的工作流平均比未通过的工作流高出 **11.94%**，而 **LeanEvolve** 进一步将 SWE 性能平均提升了 **7.47%**。此外，**Lean4Agent** 为利用具有表达力的依赖类型形式语言对智能体行为进行形式化建模与验证这一新领域奠定了基础。
| 评论： | Nips 2026 接收论文 |
| 主题： | 人工智能（cs.AI）；机器学习（cs.LG）；计算机科学中的逻辑（cs.LO）；软件工程（cs.SE） |
| 引用为： | arXiv:2606.06523 [cs.AI] |
| （或本版本的 arXiv:2606.06523v3 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2606.06523 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Ruida Wang [查看邮箱]
[v1]
2026年6月2日星期二 18:46:50 UTC（542 KB）
[v2]
2026年6月15日星期一 18:24:02 UTC（542 KB）
[v3]
2026年10月20日星期二 22:43:41 UTC（525 KB）
来源：arXiv cs.AI · arxiv.org