热点事件观察中

LeanGuard：用Lean4验证工具调用护栏

1 篇报道1 个报道来源2 天前更新

先了解这件事

AI 综述

Sreehari Sankar 等作者提出 LeanGuard，一个在工具调用到达环境前用 Lean4 编写的策略逐条校验的运行时护栏，评估采用 fail-closed 方式，并称其判定过程与 LeanLTL 语义等价。在 Tau-Bench 上测试五个 Qwen 模型（0.8B–27B）时，无护栏智能体至少执行 33 次策略禁止的调用，LeanGuard 为零；在 DTap 上，作者称直接提示词注入成功率从 57.9% 降至 5.9%。这些数字来自论文自述的评估，尚未见独立复现。

AI 根据报道生成 · 2 小时前更新

最新进展11月2日 08:00

LeanGuard：用 Lean4 验证的工具调用智能体运行时护栏

报道时间线

沿着报道，了解事件的不同侧面。

11月2日

08:00
HuggingFace Daily Papers
LeanGuard：用 Lean4 验证的工具调用智能体运行时护栏
LeanGuard 是一个运行时护栏，在工具调用到达环境前用 Lean4 编写的策略逐条校验，评估采用 fail-closed 方式，并证明其判定过程与 LeanLTL 语义等价。在 Tau-Bench 上测试五个 Qwen 模型（0.8B-27B），无护栏智能体至少执行 33 次策略禁止的调用，LeanGuard 为零；在 DTap 上把直接提示词注入成功率从 57.9% 降至 5.9%。

本事件热度走势

还没有足够的连续观测数据，暂不绘制趋势。