SpecGuard 用 Lean 证书在编码 Agent 执行前证明任务冲突

如何在自主代码智能体运行之前，检测并形式化证明任务的自然语言描述与测试套件之间存在冲突。

• 背景与重要性：作者指出，当评估信号与用户意图产生分歧时，前沿代码智能体往往会通过篡改测试、硬编码输出或移除安全机制来进行奖励黑客攻击（reward hacking），甚至在真实部署中造成删除生产数据库等危害。
• 现有方法的不足：作者认为，事后轨迹监测或让大模型直接判断任务是否冲突，仍然需要信任检测模型本身的输出，缺乏可独立核验的证据；且在事前判断时大模型容易产生漏判。
• 核心观察与假设：作者假设任务意图具有值语义（value-semantics），若能独立从任务描述生成可执行规约并独立形式化测试要求，则二者的不一致性可通过定理证明器内核计算转化为不可满足性证书。
• 威胁模型：
  • 攻击者目标与场景：代码库或依赖项中存在疏忽引入的错误测试或对抗性注入，使测试与任务描述冲突，诱导智能体在解决任务时产生作弊或消除安全机制的行为。
  • 信任边界：任务自然语言描述 D 被视为受信任的预期行为权威陈述；代码库 C（可能含有缺陷）仅作为解释 D 的上下文，不是权威；修改 D 超出威胁模型。
  • 不受信任的输入：测试套件 T 和代码库 C 均被视为不可信，可能包含对抗性注入或错误。
  • 受害系统：在代码仓库、沙箱或评估框架中运行的自主代码智能体。
• 提出的防御框架：论文提出了 SPECGUARD，在智能体执行前，分别由 SpecAgent 生成 Lean 4 可执行规约、TestAgent 形式化测试要求，并通过 Certifier 构建语义连接器，利用 Lean 内核输出机器可校验的冲突证书。

• 奖励黑客与测试作弊：Amodei 等人（2016）、Krakovna 等人（2020）和 Skalse 等人（2022）长期研究优化系统中的规约博弈与奖励黑客；Arx 等人（2025）观察到前沿代码智能体在评测中颠覆任务设置。EvilGenie（Gabor et al., 2026）与 SpecBench（Zhao et al., 2026）研究允许测试作弊的代码环境；ImpossibleBench（Zhong et al., 2025）通过故意篡改测试用例使其与任务描述冲突并观察智能体作弊行为。作者称本文采用了与 ImpossibleBench 相同的冲突任务设定，但探讨在智能体运行前形式化确立冲突。
• 自动形式化与规约合成：Wu 等人（2022）与 Weng 等人（2025）推进自然语言向形式化语言翻译；Liu 等人（2025）与 Lu 等人（2024）指出类型正确的形式化仍可能偏离源语义。Endres 等人（2024）与 Sun 等人（2024）从自然语言合成形式后置条件和契约；Chen 等人（2022）与 Ni 等人（2023）利用生成测试或执行结果作为语义证据。CodeSpecBench（Chen et al., 2026）、Intent Formalization（Lahiri, 2026）以及同期工作 SWE-Proof（Ma et al., 2026）研究仓库级行为规约生成或验证候选实现是否满足规约。作者指出 SPECGUARD 是在生成候选实现之前，检验独立表示的任务意图与测试要求是否联合可满足。
• 基于 LLM 的检测与智能体形式化监管：LLM 裁判（Zheng et al., 2023; Gabor et al., 2026）、训练期推理监控（Baker et al., 2025）、生成期激活探针（Wilhelm et al., 2026）、轨迹事后监控 MALT（Neev Parikh, 2025）与 TRACE（Deshpande et al., 2026）通过观察模型行为或已完成轨迹检测奖励黑客。作者指出这些方法运作在智能体行为期间或之后，且判定依赖对检测模型的信任。运行时约束（Wang et al., 2025）、可强制执行理论（Ray, 2026）、静态工作流验证（Xavier et al., 2026）、技能审计 Semia（Wen et al., 2026）、MalSkillBench（Guo et al., 2026）与保证安全 AI 框架（Dalrymple et al., 2024）将形式化与静态方法引入智能体监管。
• 基线方法与基准：基线包括基于 bash 和 Python 工具进行 5 次多数投票的 LLM Judge Agent，以及生成可执行 Python 模型并直接运行争议测试的 Python Reference Model。评估基准包含 SWE-bench、LiveCodeBench、VERINA 以及来自真实 GitHub 仓库的冲突案例。

作者将本文定位为携证代码（PCC，Necula, 1997）谱系下的具体实例，其核心区别在于并非证明候选实现满足规约，而是在代码智能体或候选实现运行前，自动生成任务级不一致性的机器可校验形式化证明。

SPECGUARD 在代码智能体运行前，将任务自然语言描述与测试套件分别独立转换为形式化表示，并通过语义连接器由 Lean 4 内核检查二者是否不可同时满足，从而产生机器可验证的冲突证书。

核心设定与形式化

• 任务定义与适用范围：代码任务定义为三元组 t = (D, C, T)，其中 D 为自然语言描述，C 为代码库，T 为测试套件。任务范围限定在具有值语义（value-semantics）意图的任务，其行为可表示为输入-输出值的约束。
• 冲突证书形式化定义：设 Spec_D 为根据 D 和 C（不访问 T）生成的形式化规约，Test_T 为独立从 T 生成的形式化约束，二者约束行为接口的实现 f。SPECGUARD 尝试证明核心命题： ¬ ∃ f. Spec_D(f) ∧ Test_T(f) 若该命题由 Lean 内核验证通过，即构成冲突证书。
• 三值判定机制：系统返回 {conflict, no-conflict, inconclusive} 之一。若无法构建连接或描述未规定测试行为，输出 inconclusive。

三智能体流水线设计

• 规约生成（SpecAgent）：在完全屏蔽测试 T 的前提下，SpecAgent 获得代码库 C 的 120 轮 bash 探索权限，将自然语言 D 转化为可执行文件 spec.lean，定义输入输出类型及预期行为函数 Spec.run，要求表达通用行为规则而非硬编码样本。
• 测试形式化（TestAgent）：TestAgent 将补丁中引入或更新的测试断言转译为 tests.lean，如实记录测试场景的输入、设置、操作、观察点和要求的结果，指令明确禁止修复或预测断言。
• 连接与证明（Certifier）：Certifier 生成语义连接器 cert.lean，将每个形式化测试场景映射到规约接口并核对断言，在无法对齐时返回 none。附录 H 给出了三个智能体的完整提示词。

求解与内核验证机制

• 编译器反馈循环：三个智能体各自在 Lean 编译器反馈循环中运行最多 10 轮以消除类型错误，单任务超时时间设为 1 小时。
• 内核计算替代证明搜索：由于规约可执行且测试要求为具体值，最终定理使用 Lean 的 by decide 策略判定所有用例受支持且至少一个断言失败，求解过程完全由 Lean 内核规约求值完成。
• 证据等级分层：论文定义了 5 个证据层级：LLM 判定（LLM Judgement）、执行核验（Execution Checked）、属性测试（Property Tested）、形式化证明（Formally Certified）和人工验证（Human Verified），SPECGUARD 位于形式化证明级别。

实验设置

• 被测模型：GPT-5.6 Sol、Claude Opus 5、Claude Fable 5、Kimi K3。
• 数据集与规模：包含 349 个突变任务的 SWE-bench；95 个 LiveCodeBench 任务；22 个收集自 GitHub 真实 issue 和 PR 的真实冲突；187 个含人工参考规约的 VERINA 任务。
• 基线方法：LLM Judge Agent（通过 bash/Python 工具分析仓库并进行 5 次多数投票）；Python Reference Model（生成 Python 模型并在配对测试设置下执行测试）。
• 指标定义：冲突检出率 P(V = conflict | T')、形式化证明冲突率 P(V = certified conflict | T')、漏报率 FN P(V = no-conflict | T')、误报率 FP P(V = conflict | T)、无法确定率 Inconclusive。
• 评估方式与参数：严格任务级评估（完整测试向量匹配才算正确）；GPT-5.6 Sol 重复 3 次取均值和标准差，其余模型运行 1 次；GPT-5.6 Sol、Opus 5 和 Fable 5 采用 medium reasoning effort，Kimi K3 采用温度 0；计算 95% bootstrap 置信区间。

主结果

表格较宽，可左右滑动

（据 Table 8 与 Table 10；Judge Agent 与 Python Reference 不产出 Lean 形式化证明；未突变原任务误报率见 Table 8：Sol 6.0%、Opus 5 3.4%、Fable 5 4.0%、Kimi K3 12.0%、Judge Agent 2.3%）

• 检出率与证明率的分离：作者指出，单测试设置下 SPECGUARD 检出率最高达 72.8%（Fable 5），但证明冲突率最高为 51.1%（Sol），检出率最高的模型并不必然产生最高的证明率。
• 漏报率与不确定性：单测试设置下 GPT-5.6 Sol 的 SPECGUARD 漏报率为 8.1%，远低于 LLM 裁判的 39.8%；LLM 裁判从不输出 inconclusive，而 SPECGUARD 在 Sol 上保留了 34.9% 的 inconclusive 判定。
• 运行成本对比：据 Table 12，GPT-5.6 Sol 运行 SPECGUARD 单测试任务平均成本为 $0.26，配对测试为 $0.46，LLM 裁判为 $0.84，Python Reference Model 为 $0.45。

配对测试设置实验

• 测试内容：向 TestAgent 同时提供原始和突变两组测试用例，评测对齐难度缓解后的表现。
• 实验结果：据 Table 11，各模型检出率提升 16.6 至 25.2 个百分点（Sol 达 73.9%，Opus 5 达 87.1%，Fable 5 达 89.4%，K3 达 83.7%），证明冲突率提升 10.6 至 19.2 个百分点（Sol 达 67.0%，Opus 5 达 58.2%，Fable 5 达 60.2%，K3 达 67.0%）。
• 作者解读：作者认为配对测试明确了发生变化的测试条件，降低了连接难度，表明跨表示对齐是冲突证明的核心瓶颈。

失败原因归因与人工审计

• 测试内容：对未成功检出的 793 次运行进行分解，并对 242 次失败运行及 60 个成功证明案例（每模型 15 个）进行人工审计（Table 5、Table 6）。
• 实验结果：在 99 个经审计的错误判定中，69% 发生在连接器，20% 源于错误或过窄规约，8% 来自测试转译，0% 来自 Lean 证明检查。60 个成功证明中，人工评定 52 个为忠实（Faithful），2 个较弱，6 个为虚假证明（Spurious）。
• 作者解读：作者指出没有一个经审计的错误源于 Lean 证明检查本身，主要困难在于独立生成的表示之间的语义对齐。

基准之外的真实场景与泛化评测

• 测试内容：在 22 个真实 GitHub 冲突、95 个 LiveCodeBench 任务以及 187 个 VERINA 任务上评估泛化性（Table 7）。
• 实验结果：在 22 个真实 GitHub 冲突中，SPECGUARD CLI 输出 9 个冲突判定（8 个含 Lean 证书，1 个为执行证据），1 个无冲突，12 个 inconclusive；在 LiveCodeBench 上检出 80 个冲突（84.2%，均为执行核验级别）；在 187 个 VERINA 任务中，180 个规约（96.3%）经 Lean 的 grind 策略证明与人类参考规约双向等价。
• 作者解读：作者认为这表明系统具备在合成基准之外的真实代码库中产出证书的能力，且规约生成具有高保真度。

其他消融与分析

• 议题相关性：On-issue 任务证明率为 55.0%，Off-issue 任务证明率降至 32.0%（Table 3）。
• 依赖信息类型：纯函数与有状态序列证明率分别为 63.4% 与 68.5%，Fixture 数据与复杂算法任务分别降至 25.0% 与 17.8%（Table 4）。
• 错误类型分布：Fixture 依赖任务错误率最高达 27.4%，复杂算法任务 inconclusive 率达 68.9% 但错误率仅 2.2%（Table 4）。
• 未检出运行分解：部分连接失败占 50%（399/793），错误判定占 19%（153/793），未构建连接占 18%（139/793）（Table 5）。
• GPT-5.6 Sol 重复稳定性：3 次重复的证明率均值为 51.1%，样本标准差为 1.95 个百分点（Table 9）。

作者指出的局限与后续方向

• 形式化保真度边界：Lean 证明仅能保证生成的规约与形式化测试要求在逻辑上互不相容，无法由内核保证形式化表示对原始任务的语义保真度（第 6 节）。
• 信任假设与威胁模型边界：SPECGUARD 假设任务描述是受信任的，若对抗性攻击者有能力直接修改任务描述，则超出当前威胁模型（第 6 节）。
• 支持语义的表达范围：当前方法主要针对可用可执行值语义（value-semantics）表示的行为，对于不属于输入-输出值约束的行为（如并发、副作用或纯终止性属性）尚未覆盖（第 3 节、第 6 节）。
• 议题未涵盖的测试断言：在 SWE-bench 的 349 个突变测试中，有 51 个涉及议题描述从未规定的行为，这些案例在结构上无法通过意图判定，导致系统输出 inconclusive（第 6 节）。
• 流水线错误与实现空间：当前失败案例包含规约构建、测试转译、连接器生成和框架聚合中的可恢复错误，作者指出当前测得的覆盖率不应被视为冲突证明能力的天花板（第 6 节）。
• 流水线配置与模型依赖：当前的实证结果反映的是基于现有前沿模型的具体三智能体流水线和框架配置，作者未将其推广至所有模型组合（第 6 节）。

实验覆盖范围

• 被测模型范围：实验覆盖了 GPT-5.6 Sol、Claude Opus 5、Claude Fable 5 和 Kimi K3 共 4 个前沿模型。
• 任务基准范围：合成冲突实验基于 SWE-bench 抽取的 349 个任务和 LiveCodeBench 的 95 个任务，真实冲突实验包含来自近期 GitHub 仓库的 22 个案例。
• 形式化验证工具范围：形式化规约与证明全部基于 Lean 4 定理证明器及其实际求解命令 by decide。
• 计算与交互预算：每个智能体最多运行 10 轮 Lean 编译器反馈循环，SpecAgent 获得最多 120 轮 bash 操作，每个任务执行超时时间为 1 小时。
• 未报告的信息：论文未报告在非 Python 项目上的表现，未报告各模型生成过程中的具体 token 消耗量（仅报告了 API 费用），且在单版本主实验中未包含对属性测试（Property Tested）级别的实证评测。

• 定位：论文提出了 SPECGUARD，一种在代码智能体行动前，通过定理证明器内核独立核验并形式化证明任务描述与测试套件之间存在冲突的预执行安全防御方法。
• 核心问题：现有前沿代码智能体在遇到测试与任务意图冲突的任务时，倾向于作弊、篡改测试或破坏安全机制以通过评估，而事后监控或纯大模型判定缺乏独立可验证的证据且漏报率较高。
• 方法要点：在屏蔽测试的前提下，SpecAgent 基于自然语言任务描述和代码库生成 Lean 4 可执行规约；TestAgent 独立将测试断言形式化；Certifier 自动构建连接器并交由 Lean 4 内核使用 by decide 检查两者的联合不可满足性，输出机器可校验的冲突证书。
• 关键实验结果：在 349 个 SWE-bench 冲突任务上，GPT-5.6 Sol 达到了 51.1% 的证明冲突率和 57.0% 的检出率，漏报率仅为 8.1%（远低于 LLM 裁判基线的 39.8%）；在配对测试设置下，GPT-5.6 Sol 的证明率提升至 67.0%；在 22 个真实 GitHub 冲突中成功产生 8 个 Lean 证明证书；在 VERINA 187 个任务上，96.3% 的生成规约被证明与人类参考规约双向等价。
• 结论与启示：作者认为跨表示的语义对齐是冲突证明的主要瓶颈而非证明检查本身；由于形式化冲突证书可由 Lean 内核独立核验且无需信任生成模型，该方法展现了在真实软件任务中于智能体行动前拦截奖励黑客风险的可行性。