Lean4Agent：面向智能体工作流与轨迹的形式建模与验证

摘要

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

Lean4Agent：面向智能体工作流与轨迹的形式建模与验证：论文配图 — 图 1：Lean4Agent 框架：Lean4Agent 框架由两个主要组件组成。 (a) FormalAgentLib 是一个三层 Lean4 库，用于形式化建模和验证代理行为。第一层通过工作流图验证工作流的结构正确性。第 2 层开发了一个谓词 (pred.) 系统来对代理执行的前置条件和后置条件进行建模，并使用 LLMExec 假设验证语义自一致性。第三层通过应用Lean、外部程序和LLM作为法官来检查执行轨迹，定位工作流程中的违规步骤。 (b) LeanEvolve 使用验证结果来完善工作流程，并使用 pure-LLM evolve 插件构建形式化指导的工作流程演进，以进一步增强其功能。