LeanGuard：面向工具调用智能体的 Lean 验证护栏

LeanGuard 是一个运行时护栏，在每次工具调用到达环境之前先用 Lean4 编写的策略进行校验，评估采用 fail-closed 方式，并把判定过程证明为与 LeanLTL 语义等价。策略把状态谓词与作用于执行历史的作用域过去时时序算子结合起来。在 Tau-Bench 上测试五个 Qwen 模型（0.8B-27B）时，无护栏的智能体至少执行 33 次策略禁止的调用，LeanGuard 一次也没有执行，而带反馈时任务成功率没有显著变化。在 DTap 上，LeanGuard 把直接提示注入成功率从 57.9% 降到 5.9%。被拒绝的调用可通过向智能体返回违反的规则与提示来纠正，也可用 Lean 元编程在不经过模型的情况下搜索并证明一个保留用户意图的邻近调用；作者称反馈减少了重复被拒调用，并在五个模型中的四个上相比单纯拒绝提升了任务成功率。