基于合约的LLM代理符号时间监督

# 使用契约对LLM智能体进行符号化时序监督
来源：https://arxiv.org/html/2609.18128
###### 摘要

大型语言模型（\(LLM\)）智能体通过工具增强，能够通过工具调用作用于外部系统，从而自动化复杂的多步骤任务，如网页导航、代码生成和工作流编排。然而，LLM中的幻觉、分布不稳定性以及对抗性攻击，加之某些工具调用的不可逆后果，可能导致有害结果。现有的防护措施要么使用随机的LLM评判器对记录轨迹进行事后评分，要么逐次阻止不安全的操作，没有单一的确定性构件能同时履行这两种角色。我们提出了ContrAgent{\mathsf{ContrAgent}}，一个基于契约的框架，用于对LLM智能体进行符号化时序监督。ContrAgent{\mathsf{ContrAgent}}将智能体的行为捕获为工具调用序列，并将其形式化为在固定可检查谓词集上的迹。随后，它使用有限迹上的线性时序逻辑（\(LTLf\)）中的假设-保证（A/G）契约来规定所需行为。每个契约被编译为一个确定性有限自动机（\(DFA\)），该自动机同时扮演两个角色：在线上对智能体操作进行把关，在线下评估已记录的迹。一个作为可重用知识库的契约库独立于智能体模型维护，并可应用于同一任务领域内的不同智能体。我们在涵盖这两个角色的四个基准测试中展示了我们方法的有效性，其中ContrAgent{\mathsf{ContrAgent}}在性能上与最先进的LLM评判器和基于规则的护栏基线相匹配，同时能产生确定性、可复现的判定，并且在在线模式下，单次调用延迟降低了几个数量级。

1加州大学伯克利分校电气工程与计算机科学系，美国加州伯克利

\{yifeng\_xiao, pierluigi\.nuzzo\}@berkeley\.edu

## 1引言

最近的工具增强大型语言模型（\(LLM\)）智能体能够在现实领域自动化复杂的多步骤任务，包括网页导航\(Zhou et al\. 2024 (https://arxiv.org/html/2609.18128#bib.bib56)\)、代码生成\(Jimenez et al\. 2024 (https://arxiv.org/html/2609.18128#bib.bib23)\)和工作流编排\(Wu et al\. 2024 (https://arxiv.org/html/2609.18128#bib.bib46)\)。诸如OpenClaw\(OpenClaw Project 2026 (https://arxiv.org/html/2609.18128#bib.bib33)\)、HermesAgent\(Nous Research 2026 (https://arxiv.org/html/2609.18128#bib.bib30)\)和LangChain\(Chase 2022 (https://arxiv.org/html/2609.18128#bib.bib10)\)等智能体框架通过工具调用接口实现这些能力，范围从shell命令到应用程序编程接口（\(API\)）调用，以及如模型上下文协议（\(MCP\)）\(Anthropic 2024 (https://arxiv.org/html/2609.18128#bib.bib2)\)等协议。这些接口允许智能体作用于外部系统，但也引入了安全风险：LLM的幻觉和分布不稳定性，结合可能的对抗性攻击和工具调用的不可逆后果，可能导致有害结果。这些故障模式包括间接提示注入、性能压力下的指标博弈、危险代码执行以及委托智能体之间的身份混淆\(Sotiropoulos et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib41)\)。

一些方法使用LLM评判器或学习到的检测器对记录的轨迹进行事后评分\(Zheng et al\. 2023 (https://arxiv.org/html/2609.18128#bib.bib54);Sharma, Barke, and Zorn 2026 (https://arxiv.org/html/2609.18128#bib.bib39);Wen et al\. 2026 (https://arxiv.org/html/2609.18128#bib.bib45)\)，但其判定是随机的且难以复现。而强制机制则实时阻止不安全操作，但它们孤立地判断每个动作，忽略了跨越轨迹的属性\(Wang, Poskitt, and Sun 2026 (https://arxiv.org/html/2609.18128#bib.bib43);Inan et al\. 2023 (https://arxiv.org/html/2609.18128#bib.bib22)\)，关注的是语义意图而非工具调用行为\(Kamath et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib24);Miculicich et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib29)\)，或者依赖于特定智能体的模型\(Wang et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib44)\)。没有单一的确定性构件既能在线守护智能体，又能离线评估记录的轨迹。

参见标题图1：ContrAgent{\mathsf{ContrAgent}}监控LLM智能体与其工具之间的工具调用接口。受假设-保证（A/G）契约式设计\(Benveniste et al\. 2018 (https://arxiv.org/html/2609.18128#bib.bib8);Nuzzo et al\. 2015 (https://arxiv.org/html/2609.18128#bib.bib32)\)的启发，其组合推理已被应用于信息物理系统\(Xiao et al\. 2024 (https://arxiv.org/html/2609.18128#bib.bib49);Xiao and Nuzzo 2026 (https://arxiv.org/html/2609.18128#bib.bib48);Xiao et al\. 2026 (https://arxiv.org/html/2609.18128#bib.bib47)\)，我们提出了ContrAgent{\mathsf{ContrAgent}}，一个基于契约的、与模型无关的、确定性的框架，用于对LLM智能体进行符号化时序监督。我们将轨迹级需求形式化为在线性时序逻辑有限迹（\(LTLf\)）\(De Giacomo and Vardi 2013 (https://arxiv.org/html/2609.18128#bib.bib15)\)上的A/G契约，该逻辑基于可检查的原子命题（\(AP\)）作用于智能体操作。契约被编译为确定性有限自动机（\(DFA\)）检查器，通过在线上把关智能体操作（如图1所示 (https://arxiv.org/html/2609.18128#S1.F1)）或在线下评估记录的迹来监督智能体的轨迹。我们的贡献可总结如下：
- • 我们引入了A/G契约作为LLM智能体意图需求的形式化规范，使用一组可检查的工具调用迹上的原子命题（AP）形成契约库。
- • 我们提出了ContrAgent{\mathsf{ContrAgent}}，一个与模型无关的、确定性的LLM智能体监督框架，使用契约同时在线上保护智能体和线下对其轨迹进行评分。
- • 我们在涵盖两个角色的四个基准测试中评估了ContrAgent{\mathsf{ContrAgent}}，表明其在性能上与强大的LLM评判器和护栏基线相匹配，同时将单次调用延迟降低了几个数量级，并提供了确定性、可复现的已记录迹评估器。

论文其余部分组织如下：在第2节讨论相关工作后，我们在第3节提供智能体框架、LTLf和A/G契约的背景知识。第4节介绍交互谓词和智能体契约，第5节详细说明契约编译和基于契约的监督。第6节报告四个基准测试的结果，最后第7节给出结论性评述。

## 2相关工作

大多数针对LLM智能体基于工具运行的运行时安全措施作用在工具调用边界。诸如AgentSpec \(Wang, Poskitt, and Sun 2026 (https://arxiv.org/html/2609.18128#bib.bib43)\)之类的逐操作规则语言会根据一组规则检查每个提议的调用。它们快速且确定，但范围仅限于单个动作，而非对轨迹的动作顺序、历史或计数进行推理。另一条信息流工作线跟踪执行过程中的数据和权限，以阻止提示注入和数据窃取，例如Progent \(Shi et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib40)\)、CaMeL \(Debenedetti et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib17)\)、RTBAS \(Zhong et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib55)\)和Fides \(Costa et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib14)\)。然而，这条工作线中考虑的威胁模型与ContrAgent{\mathsf{ContrAgent}}的契约是正交的。

另一类方法使用逻辑来推理执行迹：Agent-C \(Kamath et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib24)\)在生成过程中使用可满足性模理论（SMT）求解来检查时序约束，VeriGuard \(Miculicich et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib29)\)使用LLM生成策略代码并在使用前进行形式化验证，而FORGE \(Palumbo et al\. 2026 (https://arxiv.org/html/2609.18128#bib.bib34)\)将确定性的Datalog策略编织到多智能体部署中。然而，它们都没有在整个轨迹上维护符号化的判定。Safety Chip \(Yang et al\. 2024 (https://arxiv.org/html/2609.18128#bib.bib51)\)将命题线性时序逻辑（\(LTL\)）编译为遮罩具身机器人智能体不安全操作的掩码，而ContrAgent{\mathsf{ContrAgent}}则使用基于可检查AP的A/G契约来监督通用的工具调用LLM智能体。

另一类方法旨在使用学习模型或LLM评判器对行为进行评分或保护。LLM即评判器评分器\(Zheng et al\. 2023 (https://arxiv.org/html/2609.18128#bib.bib54)\)、AgentPex \(Sharma, Barke, and Zorn 2026 (https://arxiv.org/html/2609.18128#bib.bib39)\)以及学习到的检测器如PolicyGuard \(Wen et al\. 2026 (https://arxiv.org/html/2609.18128#bib.bib45)\)对记录的轨迹进行评分，但其判定是随机的且难以复现，尤其是在安全判断上\(Chen and Goldfarb\-Tarrant 2025 (https://arxiv.org/html/2609.18128#bib.bib11)\)。ShieldAgent \(Chen, Kang, and Li 2025 (https://arxiv.org/html/2609.18128#bib.bib12)\)将策略文档编译为基于动作的概率规则电路，ABC \(Bhardwaj 2026 (https://arxiv.org/html/2609.18128#bib.bib9)\)在概率满足关系下强制执行行为契约，ProbGuard \(Wang et al\. 2025 (https://arxiv.org/html/2609.18128#bib.bib44)\)通过对学习到的智能体模型进行概率模型检查来预测违规，因此它们的判定是概率性的，并未用于确定性地阻止不良行为。

## 3预备知识

由于我们旨在使用A/G契约监督智能体的工具调用，我们首先提供智能体框架和时序逻辑的背景知识，然后陈述监督问题。

### 3.1智能体框架

一个智能体将LLM骨干与工具集配对，发出工具调用，并将它们的输出折叠到推理循环中，直到任务完成\(Yao et al\. 2023 (https://arxiv.org/html/2609.18128#bib.bib52)\)。*工具调用接口*是框架向智能体暴露的工具集合，连同它们的调用和返回约定。推理步骤承载智能体的决策过程，但它们仅通过发出的工具调用对现实世界产生影响，本文针对的不可逆后果类别正是在此接口处产生。因此，ContrAgent{\mathsf{ContrAgent}}跟踪*工具调用迹*，即智能体发出的工具调用事件的有序序列，这通常是一个长期、多工具的轨迹\(Xu et al\. 2026 (https://arxiv.org/html/2609.18128#bib.bib50)\)。

###### 定义 1（智能体会话）

令\(\Sigma\)表示有限的工具调用*事件*集。每个工具调用产生两个事件：一个*调用*事件\(a=(\mathsf{tool},\mathsf{args})\)（当智能体发出调用时），和一个*返回*事件\(a^{\prime}=(\mathsf{tool},\mathsf{result})\)（当执行的工具返回时）。智能体的执行是一个转移系统\(Baier and Katoen 2008 (https://arxiv.org/html/2609.18128#bib.bib3)\)\(\mathcal{T}=(S,s_{0},\Sigma,R)\)。状态\(s=(\tau,\kappa,\rho)\in S\)包括迄今为止发出的事件迹\(\tau\in\Sigma^{*}\)、一个从上下文键到从早期事件记录的值的有限映射\(\kappa\)、以及一个数值会话计数器向量\(\rho\)，初始状态\(s_{0}=(\varepsilon,\kappa_{0},\rho_{0})\)。每个事件\(a\)诱导一个转移\((s,a,s^{\prime})\in R\)，该转移将\(a\)追加到\(\tau\)并更新\(\kappa\)和\(\rho\)。一个智能体*会话*是一条有限路径\(s_{0}\xrightarrow{a_{1}}\cdots\xrightarrow{a_{k}}s_{k}\)，其迹为\(\tau=a_{1}\cdots a_{k}\)。

上下文键记录跨越事件的事实，例如调用者的身份或文档的来源，而计数器跟踪累积量，例如消耗的令牌数。

### 3.2有限迹LTL（LTLf）

LTL \(Pnueli 1977 (https://arxiv.org/html/2609.18128#bib.bib35)\)扩展了命题逻辑，用于对命题解释的无限序列或*迹*进行推理。LTLf \(De Giacomo and Vardi 2013 (https://arxiv.org/html/2609.18128#bib.bib15)\)将此逻辑限制为有限迹。令\(AP\)为有限原子命题集。LTLf公式在\(AP\)上的类别由语法\(\varphi::=P\mid\neg\varphi\mid\varphi\wedge\varphi^{\prime}\mid X\,\varphi\mid F\,\varphi\mid G\,\varphi\mid\varphi\,U\,\varphi^{\prime}\)定义，其中\(P\in AP\)是AP，\(\varphi^{\prime}\)是LTLf公式，包含时序运算符X（下一个）、F（最终）、G（总是）和U（直到）。每个LTLf公式可被编译为等价的DFA，该DFA恰好接受满足该公式的迹\(De Giacomo and Vardi 2013 (https://arxiv.org/html/2609.18128#bib.bib15)\)，这是运行时验证的规范监控器构造\(Bauer, Leucker, and Schallhart 2011 (https://arxiv.org/html/2609.18128#bib.bib6);Leucker and Schallhart 2009 (https://arxiv.org/html/2609.18128#bib.bib25)\)。

当原子谓词用于比较从会话状态\(s\)读取的算术量（例如在\(\rho\)中累积的调用计数或令牌总数，或锁定在\(\kappa\)中的参数值）与界限时，它更适合用线性算术约束而非普通命题来捕获。此时，此类原子上的LTLf公式取模线性算术，即算术LTLf（ALTLf）\(Felli et al\. 2023 (https://arxiv.org/html/2609.18128#bib.bib19)\)，这是LTLf取模理论\(Geatti, Gianola, and Gigante 2022 (https://arxiv.org/html/2609.18128#bib.bib20)\)的一个实例。ContrAgent{\mathsf{ContrAgent}}*逐点*评估每个原子，即其在每个事件上的真值是从当前事件\(a\)和会话状态\(s\)计算得出的。

### 3.3假设-保证（A/G）契约

令\(M\)表示一个组件，即系统的元素，由一组变量\(V_{c}\)和一组在\(V_{c}\)上的行为\(\llbracket M\rrbracket\)表征。一个契约\(C\)使用三元组\(C=(V_{c},A,G)\)正式捕获组件\(M\)的一组规范\(Benveniste et al\. 2018 (https://arxiv.org/html/2609.18128#bib.bib8)\)，其中\(A\)和\(G\)是在\(V_{c}\)上的行为集。\(A\)是对\(M\)环境的假设，\(G\)是\(M\)在假设满足条件下提供的保证。我们说\(M\)是\(C\)的有效实现，即\(M\models C\)，如果给定\(C\)的假设，\(M\)的所有行为都包含在保证中，即\(\llbracket M\rrbracket\subseteq G\cup\overline{A}\)。我们说组件\(E_{c}\)是\(C\)的有效环境，如果\(E_{c}\)的所有行为都包含在\(C\)的假设中。一个契约是*一致的*当且仅当存在一个有效实现，即\(G\cup\overline{A}\neq\emptyset\)，并且是*可兼容的*当存在一个有效环境\(E_{c}\)，即\(A\neq\emptyset\)。

ContrAgent{\mathsf{ContrAgent}}形式化了智能体工具调用迹上的契约：组件是智能体，其行为\(\llbracket M\rrbracket\)是其可能产生的工具调用迹（定义1 (https://arxiv.org/html/2609.18128#Thmmydefinition1)），变量\(V_{c}\)是集合\(AP\)。在运行时，会话暴露该组件的一个行为，ContrAgent{\mathsf{ContrAgent}}评估