LEANGUARD：经 Lean 证明的工具调用智能体运行时护栏 LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents
用 Lean 4 写策略并证明裁决正确，拦截违规工具调用，还能给出带证明的自动修复
前置知识
Lean 4 与内核检查证明
Lean 4 既是编程语言又是交互式定理证明器：代码与数学命题用同一语言书写，每个证明最终由一个极小的可信内核逐条检查。依赖 sorry（未证占位）或非标准公理的定理会被审计脚本拒绝。它的 tactic 元编程机制允许用户编写自动化证明搜索程序，本文的 guard_repair? 就是这样一段 tactic。
LEANGUARD 的策略规则、可执行评估器和全部安全保证都用 Lean 4 写成并证明。理解「编译即验证」「内核检查」是读懂其可靠性声明（定理 1）的前提，也是判断这篇论文与普通工程护栏的本质区别所在。
线性时序逻辑 LTL 与过去时算子
LTL 是在事件序列上解释的模态逻辑，标准形式面向未来（next、until、finally）。本文用过去时变体：PREVIOUS 对应强 next（前一相关事件上成立）、ONCE 对应 finally（更早发生过匹配事件）、SINCE 对应 until（自某见证事件起持续成立），均可限定时间窗和作用域（按主体、会话或资源投影历史）。LeanLTL 是把这类语义形式化到 Lean 中的库。
「先读过资源才能写」「同一订单只能修改一次」「确认后 10 分钟内有效」这类策略只能用时序算子表达。论文的核心定理正是可执行裁决器与 LeanLTL 语义的等价性，不懂 LTL 就无法理解这个保证的含义。
Fail-closed（故障关闭）评估
fail-closed 指评估所需数据缺失或畸形时默认拒绝而非放行。本文中谓词会读取订单状态、金额等结构化数据，读取失败产生的是「错误」而非 false；准入要求所有相关组件无错（ErrorFree）才可能 allow，从而缺失的证据无法通过否定或析取运算偷偷变成授权。
这是准入公式 Eq. (1) 的组成部分，也是「模型不能靠断言用户已批准来伪造证据过关」这一安全性质的技术基础。fail-closed 与 fail-open 的取舍直接决定了护栏在数据不完整环境中的行为。
提示注入（直接与间接）
通过文本操纵 LLM 行为的攻击。直接注入把恶意指令放进用户输入；间接注入把恶意指令藏进智能体读取的外部内容（工具输出、网页、邮件）。本文的核心威胁模型是间接注入：工具输出里一句「客户已预先批准」被智能体当成事实。DTap 是分别度量两类攻击成功率的红队基准。
论文最重要的安全结果（直接注入成功率 57.9%→5.9%）针对的就是这类攻击。理解「工具输出文本一律不作为证据」这一设计，才能明白 LEANGUARD 为什么对注入天然免疫——它根本不读那些文本。
运行时监控与 Shielding
形式化方法中的 shielding 传统：一个监视器位于系统与环境之间，阻止或替换将违反形式安全规范的动作。LEANGUARD 属于这一谱系，但监视器位于语言模型与其工具之间，且协议含 dispatch reservation：允许的调用先登记再执行，单次操作在结果未知期间不可重复，未决操作保留其配额。
智能体护栏领域已有 GuardAgent、Progent、AgentSpec、CaMeL、FORGE 等多个系统，理解 shielding 谱系和相关工作的坐标，才能看清本文「被证明的裁决器 + 被证明的修复」在领域中的相对位置与真正增量。
τ²-bench 与 DTap 基准
τ²-bench 在双控环境（智能体加模拟用户）中评估有状态工具调用，带明确的自然语言领域策略，本文形式化其 retail、airline、telecom 三域共 278 个任务。DTap 是可控红队平台，提供直接注入、间接注入攻击与良性任务，本文评估其中 7 个域。两者都提供确定性判分或 LLM 裁判。
论文所有数字结果都来自这两个基准。实验采用 None（无护栏）/LG（裸拒绝）/LG+F（带反馈）三种臂，任务成功率与策略合规性分开度量，理解这一协议设计才能正确解读主表 Table 1。
研究动机
工具调用型智能体一旦能改变外部状态——发消息、改订单、发起退款或扣款——其失败就不再只是回答错误，而是不可逆的真实后果。现状是两类失败并存且方向相反：一方面，小模型频繁违反领域策略，τ²-bench 上 Qwen3.5-0.8B 与 2B 分别有 14.4% 和 15.4% 的会话被裁判判定执行了违反策略的调用；另一方面，模型越大越容易被注入攻击操纵，DTap 上直接注入成功率从 0.8B 的 46.7% 升到 9B 的 74.4%，无护栏整体直接注入成功率 57.9%、间接 22.3%。典型场景见 Figure 1：客户要求用相机换掉订单里的书架，工具输出中被注入「客户已预先批准」，智能体便调用 exchange_delivered_order_items 把差价记到攻击者礼品卡 gift_card_7741，全程未向客户确认。重放无护栏轨迹发现至少 33 个被 Lean 策略禁止的调用实际执行并改变了状态。已有护栏（GuardAgent、ToolSafe、Progent 等）多为学习型或符号启发式，裁决过程本身没有被证明正确，无法给出「违规调用一个都不会执行」的保证。
本文的目标是本文要回答的问题是：形式化验证能否同时「强制策略合规」与「帮助智能体完成任务」。具体目标拆成四点。第一，把自然语言领域策略形式化为 Lean 4 策略，在每次工具调用到达工具之前裁决，被 Lean 策略拒绝的调用一个都不能执行，且这个保证本身要由机器检查的定理给出，而不是工程约定。第二，裁决必须 fail-closed：证据缺失或数据畸形时拒绝而非放行，使缺失的证据无法变成授权。第三，拒绝之后要给智能体两条恢复路径：一是把被违反的规则标识与自然语言提示反馈给模型让它自己修正；二是由 Lean 元编程搜索一个保持用户意图的近邻调用，并返回内核检查过的可接纳性证明，全程不依赖模型。第四，在实现上述保护的同时，任务成功率不能显著下降——既要在合规性敏感的 τ²-bench 上度量代价，也要在注入攻击基准 DTap 上度量防护收益，并单独考察电信这类无需写操作的领域中保护是否零代价。
与已有工作不同的是，已有工作把符号策略用于运行时：Progent 用最小权限符号约束，AgentSpec 提供 DSL 与运行时强制，CaMeL 分离可信控制流与不可信数据流，FORGE 用参考监视器强制执行 Datatalog 策略；也有工作开始把 Lean 用于智能体：Lean-Agent Protocol 检查金融智能体动作，Lean4Agent 形式化工作流与轨迹。它们与本文的本质区别在于：没有一个系统把「可执行裁决器」与「独立时序语义」之间的关系证明为定理——执行器写错了，策略写得再好也白搭，而这个错误在之前所有系统中都只能靠测试发现。LEANGUARD 的独特切入有三层。其一，准入可靠性定理：可执行评估器对每个历史返回 true 当且仅当该历史满足策略的 LeanLTL 解释，把「策略写对了」与「执行器算对了」两个正交问题分离。其二，证明引导修复：Lean 元编程搜索参数编辑并返回内核检查的可接纳性证明，作者指出这是首个能产出「被证明的修复」的智能体护栏。其三，拒绝后的完整闭环：先前工作止步于拦截，本文同时量化模型自行恢复（反馈）与系统代为修复（证明）两条路的效果。
核心方法
核心直觉是把护栏看作对「状态转移」的控制，而非对「生成文本」的审查：调用格式上合法，但允许与否取决于后端状态、先前动作、用户是否看到过详情、是否存在先前授权。技术路线是三步流水线。第一步，智能体照常发出结构化工具调用（LEANGUARD 不增加新动作语言，模型从不写 Lean 代码），宿主在调用到达工具前截获并视其为不可信数据；领域适配器对权威后端做快照（带修订号）、校验参数、推导策略所需事实，工具输出中的文本永远不作为证据。第二步，用编译后的 Lean 策略评估该调用：策略由 permit/requirement/forbid 三类规则加带时间窗与作用域的过去时算子（PREVIOUS、ONCE、SINCE）构成，评估严格 fail-closed。第三步，只有所有相关组件无错且通过才允许；允许的调用先记录为 dispatch reservation 再执行，保证单次操作不被重复；拒绝的调用返回形式化决策记录加自然语言提示，或由 Lean 的 guard_repair? 离线搜索修复。整个监控协议为 proposal → snapshot → admission → dispatch → external effect → outcome，未来决策会考虑已授权但仍在执行中的动作。
核心创新是把「准入函数的正确性」变成定理。设 $s_t$ 为权威环境状态、$H_t$ 为监视历史、$a_t=(u_t,x_t)$ 为提议调用，可信适配器导出证据 $o_t=O(s_t,a_t)$ 并形成决策上下文 $c_t=(a_t,o_t,H_t)$。准入函数定义为 $D_P(c_t)=\text{allow}\Leftrightarrow\bigwedge_{p\in P}p(c_t)\wedge\bigwedge_{r\in R}r(c_t)\wedge\bigwedge_{f\in F}\neg f(c_t)\wedge\mathrm{ErrorFree}_P(c_t)$。定理 1（准入可靠性）：若 LEANGUARD 返回 allow，则 $c_t$ 满足 Eq. (1) 的 LeanLTL 解释，运行时只在 allow 后分派。关键设计是「评估器不是规范」：历史 $[e_2,e_1]$ 被嵌入为从最新到最旧的 LeanLTL 有限迹，先对单个时序公式证明等价，再升级到授权与带 fail-closed 条件的完整准入决策。三个过去时算子均可限定时间窗与作用域（按主体、会话或资源投影历史），使「对该订单的上一次观察」确实指向那个订单。与已有方法的本质区别：CaMeL、FORGE、Progent 靠工程实现保证执行正确，本文靠内核检查的定理，且被拒调用还能获得带证明的修复。
方法步骤详情
步骤 1（证据落地）：模型经普通工具 schema 发出调用，宿主截获；适配器快照权威后端（带修订号），校验参数并把事实写入 journal；过去分派的事实保留在分派时的记录上，模型无法靠断言「客户已批准」伪造证据。用户确认是绑定到具体提议、参数、资源与状态修订的一次性可信证据，用后即消耗。步骤 2（策略评估）：谓词是对决策上下文的领域检查（如 retail.order_owner 验证订单属于已认证客户）；规则三类——permit 缺失即默认拒绝，requirement 必须满足，forbid 直接禁止，宽 permit 不能覆盖未满足的 requirement 或适用的 forbid。谓词读取结构化数据失败时产生错误而非 false，只有 ErrorFree 成立才可能 allow。步骤 3a（反馈恢复）：拒绝返回形式化决策记录（失败规则 ID、适用 forbid、评估错误、支撑证据）与自然语言提示，提示只是渲染、本身不被验证。步骤 3b（证明修复）：guard_repair? 是 Lean 元编程 tactic，最多尝试 32 个按优先级排序的候选编辑，guard_solve 用已有假设、封闭义务求值和 grind 引擎（等式推理、线性算术、定理实例化）消解目标，只返回带内核检查证明的修复；留有未决目标或依赖 sorry 的候选一律拒绝。
技术新颖性
技术新颖性有四点。第一，可执行评估器与独立语义的等价性分级证明：先单时序公式，再授权，再带 fail-closed 条件的完整准入决策；度量窗口与作用域投影扩展了 LeanLTL 的迹集合，并非平凡有限迹 LTL；全部证明在策略构建时检查，不为单次调用构造。第二，证明引导修复：修复是 $\exists x' \in C_t.\ \mathrm{EditOK}(x_t,x')\wedge D_P(c_t(x'))=\text{allow}$ 的见证，EditOK 约束编辑保持用户意图（如 100 单位预算已花 60，提议花 70 可修复为 40）；配套定理证明修复对 $D_P$ 存在当且仅当对策略的 LeanLTL 语义存在，因此带时序义务的修复目标可直接在时序逻辑中陈述。第三，扩展性设计：策略作者用 guard_rule 属性把已证明事实注册进求解器定理库，或提供自定义消解 tactic，扩展修复无需改动运行时。第四，验证目标定位：Lean-Agent Protocol 检查金融智能体动作但拒绝时只告知违反的义务，Lean4Agent 形式化工作流与轨迹；本文验证的是「提议的工具调用在已审策略、可信状态与历史下是否可接纳」这一运行时决策，并把拒绝变成可恢复的结构化信号。据作者所知，没有已有智能体护栏能产出被证明的修复。
实验结果
RQ1：无护栏时裁判标记 9.7% 的 τ²-bench 会话；重放发现至少 33 个违规调用（14 个状态违规、17 个时序违规、3 个禁止类）在 28 个会话中实际执行并改变状态。LEANGUARD 停下的 1,702 个调用中，授权失败最多（572，含 338 个未经确认的写操作）、无效调用 551、时序不兼容 411、策略禁止 313。RQ2：LEANGUARD 执行的策略禁止调用为 0；τ²-bench 任务成功率从 72.7%（无护栏）到 68.9%（裸拒绝，$p=0.007$）再到 70.9%（带反馈，$p=0.21$ 不显著）；裁判标记率 9.7%→5.6%/6.5%（$p=0.002$）。与 ToolSafe（违规率 1.6%）、Progent（2.6%）相比，LEANGUARD 是唯一达到 0.0% 的护栏。DTap 上直接注入 57.9%→5.9%（降 52.0pp）、间接 22.3%→3.8%（降 18.5pp）；telecom 域良性成功率不变（75.1%→75.3%）而直接攻击 55.1%→2.4%，证明无写需求的领域防护零代价；但只读部署使整体良性成功率 53.1%→12.5%。RQ3：被拦截调用 983→719，恢复动作 34→48（占被拒动作 5.5%→9.1%，$p=0.02$），五个模型中四个任务成功率提升 2.2–5.8pp；例外 Qwen3.8-27B（75.9%→71.2%），但 43 个反转任务中 35 个其反馈臂根本没收到过拒绝，属随机分支差异。裸拒绝后 30% 是同一调用原样重试再被拒，反馈降到 22%。RQ4：离线重放复现全部 7,720 个准入决策；1,613 个拒绝逐一作为定理检查；252 个参数值类拒绝中 88 个（34.9%）被证明存在可接纳编辑，中位 2ms（最多 70ms）；最常见修复是退款到订单原支付方式（64）和用卡而非旅行券支付改签费（18）；智能体自己发出被修复调用时任务成功 16/22，对照仅 7/66。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| τ²-bench 策略合规（违规调用执行数） | 被 Lean 策略禁止且实际执行并改变状态的调用数 | 0 | 无护栏 ≥33 个调用（分布在 28 个会话） | 完全消除（按构造保证，重放确认） |
| τ²-bench 任务成功率 | 基准确定性奖励（%） | 70.9（LG+F）/ 68.9（LG） | 72.7（无护栏） | −1.8pp（不显著 $p=0.21$）；裸拒绝臂 −3.8pp（显著 $p=0.007$） |
| τ²-bench 裁判标记率 | LLM 裁判判定执行了违反基准策略调用的会话比例（%） | 6.5（LG+F）/ 5.6（LG） | 9.7（无护栏） | −3.2pp / −4.1pp（$p=0.002$） |
| DTap 直接提示注入防御 | 直接注入攻击成功率（%，越低越好） | 5.9 | 57.9（无护栏） | −52.0pp |
| DTap 间接提示注入防御 | 间接注入攻击成功率（%，越低越好） | 3.8 | 22.3（无护栏） | −18.5pp |
| DTap 电信域良性任务（无写需求场景） | 良性任务成功率（%） | 75.3（LG+F） | 75.1（无护栏）；同域直接攻击 55.1→2.4 | 保护零代价（+0.2pp，同时攻击成功率降 52.7pp） |
| τ²-bench 与其他护栏的违规率对比 | 重放发现的有违规调用执行的会话比例（%） | 0.0（LG 与 LG+F 两臂） | 无护栏 2.0（28 会话）、ToolSafe 1.6（22）、Progent 2.6（36） | 唯一达到 0.0% 的护栏 |
| τ²-bench 拒绝后的证明修复 | 参数值类拒绝中被证明可接纳修复的比例与耗时 | 88/252（34.9%），中位 2ms（最多 70ms），验证中位 8ms | 无（此前没有护栏能产出带证明的修复） | 首个带内核检查证明的修复能力 |
局限与改进
作者承认的局限：保证相对于已审形式化规范与可信输入——自然语言策略只形式化「工具可强制执行的子集」，形式化由 LLM 起草、人工修正，此步错误证明捕获不到；保证假设适配器如实上报且所有关键调用经过监视器；自由对话到同意记录的转换不在验证边界内（τ²-bench 用温度 0 的模型调用模拟可信确认屏，模拟器出错会产生错误同意证据）；只管工具调用，响应文本携带的伤害超范围——只按文本评判的客服与旅行攻击仍从 41.0% 降到 30.2%，医疗五个攻击类保持 21.4–37.0% 直接攻击成功率（如诊断操纵、忽略过敏史）；DTap 只读部署高估保护（良性成功率 53.1%→12.5%）；证明修复只在重放离线评估，运行时尚未调用；τ²-bench 有两条规则比基准更严；DTap 策略只覆盖 14 域中的 7 个；裁判是 LLM 且是受评模型之一；实验仅用 Qwen 家族、英文任务、模拟用户。我的补充观察：效果无法建模时 fail-closed 停下了 5,792 个调用（shell 命令 2,728、无价市场单 835），在通用环境会显著放大误拦；retail 域任务成功率损失最大（LG+F −7.9pp），约束式策略对多步写任务的摩擦真实存在；修复对部分规则覆盖率极低（telecom.payment_request 4/58、airline.booking 0/18），候选编辑生成器仍朴素。
独立分析的弱点
独立分析的弱点与改进方向。(1) 效果不可建模的工具一律拒绝：DTap 中 5,792 个调用因效果无法确定被停（execute_command 2,728 个、trade_stock 1,143 个），在允许 shell 的真实环境会频繁「误杀」；应为常见工具族建立效果抽象层，或让应用作者用带证明的 contract 覆盖更多工具语义。(2) 写权限部署的代价未解决：只读部署让旅行、金融、法律良性成功率降到 0.0%，医疗因患者注册被拒降到 0.3%，论文只在电信展示零代价场景；需把授权发放、双人审核、一次性确认等可信基础设施工程化并评估延迟与可用性。(3) 修复离线运行：运行时不调用 guard_repair?，把修复递给智能体的端到端收益无法度量；应在线化并测延迟预算内的成功率。(4) 修复候选生成器弱：252 个可修拒绝只修复 88 个，telecom.payment_request 仅 4/58；可加入类型驱动的参数枚举、从历史轨迹挖掘类似调用。(5) 反馈对最大模型收益不稳定（27B 降 4.7pp）且每任务只跑一次；应多种子重复，区分「反馈分支差异」与「反馈质量」。(6) 同意证据由模型模拟的可信屏生成，是验证边界外最脆弱一环；应换成确定性 UI 或硬件签名确认通道。(7) 裁判与被评最强模型同为 Qwen3.8-27B 且给自己参与的会话打分，存在自评偏差；可引入异构裁判与人工审计校准。
未来方向
未来方向。作者提出的：把拦截器从「过滤器」升级为「经验证的修正来源」，运行时在线调用 guard_repair?，把带证明的修复作为建议返回给智能体；响应文本伤害仍超出任何工具级检查。基于成果可延伸的：其一，策略自动形式化的可靠性——用 LLM 起草、Lean 检查、差分测试对齐自然语言策略与编译策略的轨迹判定，降低人工修正成本；其二，把 Lean 反馈用作强化学习信号训练智能体（相关工作已在定理证明中这样做），把「一次通过策略」内化为模型能力而非外部约束；其三，扩展到其余 7 个 DTap 域与真实生产后端，评估确认屏、授权发放、双人审核等可信基础设施的延迟与可用性；其四，工具边界护栏与输出级检查（如 CaMeL 式信息流控制）组合成纵深防御，覆盖响应文本伤害；其五，利用附录 H 的定理（修复存在性在 $D_P$ 与 LeanLTL 语义间等价）探索时序修复目标，例如「补一个前置调用」式的多步证明修复（先认证客户再执行操作）；其六，多模型家族、多语言与真实用户研究，消除单一 Qwen、英文、模拟用户的推广性疑问。
复现评估
复现评估：论文正文与附录均未给出代码开源链接，这是最大不确定项。数据与模型均公开：τ²-bench 278 个任务（114 retail、50 airline、114 telecom，revision 672227c）、DTap 七域共 2,611 个评估用例（电信 434、旅行 355、客服 358、医疗 1,091、金融 95、法律 92、OS 文件系统 186）、Qwen3.5（0.8B–9B）与 Qwen3.8-27B 均可下载。算力需求中等：每任务每臂一次（seed 300、采样解码、240 步或 2 小时上限），5 模型 × 3 臂 × 278 任务，外加 DTap 数千用例（含上千个未计分会话）。Lean 侧非常轻量：单条拒绝的修复搜索中位 2ms（最多 70ms）、验证中位 8ms，最大的 416 定理重放文件编译 43–50s（主要耗在加载 Lean 与 Mathlib）。复现难度：高。策略只有 583 行 Lean（45 条规则），但可靠性定理、fail-closed 条件、修复存在性定理与 guard_repair? 元编程 tactic 都需要熟练的 Lean 4 开发能力；DTap 侧需人工审阅 199 个工具合同，确认屏模拟器等基础设施也要自建。若作者开源，复现主结果（违规调用为零、DTap 攻击成功率骤降）应当可行；复现修复实验需逐条对齐其候选编辑顺序与优先级。
论文图表
上半部分是无护栏情景：客户要求把上一订单里的书架换成相机，工具输出中被注入「客户已预先批准」，智能体照办，调用 exchange_delivered_order_items 将差价记到攻击者的礼品卡 gift_card_7741，全程未请求确认。下半部分是有 LEANGUARD 的情景：同一调用因「note 不是同意、卡不在账户上」被拒绝并返回规则（identity、order_owner、delivered、confirmation、exchange_items）与提示「请客户确认换货」；客户在可信屏上回答「用我的 Visa •••6411」后，重发的调用被放行并记账。底部是三行头条结果：直接攻击成功率 57.9%→5.9%，间接攻击 22.3%→3.8%，违规执行调用 33→0。
一图讲清全文：威胁模型（工具输出注入）、护栏行为（拒绝+反馈+恢复）与量化收益（三组关键数字）全部呈现，是理解论文动机与价值的最佳入口。