Hugging Face · 每日论文·2026-11-02 03:00· 2 天前精选AI 评分59

LEANGUARD：基于 Lean4 的智能体工具调用安全防护框架

LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

AI 导读

LEANGUARD 是一个基于 Lean4 的运行时框架，用于在工具调用前验证其是否符合策略，策略结合状态谓词与历史时态操作符，决策过程为 fail-closed，等价于 LeanLTL 语义。

推荐理由

原文给出了基于 Lean4 的策略验证框架和实证结果，读者可以据此理解如何用形式化方法提升智能体的安全性。