智能AI
morning
Lean4Agent：代理工作流程和轨迹的形式化建模和验证
2026-06-08
1 阅读
Ruida Wang, Jerry Huang, Pengcheng Wang, Xuanqing Liu, Luyang Kong, Tong Zhang
arXiv:2606.06523v1 发布类型：新 摘要：配备大型语言模型 (LLM) 来执行可靠的多步骤工作流程已成为人工智能领域的核心挑战。尽管法学硕士的代理能力最近取得了进展，但大多数代理系统仍然缺乏指定、验证和调试其工作流程和执行轨迹的正式方法。这一挑战反映了数学中一个长期存在的问题，即自然语言（NL）的歧义促进了形式语言（FL）的发展。受此范例的启发，据我们所知，我们提出 **Lean4Agent**，这是第一个使用 Lean4（一种依赖型 FL）来建模和验证代理行为的框架。 **Lean4Agent** 推出 **FormalAgentLib**，这是一个可扩展的 Lean4 库，用于在明确的假设下进行正式建模和验证代理工作流的语义一致性，并实现轨迹揭示的执行时故障的本地化。在**FormalAgentLib**的基础上，我们进一步开发**LeanEvolve**，它应用**FormalAgentLib**中的结果来修改工作流程以增强其能力。对 5 个领先的法学硕士的 SWE-Bench-Verified 的难题子集和 ELAIP-Bench 的子集进行的广泛实验表明，通过验证的工作流程比失败的工作流程平均性能提高 **11.94%**，而 **LeanEvolve** 进一步将 SWE 性能平均提高 **7.47%**。此外，**Lean4Agent** 为使用表达依赖型 FL 来正式建模和验证代理行为的新领域奠定了基础。