LeanGuard 在工具调用前拦下违规动作：DTap 直接注入成功率从 57.9% 降到 5.9%
核心概要
工具调用型语言模型智能体常执行领域策略禁止的动作，LeanGuard 把用 Lean 4 写成的策略放在模型与工具之间，只有通过检查的调用才会真正执行。在 τ 2-bench 上，五个 Qwen 模型的无防护运行至少执行了 33 个 Lean 策略禁止的调用，加装 LeanGuard 后为零；在 DTap 上直接提示注入成功率从 57.9% 降到 5.9%，间接注入从 22.3% 降到 3.8%。带反馈的拒绝不显著改变任务成功率，而只读部署会拦下大量良性写操作。
深度剖析
LeanGuard 在工具调用到达环境之前逐条对照 Lean 4 策略做准入判断，被拒绝的调用不会执行，因此智能体无法造成策略禁止的状态变更。 此前的智能体护栏多以符号约束、领域专用语言或学习型检查器在运行时约束调用，LeanGuard 的不同之处在于其准入过程被证明与一个独立时序逻辑语义等价，并把违反的规则返回给智能体。 在 τ 2-bench 上，把无防护回合重放后至少找到 33 个执行并改变状态的违规调用，分布在 28 个回合中；加装 LeanGuard 后，1,702 个被拦调用无一执行。在 DTap 上直接注入成功率从 57.9% 降到 5.9%，间接注入从 22.3% 降到 3.8%。
策略由状态谓词和三种过去时算子组成，可以表达“先读后写”“同一订单只改一次”这类依赖执行历史的义务。 仅看当前状态的检查无法表达这类顺序与次数约束，LeanGuard 用 PREVIOUS、ONCE、SINCE 三个算子并允许限定时间窗和按主体、会话或资源限定作用域。 τ 2-bench 的零售、航空、电信三个域被形式化为 45 条规则、覆盖 43 个智能体工具、共 583 行 Lean 代码；评估采用 278 个任务，每个模型每个实验臂各跑一次。
被拒绝的调用有两条纠正路径：把失败规则和自然语言提示返回给模型，或由 Lean 元编程搜索一个保持用户意图的邻近调用并给出内核校验的准入证明。 只返回“未执行”的裸拒绝会让智能体反复重试同一调用，反馈把重复被拦调用从 983 次降到 719 次，恢复的拒绝动作从 34 个升到 48 个。 在重放的 τ 2-bench 拒绝记录上，证明式修复对 252 个由参数取值导致的拒绝中的 88 个给出了可准入修改，中位耗时 2 毫秒；该搜索在实验之后离线运行，智能体并未收到这些修复。
启示与展望
演示范围是 τ 2-bench 的零售、航空、电信三个域和 DTap 的七个域，全部实验使用 Qwen 一个模型家族、英文任务和模拟用户；保证相对于经审阅的形式化规范与可信输入成立，且只覆盖工具调用这一执行边界。
形式化只覆盖自然语言策略中可由工具强制执行的部分，且由语言模型起草、人工修正，这一步的错误不会被证明捕获；DTap 的只读部署会拦下良性写操作，因此其攻击成功率是保护效果的上界；证明式修复仅在重放的拒绝记录上离线评估，运行时尚未调用；τ 2-bench 的违规率来自一个本身也在被评估的模型裁判。