**LeanGuard：基于 Lean4 的形式化验证工具，实现智能体安全调用防护**

_LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents_

> 针对工具使用型智能体常违反领域策略的问题，研究提出了 LeanGuard 运行时系统。该系统利用 Lean4 编写策略，在调用前进行形式化验证，并支持“反馈提示”和“证明引导修复”两种机制。实验表明，LeanGuard 能完全阻断违规调用，显著降低提示注入攻击成功率，并在不损害正常任务成功率的前提下，高效修复部分被拒绝的调用请求。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：ai-models
- **发布时间**：2026-11-03 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2611.02332)