Lean4Agent: 代理工作流与轨迹的形式化建模与验证

# Lean4Agent：智能体工作流与轨迹的形式化建模与验证
来源：https://arxiv.org/html/2606.06523 \\minted@def@optcl envname\-P envname\#1 amlblock\]YAMLbreaklines, fontsize= amlblockred\]YAMLbreaklines, fontsize=, bgcolor=diffredamlblockgreen\]YAMLbreaklines, fontsize=, bgcolor=diffgreen  
Ruida Wang¹, Jerry Huang¹, Pengcheng Wang¹, Xuanqing Liu², Luyang Kong², Tong Zhang¹  
¹伊利诺伊大学厄巴纳-香槟分校，²独立研究者  
\{ruidaw, jerry8, pw29\}@illinois.edu, [email protected], [email protected], [email protected]  

###### 摘要  
使大型语言模型（LLMs）能够执行可靠的多步工作流已成为人工智能的核心挑战。尽管LLMs的智能体能力近年来取得了进展，但大多数智能体系统仍缺乏用于规范、验证和调试其工作流及执行轨迹的形式化方法。这一挑战类似于数学中一个长期存在的问题：自然语言（NL）的歧义性推动了形式语言（FL）的发展。受此范式启发，我们提出了Lean4Agent——据我们所知，这是首个利用依赖类型形式语言Lean4来建模和验证智能体行为的框架。Lean4Agent推出了FormalAgentLib，一个可扩展的Lean4库，用于在显式假设下形式化建模和验证智能体工作流的语义一致性，并能够定位执行轨迹中暴露的运行时故障。在此基础上，我们进一步开发了LeanEvolve，它利用FormalAgentLib的结果来修订工作流以增强其能力。我们在SWE-Bench-Verified (Jimenez et al., 2024 (https://arxiv.org/html/2606.06523#bib.bib11)) 的困难子集和ELAIP-Bench (Dai et al., 2025 (https://arxiv.org/html/2606.06523#bib.bib6)) 的子集上，使用5种领先LLM进行了广泛实验。结果表明，通过验证的工作流平均比未通过的工作流性能提升11.94%，而LeanEvolve进一步将SWE性能平均提升7.47%。此外，Lean4Agent为使用表达能力强的依赖类型形式语言来形式化建模和验证智能体行为这一新领域奠定了基础。  

## 1 引言  
开发具有数学可证明性质的人工智能（AI）系统一直是计算机科学界的核心追求 (Seshia et al., 2022 (https://arxiv.org/html/2606.06523#bib.bib30))。随着LLMs智能体能力的快速发展，复杂的LLM智能体工作流正越来越多地部署在高风险领域 (Tran et al., 2025 (https://arxiv.org/html/2606.06523#bib.bib34))。这一趋势加强了对LLM智能体系统在工作流规范和轨迹执行层面进行形式化规范的需求。现有验证基于LLM系统的方法在范围和格式上仍显零散。早期方法，如LLM-as-judge (Zheng et al., 2023 (https://arxiv.org/html/2606.06523#bib.bib49))，评估模型的自然语言输出，但在长期执行中容易产生幻觉和过度自信 (Lin et al., 2025a (https://arxiv.org/html/2606.06523#bib.bib16))。最近的工作引入了形式化方法，包括用于验证工具调用的简单Hoare风格逻辑合约 (Liu et al., 2026 (https://arxiv.org/html/2606.06523#bib.bib19))、基于SMT的动作级策略验证 (Miculicich et al., 2025 (https://arxiv.org/html/2606.06523#bib.bib21))，以及对其工件进行时序逻辑检查 (Ramani et al., 2025 (https://arxiv.org/html/2606.06523#bib.bib27))。然而，每条工作线仅解决部分问题，且受到其底层形式语言表达能力的限制。时序逻辑语言无法建模数据依赖属性，而基于SMT的合约检查难以表达高阶推理。因此，据我们所知，现有工作尚未提供一个统一的框架来形式化建模和验证智能体工作流与轨迹。这两者对长期自主智能体都至关重要 (Wang et al., 2026 (https://arxiv.org/html/2606.06523#bib.bib36))。  

参见图注  
图1：Lean4Agent框架：Lean4Agent框架包含两个主要组件。(a) FormalAgentLib是一个三层Lean4库，用于形式化建模和验证智能体行为。第一层通过工作流图验证工作流的结构正确性。第二层开发谓词（pred.）系统来建模智能体执行的前置条件和后置条件，并利用LLMExec假设验证语义自一致性。第三层通过应用Lean、外部程序和LLM-as-judge检查执行轨迹，定位工作流中违反的步骤。(b) LeanEvolve利用验证结果来精炼工作流，并构建形式化引导的工作流演化，配合纯LLM演化附加组件以进一步增强其能力。  

现代纯数学中一直存在一个类似的挑战：大多数问题涉及证明没有数值答案的定理。由于自然语言天生具有歧义性，随着证明长度和复杂性的增加，验证复杂的数学论证变得越来越困难。为了解决这个问题，数学家和计算机科学家采用了依赖类型理论 (Martin-Löf and Sambin, 1984 (https://arxiv.org/html/2606.06523#bib.bib20)) 来形式化验证证明。这一范式催生了表达能力强的形式语言（FL），如Lean (De Moura et al., 2015 (https://arxiv.org/html/2606.06523#bib.bib7); Moura and Ullrich, 2021 (https://arxiv.org/html/2606.06523#bib.bib22)) 和Coq (Coq, 1996 (https://arxiv.org/html/2606.06523#bib.bib5))，以及针对它们的LLM工具。尽管形式语言在数学上取得了成功，但在统一建模和验证LLM智能体系统方面的应用仍研究不足。为应对这些挑战，我们提出了Lean4Agent——据我们所知，这是首个使用依赖类型形式语言来统一建模、验证和精炼智能体系统的框架。 Lean4Agent的概述见图1 (https://arxiv.org/html/2606.06523#S1.F1)。 Lean4Agent推出了FormalAgentLib，一个可扩展的三层Lean4库，用于在三个正确性级别上形式化建模和验证智能体工作流与轨迹：结构正确性、语义正确性和运行时轨迹正确性。第一层验证智能体工作流的结构良好性，类似于程序的编译器级检查。第二层开发了一个依赖类型谓词系统，用于指定各个执行步骤的前置条件和后置条件。它还使我们能够统一建模分支、循环和子模块组合行为。借助LLMExec——对LLM局部正确性的假设，我们能够自动化静态语义正确性的证明，同时可扩展到新领域。这是通过类型匹配、Hoare逻辑推理以及FormalAgentLib所证明的辅助定理来实现的。该层允许工作流规范在部署前在假设下进行形式化验证，支持正确性通过构造的工作流设计 (Seshia et al., 2022 (https://arxiv.org/html/2606.06523#bib.bib30))。第三层使用经过验证的工作流，借助LLM检查执行轨迹，确定步骤级前置条件和后置条件是否满足，并定位导致失败的执行步骤。基于FormalAgentLib，我们进一步提出了LeanEvolve，一种由轨迹验证和可选环境反馈驱动的运行时工作流精炼方法。 LeanEvolve利用LLM和FormalAgentLib的验证结果来识别当前工作流中的缺陷并修订规范，从而提高工作流性能。我们将Lean4Agent的贡献总结如下：(1) 我们推出了FormalAgentLib——据我们所知，这是首个可扩展的Lean4库，用于在显式假设下形式化建模和验证智能体工作流的语义一致性，并能够定位轨迹所揭示的故障。(2) 基于FormalAgentLib，我们提出了LeanEvolve，一种形式化引导的工作流演化方法，利用验证反馈和可选环境信号来精炼智能体工作流。(3) 我们通过软件工程（SWE）任务（使用SWE-Bench-Verified (Jimenez et al., 2024 (https://arxiv.org/html/2606.06523#bib.bib11)) 的困难子集）和AI论文理解任务（使用ELAIP-Bench (Dai et al., 2025 (https://arxiv.org/html/2606.06523#bib.bib6)) 的子集）在五种领先LLM上进行了广泛实验，以评估Lean4Agent。与未通过验证的工作流相比，FormalAgentLib验证过的工作流在SWE任务上平均提升14.80%，在ELAIP-Bench子集上平均提升9.07%。通过LeanEvolve，验证过的工作流在SWE任务上进一步平均提升7.47%。这一统计显著的改进证明了Lean4Agent工作流验证的有用性及其精炼方法的有效性。广义上讲，Lean4Agent为可验证的LLM智能体系统提供了坚实统一的基础，并为训练和开发自我改进的LLM智能体开辟了未来方向。它还提供了为长期黑盒系统建模的原则。为了支持该领域的进一步发展，我们将在近期于https://github.com/RickySkywalker/Lean4Agent开源代码。  

## 2 方法论  
本节介绍Lean4Agent框架的设计。目标是为在显式假设下建模和验证智能体工作流与轨迹提供形式化基础，并利用形式化指导来改进工作流设计。第2.1节 (https://arxiv.org/html/2606.06523#S2.SS1) 介绍关键预备知识，第2.2节 (https://arxiv.org/html/2606.06523#S2.SS2) 描述FormalAgentLib的设计，第2.3节 (https://arxiv.org/html/2606.06523#S2.SS3) 介绍LeanEvolve方法。  

### 2.1 预备知识  
我们定义本文使用的三个核心概念如下：  
LLM智能体：遵循ReAct (Yao et al., 2022 (https://arxiv.org/html/2606.06523#bib.bib44))，我们将LLM智能体定义为能够执行推理-行动循环的模型，该模型将内部推理与任务特定行动交错进行。推理使模型能够制定、跟踪和修订计划，而行动则允许模型与外部工具或信息源交互。  
智能体工作流：我们将智能体工作流定义为LLM智能体如何接近任务的显式、结构化的规范。形式上，我们将工作流表示为一个异构图 G:=⟨V,E⟩，其中 V:=\{v_i\}_{i=1}^n 是执行节点集，E⊆V×V 是转移集。每个节点表示为 v_i:=⟨r_i, w_i, t_i, τ_i⟩，其中 r_i 和 w_i 是节点读取和写入的变量集，t_i 是自然语言（NL）指令，τ_i 是其执行类型。在我们的实现中，我们使用AgentSPEX (Wang et al., 2026 (https://arxiv.org/html/2606.06523#bib.bib36)) 提供的YAML工作流格式，因为它为执行步骤和转移提供了清晰的类型系统。然而，我们的公式化可以基于控制流图基础适应于通用工作流规范。  
执行轨迹：我们将执行轨迹定义为LLM智能体在工作流上运行时产生的实际展开。它可以看作是 G 上的一个带值路径，形式化为 T:=s_0→s_1→⋯→s_l，其中 s_i:=⟨pre_i, v_{j_i}, gen_i, pos_i⟩，pre_i 和 pos_i 是执行前和执行后的状态，v_{j_i}∈V 是在该转移处执行的工作流节点，gen_i 记录单个ReAct风格步骤的LLM推理和工具调用踪迹。  

### 2.2 FormalAgentLib  
我们现在详细介绍FormalAgentLib的设计，这是一个可扩展的Lean4库，用于统一建模和验证LLM智能体工作流与轨迹。据我们所知，这是首次尝试使用表达能力强的依赖类型形式语言来验证智能体行为。FormalAgentLib组织为三个互补层：结构验证（第2.2.1节 (https://arxiv.org/html/2606.06523#S2.SS2.SSS1)）、语义验证（第2.2.2节 (https://arxiv.org/html/2606.06523#S2.SS2.SSS2)）和轨迹级分析（第2.2.3节 (https://arxiv.org/html/2606.06523#S2.SS2.SSS3)）。  

#### 2.2.1 第一层：结构验证  
该层为验证智能体工作流中独立于LLM的结构属性提供了基础。它定义了变量、执行节点和图转移的基本类型系统，从而能够验证工作流的结构良好性。由于篇幅限制，完整定义见附录B.1 (https://arxiv.org/html/2606.06523#A2.SS1)。我们首先通过定义工作流变量的数据类型来构建该层。具体来说，我们引入了Lean归纳类型BaseType，并按照Siek和Taha (2006 (https://arxiv.org/html/2606.06523#bib.bib31))；Flanagan (2006 (https://arxiv.org/html/2606.06523#bib.bib10))的思想实现了兼容关系。我们进一步定义了StepType，一个用于建模不同类型执行节点的归纳类型。其中，step和task最为核心：step执行带有对话历史的LLM查询，而task则在没有历史的情况下执行。BaseType和StepType共同定义了WorkflowNode，即智能体步骤的Lean建模。对于节点 v_i=⟨r_i, w_i, t_i, τ_i⟩，我们表示 r_i=\{r_{ij}\}_{j=1}^{|r_i|}，w_i=\{w_{ij}\}_{j=1}^{|w_i|}，其中 r_{ij}, w_{ij} 是类型化变量，τ_i:StepType。我们接下来定义WorkflowEdge来建模节点转移模式，包括顺序执行、分支和循环。利用这些基础类型，我们形式化地将智能体工作流建模为：W=(V,E,v_entry,X,P)，其中 V 和 E 是类型化节点和边的有限集合，v_entry∈V 是入口节点，X⊆V 表示出口节点，P 是表示上下文中初始参数的类型化变量列表。第一层建模支持结构验证，例如节点可达性、边有效性和读写一致性，类似于程序编译级别的简单验证。例如，当节点读取的变量既不是初始参数也不是可达前驱产生的变量时，我们可以检测到读取不一致。附录B.1.6 (https://arxiv.org/html/2606.06523#A2.SS1.SSS6)提供了此类错误的详细示例。  

#### 2.2.2 第二层：智能体工作流的静态语义验证  
第二层对智能体工作流在关于局部LLM正确性的显式假设下建模和验证静态语义正确性。为此，我们引入了一个基于谓词的语义验证系统，包含三个组件：一个谓词系统，用于形式化建模显式和隐式变量的语义属性；一个语义工作流图，将这些谓词组织在工作流中；以及一个验证过程，用于验证每一步的前置条件是否由先前建立的谓词蕴含。由于篇幅限制，完整的正式细节见附录B.2 (https://a