arXiv · cs.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 · 9 小时前模型评分52
LeanGuard 提出用 Lean4 策略校验工具调用，拦截智能体越权操作
LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents
导读
LeanGuard 是一个运行时，在工具调用到达环境之前用 Lean4 编写的策略逐条校验，策略结合状态谓词与执行历史上有界的时间算子，判定过程被证明与 LeanLTL 语义等价，且采用失败即拒绝的方式。
分类置信度
中 · 待人工复核
- 只有单一媒体来源，需要人工复核。
来源级别：媒体与个人
事件类型：研究发布
证据摘录
- “We present LeanGuard, a runtime that checks every proposed tool call against a policy written in Lean4 before the call reaches the environment.”
来源：arXiv · cs.AI · arxiv.org