arXiv cs.CL· Sreehari Sankar, Debargha Ganguly, Vikash Singh, Mohsen Hariri, Weicong Chen, Yanyan Zhang, Shouren Wang, Wang Yang, Chaoda Song, Alexander Nemecek, Osama Zafar, Idan Davidovich, Yuting Shao, Kai Ye, Biyao Zhang, Xinpeng Li, Joe Stubbs, Erman Ayday, Jing Ma, Vipin Chaudhary·· 11 小时前AI 评分47
LeanGuard：为工具调用智能体提供 Lean4 验证的运行时护栏
LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents
AI 导读
LeanGuard 是一个在工具调用到达环境前用 Lean4 策略校验每次调用的运行时，评估采用 fail-closed 方式，其判定过程被证明与 LeanLTL 语义等价。
正文 · AI 翻译
作者：Sreehari Sankar、Debargha Ganguly、Vikash Singh、Mohsen Hariri、Weicong Chen、Yanyan Zhang、Shouren Wang、Wang Yang、Chaoda Song、Alexander Nemecek、Osama Zafar、Idan Davidovich、Yuting Shao、Kai Ye、Biyao Zhang、Xinpeng Li、Joe Stubbs、Erman Ayday、Jing Ma、Vipin Chaudhary
摘要：使用工具的语言模型智能体常常执行其领域策略所禁止的操作。我们提出 LeanGuard，这是一个运行时，在每次提议的工具调用到达环境之前，用 Lean4 编写的策略对其进行检查。策略将状态谓词与作用于执行历史的有界过去时态算子相结合，求值采用失败关闭（fail-closed）方式，并且其判定过程被证明与 LeanLTL 语义等价。被拒绝的调用可以通过两种方式修正。在反馈模式下，智能体收到被违反的规则和提示；在证明引导修复模式下，Lean 元编程会搜索一个保持用户意图的邻近调用，并证明该策略允许该调用，无需模型参与。在 Tau-Bench 上使用五个 Qwen 模型（0.8B-27B）时，无防护的智能体至少执行了 33 次 Lean 策略禁止的调用，而 LeanGuard 一次也没有执行；在反馈模式下，任务成功率没有显著变化。在 DTap 上，LeanGuard 将直接提示注入成功率从 57.9% 降至 5.9%，而在电信领域，良性任务无需写入，良性成功率保持不变。与仅给出拒绝相比，反馈减少了重复的被阻止调用，并在五个模型中的四个上提高了任务成功率。在重放的拒绝案例中，修复为 252 次由参数值导致的拒绝中的 88 次证明了可接受的修改，中位耗时 2 毫秒。
| 主题： | 人工智能（cs.AI）；计算与语言（cs.CL） |
| 引用为： | arXiv:2611.02332 [cs.AI] |
| （或本版本的 arXiv:2611.02332v1 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2611.02332 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Vikash Singh [查看邮箱]
[v1]
2026年11月2日星期一 00:26:48 UTC（302 KB）
来源：arXiv cs.CL · arxiv.org