LeanGuard 在工具调用前拦下违规动作：DTap 直接注入成功率从 57.9% 降到 5.9%
工具调用型语言模型智能体常执行领域策略禁止的动作，LeanGuard 把用 Lean 4 写成的策略放在模型与工具之间，只有通过检查的调用才会真正执行。在 τ 2-bench 上，五个 Qwen 模型的无防护运行至少执行了 33 个 Lean 策略禁止的调用，加装 LeanGuard 后为零；在 DTap 上直接提示注入成功率从 57.9% 降到 5.9%，间接注入从 22.3% 降到 3.8%。带反馈的拒绝不显著改变任务成功率，而只读部署会拦下大量良性写操作。