LeanGuard：通过 Lean 验证的工具调用代理安全护栏
LeanGuard 会在执行前，根据以 Lean4 编写的策略检查语言模型代理提出的每一次工具调用。策略可考虑当前状态和执行历史；若无法确认调用是否合规，系统就会拒绝执行。在 Tau-Bench 测试中，它拦截了未受保护代理发出的所有违规调用。在 DTap 上，直接提示注入攻击的成功率从 57.9% 降至 5.9%。与直接拒绝相比，针对被拦截调用提供反馈，使五个模型中的四个提高了任务成功率。基于证明的修复方法在重放的 252 次拒绝中，为 88 次找到了合规修改，中位耗时为 2 毫秒。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。