大型语言模型（LLM）代理通过工具调用可以完成网页浏览、代码生成和工作流编排等多步骤任务。然而，LLM 的幻觉、分布不稳定以及对抗性干扰，加上某些工具调用的不可逆后果，可能导致有害结果。现有的安全措施要么在事后使用随机 LLM 判官对轨迹打分，要么逐个拦截不安全的调用，且缺乏统一的确定性机制。\
我们提出 ContrAgent——一种基于合约的符号时序监督框架。ContrAgent 将代理的行为记为工具调用序列，并将其形式化为在固定可检查谓词集合上的轨迹。随后使用线性时序逻辑（LTLf）中的假设-保证合约描述所需行为。每个合约被编译为确定性有限自动机（DFA），该 DFA 同时承担两项职责：在线过滤代理动作以及离线评估记录轨迹。\
合约库作为可复用的知识库独立于具体模型维护，可在同一任务域的不同代理之间共享。我们在四个基准上验证了该方法，覆盖在线过滤和离线评估两种角色。实验表明，ContrAgent 在准确性上与最先进的 LLM 判官和基于规则的防护基线持平，同时提供确定性、可复现的判决，并在在线模式下实现了数量级更低的每次调用延迟。\
点评