Skip to main content
2026arXiv 2512.23738

Agent-C：为 LLM Agent 执行时序安全约束

Enforcing Temporal Constraints for LLM Agents

Agent-C 提出了一种运行时框架，通过 DSL 表达时序安全属性、翻译为一阶逻辑并用 SMT 求解器检查，在 LLM 生成 token 的过程中实时执行约束。在 τ-bench 基准上实现 100% 合规率和 0% 伤害率，同时提升任务效用。

Adharsh Kamath, Sishen Zhang, Calvin Xu, Shubham Ugare, Gagandeep Singh, Sasa Misailovic
AI解读Agent 规范与安全Agent 架构设计Temporal ConstraintsSMT SolvingConstrained GenerationRuntime Monitoring

论文概览

LLM Agent 在安全关键场景中的部署面临一个根本性挑战：现有护栏系统无法有效防止时序安全策略的违反。这类策略要求推理动作的顺序和时序——例如"访问敏感数据前必须先认证用户"或"退款必须退回原始支付方式"——而不是单条动作的合法性。现有的护栏要么依赖不精确的自然语言指令，要么只能做事后监控，无法提供形式化保证。

Agent-C 由 UIUC 的研究团队提出，将形式化验证原理引入 LLM Agent 的运行时监控。其核心思路是：对 LLM 生成的工具调用施加结构化约束，并在 token 生成过程中通过 SMT 求解器实时检查合规性。框架提供了一个领域特定语言（DSL）来表达时序属性，将其翻译为一阶逻辑公式，利用 Z3 求解器增量检查，并通过约束生成技术确保每个生成的动作都满足规范。

在标准 τ-bench 基准上，Agent-C 在所有模型和场景中实现了 100% 合规率和 0% 伤害率，同时在大多数情况下提升了任务效用——例如在零售场景中，Qwen3-32B 的效用从无约束的 25.52% 提升至 53.31%，Claude Sonnet 4.5 从 76.52% 提升至 80.46%。

核心创新

1. 时序约束 DSL 与 FOL 翻译

Agent-C 的 DSL 包含五个核心谓词，能够表达工具调用之间的时序关系和状态依赖：

谓词语义示例
Before(P, φ₁, P', φ₂)调用 P 前必须曾调用 P'Before(read(f1), True, open(f2), f1==f2)
After(P, φ₁, P', φ₂)调用 P 后必须再调用 P'After(open(f1), True, close(f2), f1==f2)
Seq(P, φ₁, P', φ₂)P 后必须存在 P' 的调用序列Seq(use(r1), r1=="123", dispose(r2), r1==r2)
Forall(P, φ)P 的每次调用都满足 φForall(rm(p), p!="/root")
Exists(P, φ)至少存在一次 P 调用满足 φExists(create(r), r=="456")

Agent-C DSL 谓词语义与 FOL 翻译
Agent-C DSL 谓词语义与 FOL 翻译

DSL 还支持 state() 语法来查询工具运行时状态（如检查订单的支付方式是否匹配），以及 output() 来引用历史工具调用的输出。这些谓词通过合取、析取和否定进行组合，表达能力覆盖了一阶线性时序逻辑（FLTL）的一个无 Next 片段。

规范到 FOL 的翻译遵循明确的语义规则。例如，Before(P, φ₁, P', φ₂) 翻译为：

∀t.(Tt=P∧⟦ϕ1⟧τ[x↦xt])⇒∃t′.t′<t∧Tt′=P′∧⟦ϕ2⟧τ[x′↦xt′,x↦xt,y′↦yt′]\forall t. (T_t = P \land \llbracket \phi_1 \rrbracket_{\tau}[x \mapsto x_t]) \Rightarrow \exists t'. t' < t \land T_{t'} = P' \land \llbracket \phi_2 \rrbracket_{\tau}[x' \mapsto x_{t'}, x \mapsto x_t, y' \mapsto y_{t'}]

2. Safe-LLM 合规生成算法

Agent-C 的核心是 Safe-LLM 算法，它在 LLM 生成 token 的过程中实时检查合规性。算法维护一个轨迹（trace），记录每次工具调用的输入、输出和状态投影。当 LLM 尝试生成一个工具调用时，Agent-C 将该调用附加到轨迹上，编码为 FOL 公式并用 Z3 检查可满足性。

Agent-C 系统架构
Agent-C 系统架构

针对不同模型类型，Agent-C 提供两种生成策略：

  • Gen-Call（开权重模型）：利用约束生成框架的回溯能力，在 token 级别进行细粒度控制。当某个参数导致违规时，可以只回溯该参数的生成，而保留之前已生成的部分。这大幅减少了 token 消耗——相比 Reprompt 方式，输入 token 减少最多 40%，输出 token 减少最多 54%。

  • Gen-Call-Reprompt（闭源模型）：由于商业 LLM 提供商不暴露完整的 token 概率分布，采用更粗粒度的重新提示策略。每次发现违规时，将错误信息反馈给 LLM 并重新生成完整的工具调用。

两种算法都保证了形式化的合规性：只有当 SMT 求解器返回 SAT（可满足）时，工具调用才被允许执行。

3. 形式化执行保证

Agent-C 提供了两个关键定理：

定理 2（可靠性）：给定满足规范的轨迹 τ，如果 Safe-LLM 返回一个工具调用，则将此调用附加到 τ 后的新轨迹 τ' 仍然满足规范。

τ⊢Ψ∧Safe-LLM(…)=(Tool,(P0,x0,σ0))⇒(τ::(P0,x0,σ0))⊢Ψ\tau \vdash \Psi \land \text{Safe-LLM}(\ldots) = (\text{Tool}, (P_0, x_0, \sigma_0)) \Rightarrow (\tau :: (P_0, x_0, \sigma_0)) \vdash \Psi

定理 3（合规执行）：每次以 Endsafe 终止的执行都是合规执行。

合规性的核心定义是：轨迹 τ 满足规范 Ψ，当且仅当公式 ⟦τ⟧T⇒¬⟦Ψ⟧\llbracket \tau \rrbracket_T \Rightarrow \neg \llbracket \Psi \rrbracket 在一阶逻辑中有效（等价于 ⟦τ⟧T∧⟦Ψ⟧\llbracket \tau \rrbracket_T \land \llbracket \Psi \rrbracket 不可满足）。

方法论详解

形式化模型

Agent-C 将 Agent 系统建模为元组 Sˉ=(C,T,R,QT,Ψ)\bar{S} = (C, T, R, Q_T, \Psi)，其中 C 是受约束的 LLM，T 是工具运行器，R 是运行时，QTQ_T 是状态投影映射，Ψ\Psi 是形式化规范。

系统执行通过六条转换规则推进：Infer-AgC（调用 Safe-LLM）、Invoke-AgC（生成工具调用）、Execute-AgC（执行工具）、Feedback-AgC（反馈结果）、Terminate-AgC（正常终止）、Terminate-Err-AgC（错误终止）。每次工具调用被编码为一个事件 E=(P,x,σ0,Tout)E = (P, x, \sigma_0, T_{out})，记录工具名、输入参数、状态投影和输出。

状态投影机制

Agent-C 通过状态投影函数 Qi:TS×Arg→ValQ_i: T_S \times \text{Arg} \to \text{Val} 来读取工具状态，而不直接操作状态。例如 payment_method_same(order_id, payment) 检查给定订单的原始支付方式是否与提供的退款方式匹配。这种设计使 Agent-C 能与多种底层存储机制（内存数据库、分布式数据库等）协作，同时保持规范的纯净性。

增量求解

Agent-C 利用 Z3 的增量求解特性，复用之前求解过程中的证明信息，避免每次从零开始约束求解。这在实践中显著降低了运行时开销——在良性场景中仅比 AgentSpec 慢 17%，比无约束 Agent 慢 44%。

实验结果

RQ1：开权重模型性能

在 τ-bench 的零售和航空场景中，Agent-C 与三种基线对比：

模型框架零售合规率零售效用航空合规率航空效用
Qwen3-32BAgent-C100%53.31%100%35.83%
Qwen3-32BAgentSpec84.06%37.39%79.33%38.67%
Qwen3-32BDynaGuard77.10%9.57%69.39%17.01%
Qwen3-32BUnrestricted37.69%25.52%35.33%17.33%

实验结果对比
实验结果对比

Agent-C 在所有配置下实现 100% 合规和 0% 伤害，同时效用显著高于基线。值得注意的是，DynaGuard 虽然是安全导向的护栏，但在对抗场景中仍出现了高达 19.61% 的伤害率——它无法可靠地推理时序约束，导致泄露用户订单信息甚至允许取消他人预订。

RQ2：闭源前沿模型

模型框架零售合规率零售效用对抗伤害率
Claude Sonnet 4.5Agent-C100%80.46%0%
Claude Sonnet 4.5Unrestricted93.04%76.52%29.41%
GPT-5Agent-C100%73.62%0%
GPT-5Unrestricted91.88%71.01%3.92%

即使是最强前沿模型，在无约束下也无法可靠遵守安全策略——Claude Sonnet 4.5 在对抗场景中有 29.41% 的伤害率。Agent-C 不仅消除了所有安全违规，还将效用从 76.52% 提升至 80.46%（Sonnet 4.5）和 71.01% 至 73.62%（GPT-5）。

RQ3：开销分析

框架良性时间(s)VRAM(GB)对抗时间(s)
Agent-C480.2369.7249.85
AgentSpec409.3567.6625.18
DynaGuard494.1881.4044.10
Unrestricted333.0567.6627.83

Agent-C 的时间开销比 AgentSpec 高 17%，但 VRAM 仅增加 3%（69.72 vs 67.66 GB），远低于 DynaGuard 的 81.40 GB（因为 DynaGuard 需要额外运行一个判断 LLM）。

RQ4：约束生成 vs 重新提示

使用 Qwen3-8B 的消融实验显示，约束生成（Gen-Call）比重新提示（Gen-Call-Reprompt）效用高 3+ 个百分点（42.11% vs 36.52%），同时输入 token 减少最多 40%，输出 token 减少最多 54%。这证明了细粒度回溯在效率和效用上的双重优势。

RQ5：自动化规范生成

使用 Claude Sonnet 4.5 从自然语言策略自动生成 Agent-C 规范，在 Qwen3-8B 零售良性基准上达到 100% 合规和 42.11% 效用——与手动编写的规范完全相同。这显著降低了采用门槛。

启示与思考

从"最好努力"到形式化保证

Agent-C 的核心贡献在于将 LLM Agent 的安全执行从"最好努力"（best-effort）提升到形式化保证。现有的 DynaGuard 和 AgentSpec 虽然也声称提供安全防护，但它们的防护依赖于 LLM 自身的判断能力，在时序推理中频繁失败。Agent-C 通过 SMT 求解器提供了数学上可证明的合规性——只要 Safe-LLM 返回工具调用，就保证不违反规范。这种从概率性防护到确定性执行的转变，对安全关键场景的 Agent 部署具有深远意义。

约束生成与安全性的协同

一个反直觉的发现是：安全约束不仅没有降低效用，反而提升了效用。这是因为 Safe-LLM 算法在发现违规时不是简单拒绝，而是通过回溯探索替代方案，引导 LLM 走向合规且高效的动作路径。这与 SkillOpt 的理念相呼应——约束和优化不是对立的，恰当的约束本身就是一种优化信号。

时序推理的普适性

Agent-C 聚焦的时序约束问题在 Agent 安全中具有普适性。"先认证后访问"、"先打开后关闭"、"退款回到原始支付方式"——这些模式在几乎所有真实业务场景中都存在。DSL 的设计在表达力和可判定性之间取得了平衡：它覆盖了 FLTL 的一个实用片段，同时保证了 SMT 求解的效率。

与其他安全框架的互补

Agent-C 在对话层和工具调用层提供时序约束执行，与已发布的其他安全框架形成互补：

  • ActPlane：在 OS 层通过 eBPF 执行跨事件策略，关注系统调用级的数据流追踪。Agent-C 在更高的抽象层（工具调用）工作，两者可以构成纵深防御。
  • AgentFlow：通过静态分析发现 Agent 程序中的风险依赖路径。AgentFlow 可以在开发期识别需要哪些时序约束，Agent-C 则在运行时执行这些约束。
  • Cognitive Firewall：在对话层防御多轮越狱攻击。Cognitive Firewall 关注的是恶意意图的累积，Agent-C 关注的是工具调用的时序合规，两者的关注点不同但可叠加。

这启示我，Agent 安全需要多层、多维度的防护体系——没有任何单一框架能覆盖所有风险面。Agent-C 填补的是"时序约束形式化执行"这一关键空白，其 SMT-based 方法为确定性安全保证提供了一个值得借鉴的范式。

局限性

论文也坦诚了几点局限：DSL 不支持 Next 算子（无法约束紧邻的下一步动作）；状态投影假设工具状态全局一致（不考虑并发修改）；规范编写仍需要一定专业知识（虽然 LLM 辅助生成缓解了这一问题）；以及 SMT 求解的超时设置（2 分钟）可能在极端复杂规范下成为瓶颈。这些局限指明了未来工作的方向。

参考链接

研究