2026.10.22

改动

APRIL 提供的评估是单次执行，不含搜索或迭代，因此没有检验修复是否能融入定理级采样。本文则将一个预训练修复模型置于 Lean 证明搜索内部。每一步，系统都会采样 K 个候选策略；当 Lean 拒绝其中一个时，系统便将编译器错误反馈给修复模型，在原处修正被拒绝的策略，最多尝试修复 R 次。R=0 时即为仅采样的基线。因此，关键设计选择是明确的计算资源分配：将计算用于生成新策略，还是用于受诊断信息引导的修正。

测量结果

在包含 1,990 个定理的 LeanDojo 子集上，同一 K 值下的比较显示，Pass@1 提升 2.3–4.1 个百分点，净增成功求解的定理 45–82 个；比较范围为 K ∈ {1, 3, 5, 8}。在报告的扫描实验中，首次修复贡献了大部分、但并非全部的净增收益：它占三次尝试所得总收益的 84–96%。失败分析进一步限定了可能机制。对于某些局部策略失败，修复成功率高于类型不匹配；这与论文报告的结论一致，即收益主要来自浅层的策略执行失败，而非结构性错误。

这一结果并不局限于该基准配置。在 Lean Workbook 上，报告的验证集求解率从 21.4% 升至 42.9%，留出测试集求解率则从 19.1% 升至 31.5%，对应 R=2；在这一比较中，两个数据划分上的结果均未低于基线。但修复代价高昂：在 K=8 时，R=3 下每个定理的平均耗时从 200.5 秒增至 485.7 秒；论文指出，增加的延迟可能会在 600 秒超时限制下导致性能回退。作者还报告，在每个定理的运行时间相同的情况下，一次修复通常能提高覆盖率，同时指出存在预算极紧时的例外，并且测量结果受噪声影响；本文未独立审查图 4 中作为依据的曲线。

可借鉴的研究操作

应将修复视为一种有条件的计算策略，而非必然有益的附加阶段。对于新的证明器，应运行 K × R 网格实验，分别报告候选数量预算相同和实际运行时间相同的结果，按编译器失败类别分层统计恢复的尝试，并记录超时导致的性能回退。论文中的每个数字都来自单次确定性运行，因此在对方差或稳健性作出判断之前，这一实验方案还应加入重复随机种子或重复运行。可迁移的问题是：在每种预算下，哪些被拒绝的策略属于足够局部的失败，以至于利用编译器反馈修复它们，比再采样一次成本更低？

隐私审计通常使用成员推断攻击（MIA），在选定的置信水平下估计机制隐私泄露的下界，再将该下界与机制差分隐私（DP）的理论上界进行比较。论文的核心警示有明确条件，但影响重大：如果审计在检查同一批用于估计错误率的观测数据后，才选择 MIA 阈值——或者在单次运行审计中才确定猜测次数——那么固定阈值置信程序就无法维持其名义覆盖率。这是认证步骤中的选择偏差，并非攻击本身发生了变化。

在方法上，论文将固定阈值 MIA 视为假设检验，估计其假阳性率和假阴性率，并通过反演 DP 权衡关系得到置信下界。随后，论文调整并采用已有补救方法：留出集选择、对预先指定的有限阈值网格进行 Bonferroni 校正的界、多次运行审计中基于 DKW 的阈值同时界，以及 K 折选择。对于单次运行审计，由于金丝雀分数观测之间存在依赖，DKW 方法不可用；固定猜测数、经校正的有限网格界、留出集和 K 折仍可选用。该校正建立在现有的 MIA 到界限流程之上，因此实际操作的关键在于选择与审计方案相匹配的选择程序。

覆盖率实验提供了决定性的诊断。在参数已知的高斯模拟中，每种设置进行了 10,000 次独立审计，名义置信度为 95%；在 μ0 = 2、n = 10,000 时，未校正的阈值最大化导致 19.36% 的案例未覆盖，而所测试的有效方法中这一比例均低于 5%。在对选定真实模型审计进行的重新分析中，根据审计和有效方法的不同，校正使报告的界限降低了 5% 至 93%；作者提醒，这一差异同时反映了选择偏差和有效方法的保守性。

对于研究者，可迁移的操作很简单：应将“选择最佳阈值或猜测次数”视为推断的一部分，而非无害的调参；在将所得界限解读为反对 DP 保证的证据之前，应预先指定校正方法。被抬高的界限可能会错误地将符合要求的机制判为违规，而有效的选择程序则可在所述置信度解释下排除这些误报。边界同样重要：真实模型的重新分析比较的是界限数值，并未确立经验覆盖率；所评估的有效程序具有保守性；且没有任何校正在所有设置中都占优。K 折被提出作为一个合理的默认方法，而非普遍最优的方法；此外，在假阳性率极低的区域，DKW 方法可能过于宽松。

评估方式的改变

本文针对的具体局限是：针对当前问题进行压缩后，当前问题上的得分并不能可靠反映压缩内容对后续问题的帮助。因此，作者将评估目标从仅考察已知问题，改为考察压缩时尚未揭示的问题。

实验方案

作者使用四个语料库，这些语料库为每段文本标注了多个问题对应的证据，并结合记录下来的智能体轨迹；在指定的条件下，将不同压缩策略与随机删除进行预算匹配比较。删除时，当前问题可见，后续问题则保持隐藏。评估结合了答案准确率、证据保留情况和支持度检查。在轨迹测试中，后续问题要求提供后续工具调用所需的标识符。

发现

在 MultiRC 上，相比随机删除，为当前问题选取句子能提高该问题上的表现；但在匹配的 25% token 预算下，未检测到其对后续问题的平均收益。平均结果无差异掩盖了方向相反的结果：类型化选择有利于与已知问题共享证据的问题，却不利于证据不相交的问题；这一划分是事后进行的。

改变删除单位会改变结果。在后续 MultiRC 问题上，LLMLingua-2 在 token 数相同的条件下比随机删除句子高 12.5 个百分点；但在内容词保留量相同的条件下，差距缩小至 7.3 个百分点。后者分析具有探索性，不能证明因果关系。在 FEVER 上，类型化选择虽然提高了主张标签准确率，却未伴随标注推导出的支持度评分出现可检测的提升，这说明标签恢复可能会夸大保留文本实际能够支持的内容。

排名取决于具体条件。在名义上的 25% 预算比较中，类型化选择在 Evidence Inference 的隐藏主张上优于 LLMLingua-2，但保留的 token 数量并不相同。在所测试的零售轨迹中，类型化选择在后续标识符问题上的表现显著优于随机删除，而 LLMLingua-2 未显示出可检测的收益。

研究操作

对于新的压缩评估，应在写入时隐藏未来问题，与 token 数量匹配的随机删除进行比较，并同时评估答案恢复情况，以及保留文本是否包含标注的支持证据。按证据重叠程度对隐藏查询分层，有助于发现汇总得分是否掩盖了不同的失败模式。

边界

这些结果证明的是基准测试和记录轨迹中的表现，并非实时智能体或部署环境中的性能。内容词机制仅能解释部分结果，且具有探索性；证据保留和基于支持度的评估也受限于标注不完整。因此，报告的选择策略排名应被理解为仅适用于所测试的数据集、策略、预算和任务类型。

一个序列中的每个动作都可能在局部获得授权，但其执行仍可能违反涉及意图、目的、来源、同意或委托的策略。论文将此称为组合式授权失效（CAF）。其中具体的组合缺口在于，有些目的违规具有关系性：只有比较不同执行过程时才会出现相关证据，而不是通过更仔细地检查单条轨迹就能发现。

所提供的既有设计采取了不同的局部措施。Fides 在模型查询过程中传播标签，并在工具调用执行前依据策略进行检查。RTBAS 筛查相关历史区域、对限制更严格的区域进行删减，并依据策略检查拟议的工具调用。SafeFlow 将运行时流控制与事务日志结合起来。本文将分析单位从单条动作轨迹改为针对多个执行过程的策略，但并未声称这些早期机制能够应对所有可能的全局策略。

形式上，论文依据表达能力——单轨迹安全与关系型 k-安全——以及可观测性（使用一系列监控器配置）来刻画 CAF。对于关系型目的违规，论文证明：若逐轨迹监控器从不误报，就无法检测到任何此类违规。这种监控器必须比较不同执行过程，或接受误报。为使这一边界可以检验，AL-Synth 使用 SAT/SMT 有界模型检查和自组合来合成最小、局部已获授权的见证，再将求解器结果与小规模模型及有界时域上的穷举预言机进行比较。

关键演示是评审模型研究。在九个 LLM 评审模型中，有八个在逐动作、每种情况下重复 0/30 次的设置下都拦截不了合成的关系型见证；当同时展示两种执行过程时，其中八个在 30/30 次中标记了该见证，而 Llama-4-Maverick 标记了 17/30 次。这衡量的是报告设置下评审模型的行为，并非自主智能体的漏洞率。另一个日历实验展示了互补情形：在所测试的 Qwen3-30B 任务中，具备组合感知能力的同意保护措施消除了累积同意失败，而仅基于意图的保护措施并未显示出可测量的减少。

定理比经验层面的推广结论更强：这些演示使用干净的符号模型和合成任务，AL-Synth 的验证具有有界性；六种机制的防御矩阵是根据已发表的设计推断得出，而不是通过运行这些系统获得。由此可直接得出一种有用的评估操作：将策略中的每个合取条件归类为轨迹级或关系型，生成单次运行和成对运行测试，并避免将逐动作拦截率为零视为关系型策略已获认证的证据。

与 AgentCheck 文档所述的“复现—干预—缓解”工作流相比，RITE 增加了一个由正确值、静默错误和显式失败组成的匹配检查点，以及端到端任务/过程分解；所提供的比较并不能证明 AgentCheck 缺少其他控制措施。

RITE 根据九种电子商务工作流和源自生产日志的输入，构建了 167 个“槽位—位置”单元，得到 501 个匹配实例。每个单元在三种条件下都保持查询、所需结果、检查点历史和后续环境不变。在受影响的检查点，静默条件会插入一个看似合理、符合模式但与任务要求不符的值；记录下来的工具行为在重放期间保持固定，智能体则可自由继续执行。

关键结果体现为端到端差距，而不仅仅是检测差距。在温度为 0、步数预算为 25、且排除环境侧工具异常的条件下，十个模型在正确条件下的 RSR 为 0.716–0.827，而在静默错误条件下为 0.277–0.403；隐式条件下的保持率为 0.345–0.526。过程指标揭示了连续出现的失败环节：在未察觉的运行轨迹中，最新的生产者观测与金标准值相符的比例为 0.3%；在已察觉的运行轨迹中，这一比例为 23.3%，但已察觉的运行轨迹中仍有 57.8% 保留了受污染的值。在重新获取生产者结果的 147 条运行轨迹中，87 条恢复了金标准值，60 条既不匹配金标准值，也不匹配受污染的值；即便是在已察觉错误后重新获取结果的运行轨迹中，RSR 也只有 0.655。

可迁移的研究操作是：将恢复过程作为三个相互关联的关口加以度量——识别、来源核验，以及最终使用修正后的证据——并在相同检查点下分别评估每个关口与最终任务成功之间的关系。这比“智能体是否重试？”提出了更明确的工程问题：修正后的证据是否真正传递并用于答案？

需要注意其适用边界。每个静默错误实例只包含一个被破坏的值，且重新查询其生产者会返回未受污染的响应；因此，RITE 并未证明系统能够抵御持续性或相关性故障。时间陈旧性虽有定义，但没有在实验中实例化。证据来自九种内部工业电子商务工作流，因此能否迁移到其他领域和工具生态尚未确定。最后，RSR 使用 LLM 评审；人工验证显示，在 Result 项上，100 个样本中有 76 个获得多数一致，Cohen’s kappa 为 0.318，因此绝对成功率应谨慎解读。