2026-10-16
2026-10-16
固定证明义务，让验证器诊断成为可训练的代码智能体奖励
Verifier-Grounded Agentic RL for Provably Correct Code
局限与改进
代码智能体可能通过测试，却无法处理测试未覆盖的输入。相对于规格说明，形式化验证器提供了更强的判定依据；但如果所有候选方案都失败，二元的接受/拒绝信号就无法提供学习梯度。此前的 SWE-Proof 工作提供了带有形式化规格说明和经验证参考实现的真实问题任务；本文在方法上的增量是训练环境与奖励设计，而非基准构建。
每个回合开始前，环境都会为该实例固定证明义务的集合及其分母。智能体可以在多个轮次中向在线验证器提交候选方案并接收诊断信息。它获得的奖励是已履行义务的加权比例；对于标注修复任务，还会使用从参考证明注释中推导出的隐藏孤立断言。由于分母固定，添加琐碎注释或减轻候选方案自身的证明负担，不会直接提高得分。完整性审计拥有高于验证器的裁决权：若候选方案改动规格说明，或引入使验证逃离预期证明目标的结构，就会被拒绝。
受控证据说明了什么
最清晰的比较是在 DafnyBench 上进行的匹配二元奖励消融实验。对于 35B-A3B 模型，基于验证器的奖励在标注修复任务上达到 76.7%，而二元奖励为 75.2%；在代码生成任务上分别为 93.5% 和 71.0%。环境、超参数、训练步数以及按验证器评分的回合批次均保持不变，因此，与跨不相关系统的比较相比，这项比较更接近于单独检验候选方案奖励的变化。
在留出集 SWE-Proof 上的结果更显著，但回答的是另一个问题。对于同一 35B-A3B 模型，标注修复验证率从 3.1% 升至 68.8%，代码生成验证率从 56.3% 升至 100.0%。在另一项仓库补丁任务中，借助专家模型的设定将留出问题解决率从 59.6% 提高至 72.5%；问题是否解决由各项目的保留测试决定，并非只看验证结果。这些结果表明，应分别考察奖励设计和专家模型条件，而不应将其视为一个端到端效应。
如何用于新实验
应将审计视为第二种测量工具，而不是规格说明正确性的证据：验证能够确认实现是否忠实于给定契约；但契约是否表达了预期行为，仍由人负责。审计覆盖范围也取决于能否正确枚举所用语言中那些可规避验证的结构。
一项有用的复现实验操作是：固定环境、训练安排和验证器批次，只替换奖励，然后报告义务分母、隐藏探测策略和工件审计失败情况。最后，应谨慎解读这些比率：论文对每个实例只报告一次贪心回合，依据留出集验证率选择检查点，并指出留出划分仅包含 58–129 个实例。该结果提供了一套用于检验稠密验证器反馈的具体方案，而不是软件必然正确的一般性保证。
阅读本文，可以考察一项匹配的二元奖励消融实验：它将验证器诊断是否比通过/失败反馈更能提供有效的强化学习信号单独检验出来；同时也能了解完整性审计和单回合评估如何限制这一结论。
abstract; Section 3, The obligation ratio (S3.SS0.SSS0.Px1.p1); Hidden probes (S3.SS0.SSS0.Px2.p1); Section 4, Table 3 (S4.T3.2.4–5); controlled-ablation description in Section 4.5 (S4.SS5.p1); Section 4, Table 2 (S4.T2.6.8); Appendix E.3, SWE-Proof split (A5.SS3.SSS0.Px2.p1); Section 4, Table 4 (S4.T4.1.3); task and metric description in Section 4.6 (S4.SS6.p1–p2); Appendix I, Intended use and misuse (A9.SS0.SSS0.Px7.p1); Appendix C.3, What the two halves guarantee (A3.SS3.SSS0.Px4.p1); Appendix D.3, Reproducibility (A4.SS3.p2); Appendix F.1, Training curves (A6.SS1.p3) · Abstract; Section 1, paragraph 5; Appendix A, Table 4
回答重构博弈能降低越狱判定误差和波动，但会漏掉部分履行行为
Did the LLM Answer the Question? A Semantic Reconstruction Game for Jailbreak Evaluation
本文从一个具体的评估器失效问题出发：现有评估器可能将拒绝回答或仅在主题上相关的回答误判为成功攻击；仅更换裁判大语言模型，就能使报告的 ASR 改变至多 82 个百分点。本文的贡献比首次提出实质性履行评估器更为有限：FJAR 先前已使用针对查询的锚定参考答案和分阶段判定来评估履行情况。本文的独特改动，是将仅基于回答的重构，而非针对查询的锚定参考答案，作为核心测试。
在只看到一条回答的情况下，第一个大语言模型会重构一个简洁请求，以实质性内容表示该请求，并排除重复、具名或遭拒绝的内容。第二个大语言模型会生成五个语义相近的干扰项，它们在请求的动作、信息、结果或方向上有所不同。裁判会收到原始请求以及顺序随机的重构项—干扰项配对，选择匹配的候选项；若两者都不匹配，则弃权。弃权会计入对重构不利的结果；如果重构项赢得多数比较，就会标记为越狱。因此，这种操作性信号衡量的是语义可恢复性，而不是直接判断有害性。论文分析明确提出了其核心假设：履行请求的回答通常应使请求可恢复，而未履行请求的回答通常应使请求不可恢复。
在两个由人工标注的基准上，该博弈方法在所有评估方法中的平均 MAE 最低。在指定的基准条件下，使用三个现成裁判时，该方法在 StrongREJECT 上的平均 MAE 为 0.147，而普通裁判判定为 0.181；在 HarmBench 上分别为 0.224 和 0.389。在针对 Qwen2-7B-Instruct 测试的五种攻击中，该博弈方法在基于大语言模型的分类器中 ASR 波动幅度最小，但波动仍为 12–28 个百分点；对于 I-GCG，普通裁判的 ASR 范围为 6% 至 88%，而博弈方法的 ASR 范围为 36% 至 48%。这一比较需要谨慎看待，因为每次攻击运行都将其评估器用作循环内裁判，因此裁判也影响了攻击生成。
SorryBENCH 展示了这种保守取舍：该博弈方法在拒绝、具体拒绝以及附带安全替代方案的拒绝类别中的平均 MAE 分别为 0.000、0.012 和 0.011；但在不完整回答和实质性成功回答类别中，分别为 0.519 和 0.425。这一模式与论文估算的履行—可恢复性差距一致：不完整回答可能履行了请求，却没有暴露足够内容供重构。复现实验中一个具体的问题是，改变干扰项数量是否会改变召回率和假阳性；论文使用五个干扰项，但没有对其数量进行消融。方法能否迁移仍不确定：实验使用小型的 8–12B 裁判模型和小型攻击目标，不涉及思维链轨迹、多轮越狱或多智能体交互，也未证明其能抵抗针对评估器判决优化的攻击。实际启示是，应将可恢复性和履行情况作为两个独立指标报告，而不是把该博弈方法的标签视为真实情况。
阅读本文，可以了解如何在报告越狱 ASR 时，将语义可恢复性与有害请求的履行情况区分开来，以及如何依据人工标签和裁判差异检验这一选择。
abstract; Section 6.2; Tables 3–4; Section 6.3; Table 5 · Section III-A, Anchored Reference Generation; Section III-B, Evaluation Process
当错误答案的得分尾部超过正确答案时，Best-of-N 可能适得其反
Tail Competition Explains Scaling in Best-of-N Sampling for Verifiable Problems
Best-of-N 不仅关乎采样是否产生了正确候选答案。本文将选择过程视为一场竞赛：正确候选答案中的最高奖励，与错误候选答案中的最高奖励相互较量；只有前者胜出，选择才算成功。其极值分析区分了正确答案尾部占优、错误答案尾部占优和临界三种情形，从而解释性能为何既可能随规模提升，也可能下降。
所提供的比较中，先前工作已经研究了推理时的代理奖励投机，并提出 HedgeTune；其原则性校准需要真实奖励反馈。本文的实际改进是根据无标签的逐查询奖励分数诊断选择风险，而不是依靠真实奖励反馈。具体而言，作者拟合双成分高斯混合模型，将均值较高的成分作为正确回答的代理，将均值较低的成分作为错误回答的代理，估计领先阶交叉预算；当均值较低的成分方差更大时，在达到该点后停止采样。
高斯分析给出了决定性条件。即使正确回答的平均得分较高，只要错误回答的方差足够大，随着采样预算增加，其上尾最终仍会占优；论文将这种非单调情形解释为奖励投机。这比平均分差异提供了更精确的诊断：应测量哪一类在最大值比较中更有竞争力，而不只是看哪一类的平均分更高。
报告的证据与这一机制相符，但结论仍有条件限制。在真实分数统计中，正确回答通常平均分更高，而错误回答往往方差更大，但也存在例外。关于提前停止，附录 B.2 报告了一项具体设定：在计划的 n=8192 时，Skywork Qwen3-1.7B 将计算量减少 27.6%，并将被投机子集上的准确率从不停止时的 0.0366 提高到停止时的 0.0792。论文也指出，当准确率单调提升时，停止可能并非最优选择。
不要将这条规则视为通用验证器控制器。该框架针对可验证问题；对于非双峰或明显偏离高斯分布的分数、错误答案平均奖励更高的情况，或可靠地识别有限预算下所处机制的情形，这一启发式方法均未得到验证。一项有用的研究操作是在新的验证器上拟合混合模型并估计交叉点，随后在该预算两侧测试准确率和成本，同时检查混合模型的各成分是否确实与正确性相对应。
阅读本文，可以检验验证器的得分方差是否标示出这样一个节点：继续增加 Best-of-N 样本不再有帮助。
abstract; Section 3.2, Example: Gaussian distribution, Eq. (6) and surrounding text; Section 5, Eqs. (15)–(17); Section 6, Effectiveness of the proposed early stopping method; Appendix B.2, table of full early-stopping results; Appendix B.3, Table 3 caption and score statistics; Section 8, Limitations and Future Work · abstract; Section 4, paragraph 1; Section 5.2
在所测试的 JEPA 设定中，更高的单步保真度并不能可靠预测规划收益
One-Step Prediction Fidelity Is a Poor Proxy for Planning Performance in JEPA World Models
单步预测损失是一个很有吸引力的检查点指标，但它衡量的目标是模型自身的嵌入，而不是可解释的物理量。因此，它可能同时包含编码器表征中已有的误差，以及动力学预测器新增的误差。本文将这一局限转化为一项测量实验：刻意提升单步保真度，是否也会改善目标条件规划？
作者提出的流程是：拟合一个解码器，将真实观测的编码器嵌入映射到模拟器状态；冻结该解码器；随后在独立的测试回合中，分别评估解码后的真实下一状态和解码后的预测潜变量。误差以物理单位归一化。报告分别列出表征误差、预测误差和超额误差；后者旨在于编码器/解码器贡献占主导时，识别预测器额外引入的误差。作者还用一种无需解码器的指标——潜变量漂移——重复分析。他们通过从检查点出发进行热启动微调来改变保真度，并使用三个训练随机种子和配对的规划随机种子评估规划表现。
最清晰的证据来自 PushT 检查点序列。第一个训练轮次使保真度提升了 32.0%，规划表现提升了 4.44 个百分点。此后，在接下来的 15 个检查点中，保真度持续单调改善，但单步误差与规划成功率之间的相关性约为零（r = -0.010）。这并非任务已达上限所致：最低支持度数据分层中的规划表现起始值为 80%，仍有提升空间；然而，从第 1 个训练轮次起，即使保真度持续改善，规划表现仍保持平稳。不同环境之间，数值上的对应关系也不稳定：在 TwoRoom 中，预测误差降低 93%，对应的规划表现却下降 -0.7 个百分点；在 PushT 中，预测误差降低 40%，对应的规划表现则上升 +4.9 个百分点。这些百分比仅用于说明，并非可在不同任务间直接比较。
一项匹配的继续训练对照也吸收了原本归因于辅助状态对齐目标的保真度提升；测得的两组效应无法区分。因此，实际操作中应将单步损失视为诊断指标，而非部署效果的替代指标：冻结一个与任务相关的解码器，分离表征误差与预测器误差，并在实际规划目标上评估匹配的检查点。
结论的适用范围相当有限。本研究评估了一个 15M 参数架构、三个低维模拟环境、一个规划器，以及从同一检查点系列出发的热启动微调。其核心的任务内结果只涵盖第 1 个训练轮次之后有限的保真度变化范围；作者还指出，三个训练随机种子使得小效应难以辨别。该结果是在这一测试设定下对检查点选择的提醒，而不是关于所有世界模型的普遍结论。
如果你用单步预测损失选择世界模型检查点，可以读这篇论文：它提供了一种以物理单位衡量的具体诊断方法，并展示了一个受控案例，其中持续提升的保真度并未与规划表现同步。
abstract; §1, contributions; §3.1–3.2
P2Patch 将补丁后确认的漏洞利用转化为累积修复要求
P2Patch: Exploit-Guided Vulnerability Repair
局限
本文针对一项具体的验证局限：修复智能体往往依据构造补丁时使用的同一证据来验证补丁，例如静态告警、消毒器跟踪、已公开的漏洞利用或测试套件。因此，只要阻断了这些证据所代表的攻击路径，同一漏洞的变体仍可能可以利用。
方法改进
P2Patch 将一次性验证改为自适应的攻击与修复循环。流程从一项标准化漏洞发现开始：漏洞利用智能体构造可复现的漏洞证明（PoV），补丁智能体修复程序，随后漏洞利用智能体再攻击已修补的程序，寻找同一漏洞的另一种利用方式。每个经执行确认的绕过都会成为永久修复要求，而构造阶段的 PoV 则与留出评估预言机分开处理。
随附的 VulnRepairBench 包含 101 个 CVE，覆盖 60 个 Java 和 41 个 C/C++ 研究对象、61 个代码仓库和 20 类弱点。其留出设计区分了官方修复所阻断的攻击路径，以及修复后仍可复现的候选攻击路径。
关键证据
在主要配置中，补丁已经阻断其引导 PoV 后，对抗阶段仍在 41% 的运行中找到了至少一种经确认的绕过。与使用 Claude Code、依据同一漏洞发现进行的单轮修复相比，在基准的评分规则下，P2Patch 将修复闭合覆盖率从 78.1% 提高到 84.7%，并将超越上游修复的覆盖率从 42.1% 提高到 62.5%。报告中的消融实验将可检测到的覆盖率提升归因于对抗式加固，而非仅仅归因于引导 PoV。这一改进的代价是平均每个研究对象花费 $2.09，而单轮修复为 $0.45。
可借鉴之处，以及不应得出的结论
一项可迁移的研究操作是：将每个经执行确认的反例视为一项新的验收要求，在修复过程中累积这些要求，并为最终评分保留一套独立测试。这样就能将评估问题转化为可操作的检验：系统能否改进它在修复过程中未使用过的攻击路径？
这些结果仍属于有边界的测试证据，并不能证明补丁完整。留出测试套件经过人工整理且并不完备；论文报告称，后续上游修复印证了 14 个残余案例，而仅有 8 个案例在后续代码树上的闭合情况得到验证。除拒绝重复命令外，语义上的差异性并未经过机器检查，因此作者指出，41% 的绕过率是对真正不同攻击路径比例的上界。
阅读本文，可以了解如何将可执行反例纳入修复目标，同时避免在最终评估中重复使用同一证据；文中报告的消融实验和留出预言机设计，使这一流程可以直接在新的修复系统中检验。