LeanGuard：用 Lean4 为工具调用加上一道可证明的安全闸门

导语

工具型语言模型代理一旦获得查询、修改账户或执行外部操作的能力，安全问题就不再只是“模型说了什么”，而是“模型实际做了什么”。即使代理遵循了大致任务目标，也可能因为上下文误导、提示注入或参数错误，发出领域策略禁止的工具调用。LeanGuard 的思路是把安全检查放到工具调用链路的最后一道关口：任何动作在抵达环境前，都必须通过用 Lean4 编写的策略验证。

核心要点

• 策略不仅检查当前参数。 LeanGuard 可以将当前状态谓词与执行历史结合起来，并支持带作用域的过去时序算子。因此，规则既能约束“这次调用的参数”，也能表达“此前是否发生过某类操作”等历史条件。
• 默认失败关闭。 当策略无法证明调用合规时，系统拒绝放行，而不是把不确定性当成许可。其决策程序还被证明与 LeanLTL 语义等价，为运行时检查提供了形式化依据。
• 拒绝后不止返回错误。 反馈模式会向代理说明被违反的规则并给出提示；证明引导修复则由 Lean 元编程搜索相近调用，在保持用户意图的前提下证明替代调用满足策略，不依赖模型自行猜测。
• 实验结果显示防护有效。 在 Tau-Bench 的五个 Qwen 模型、规模覆盖 0.8B 至 27B 的测试中，未加防护的代理至少执行了 33 次被策略禁止的调用，而 LeanGuard 没有放行这类调用。加入反馈后，任务成功率整体没有显著变化，同时重复触发被阻断调用的情况减少。
• 对提示注入的影响更直接。 在 DTap 测试中，直接提示注入成功率从 57.9% 降至 5.9%。在电信场景中，由于正常任务不需要写操作，加入防护并未改变良性任务成功率。针对因参数值导致的拒绝，修复机制在 252 个回放案例中为 88 个找到可证明合规的编辑，中位耗时为 2 毫秒。

意义与边界

LeanGuard 的价值不在于让模型永远做出正确判断，而在于把“模型提议动作”和“环境真正执行动作”分离开。模型可以继续负责理解任务、规划步骤和生成参数；Lean4 策略则负责定义哪些动作在特定状态与历史下绝对不能发生。这种分工尤其适合账户变更、数据写入和其他高风险工具场景。

同时，形式化验证并不会自动保证策略本身正确。策略覆盖范围、工具架构变化、拒绝后的交互成本，仍然需要工程团队持续维护。现有结果证明了“在调用前进行可证明检查”能够有效降低违规执行，但如何降低策略编写门槛、评估复杂策略下的延迟，以及及时发现策略与工具 schema 的漂移，仍是走向生产部署时的重要问题。

总体而言，LeanGuard 展示了一条清晰路线：让代理保留灵活的语言推理能力，同时把关键执行权限交给可审计、可证明且默认保守的运行时。对于希望将智能代理接入真实系统的团队，这比单纯依赖提示词或事后审计更接近安全控制的核心。

来源：Hugging Face Daily Papers