所有 Wiki 查询均未返回结果。OMC Wiki 不包含有关软件验证主题的知识。paper-wiki 数据库侧重于音频/语音领域，因此没有匹配项。我已经阅读了完整的论文。现在我将输出审阅结果。

论文审稿：Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

论文类型: 方法型

本文提出了一种新的回归验证方法，将基于 LLM 推断的部分契约与基于假设-保证（assume-guarantee）的模块化等价性检查相结合，并附带一个语义契约紧密度比较器。核心工件是一个三工具流水线 (CONTRACTOR/SCRIBE/REGVER) 以及两个定理 (T1, T2)，属于方法型论文，但也具有很强的分析成分 (RQ2 紧密度饱和度)。

公理审查结果

公理一：对象公理

• 判定: ✅
• 依据: 回归验证是一个真实且长期存在的问题。论文正确地指出，全程序推理成本过高，手动编写规范很少见，且全等价对于错误修复而言要求过于苛刻（它保留了旧错误）。条件（回归）等价——仅在旧版本满足的属性上要求一致——是一种标准且经过充分研究的松弛 (Godlin & Strichman [3,7], Lahiri et al. [12,13])。目标对象——部分调用者充分契约作为被调用者抽象——定义清晰（定义 3, 5），操作清晰，并解决了真实的工程缺口：没有现有的工具将 LLM 推断的契约重用为双版本回归等价性证明中的被调用者抽象。论文明确指出了三个独立假设 (A1: 终止，A2: 帧规则可靠性，A3: 验证器可靠性) 并在适用处对其进行检验。声称的范围与实验验证范围一致：小规模 C 程序 (Frama-C-Problems ~17 LoC, X509 六个函数, EqBench-C 精心构造的例子)。
• Wiki 证据: OMC wiki 无记录（查询 “regression verification”, “contract-based regression verification”, “partial specification modular verification” 均返回空）。paper-wiki 数据库仅覆盖音频/语音，不覆盖 cs.SE。此空白本身确认了该主题不在本地知识库中，但回归验证是一个公认的研究领域，有着成熟的基准 (RVT, Reve, SymDiff, ARDiff)。

公理二：识别公理

• 判定: ⚠️
• 依据: 论文将 SCRIBE 与三个相关基线进行了比较：AutoSpec [4]、Preguss [6] 和 “Specify What?” [5]，以及 AutoDeduct [30]。然而，这种比较是基于已发表数字的单向比较，而非重新运行——作者承认这一点（“外部有效性：单向（已发表数字，而非重新运行）”）。不同的工具针对不同的成功预言机（AutoSpec：功能正确性；Preguss：RTE 自由度；SCRIBE：强制执行 + 调用者充分性），因此这种比较是“情境化的”而非正面对比。最令人担忧的是：在 X509 上，SCRIBE 达到了 5/6 (Opus/Kimi) 和 3/6 (Qwen)，而 AutoSpec 报告为 6/6，但函数集“相似但不完全相同”，因此这并非严格的同类比较。在等价性检查方面 (EqBench-C)，作者明确表示不对可比检查器 (RVT, Reve, ARDiff, SymDiff) 进行跨工具数字排名，理由是它们针对的是部分等价而非安全保留的条件等价。这是诚实的，但也意味着回归验证本身没有直接的竞品基线——只有将 EqBench-C 用作健全性检查（零假证明），而非用于效用比较。关于部分契约 为何 足够的因果机制已通过定理 T1（契约只需在属性观察到的输出片段上精确）和 RQ2（紧密度饱和）进行了隔离。没有进行消融实验来分离单个 LLM 反馈模态与随机基线，但三种模型的趋同结果（近乎相同的细化遥测数据）提供了一些稳健性证据。
• Wiki 证据: OMC wiki 对 “regression verification baseline” 和 “LLM contract inference ablation” 查询返回空。无法通过 wiki 交叉验证基线完整性。论文中提到的基线 (RVT, Reve, SymDiff, ARDiff, AutoSpec, Preguss, “Specify What?”, AutoDeduct) 覆盖了该领域的已发表文献。

公理三：独立性公理

• 判定: ✅
• 依据: 评估流水线具有清晰的独立性边界：(1) EqBench-C 是一个第三方数据集 (Badihi et al. [51])，并非由作者构建。(2) 回归健全性检查 (REGVER) 使用数据集标签作为基本事实，但健全性问题——REGVER 是否会产生虚假等价？——完全由验证器的可靠性（假设 A3）和数据集标签决定，两者均独立于 SCRIBE 的契约推断过程。(3) 契约推断循环使用 ESBMC 的反例作为反馈，这些反例由形式化验证器产生，而非由 LLM 自身产生——这是一种清晰的生成器-判别器分离。(4) 紧密度比较器 (JUDGE) 将契约比较为纯 SMT 有效性查询，不涉及函数体，在保持其后验的同时，不干扰推断循环。一个细微的关注点：在 Frama-C-Problems 上，SCRIBE 既进行推断又在其上进行评估，但评估标准是“契约是否通过 ESBMC 的强制执行和替换？”——这是一个独立的形式化预言机，而非 LLM 自我评判。发现的九个 EqBench 错误标签已提交至上游 (GitHub issue #15)，这是独立于作者自身结论的第三方验证。
• Wiki 证据: OMC wiki 对 “EqBench judge independence” 和 “synthetic data human validation” 查询返回空。论文关于第三方数据集和形式化验证器预言机的声明，根据其描述的方法论来看是可信的。

公理四：压缩公理

• 判定: ✅
• 依据: 该方法具有理论上的简洁性：核心见解是定理 T1，它证明对旧版本进行单边部分契约抽象对于回归等价性是可靠的——契约仅需在调用者观察到的输出片段上精确，其他地方可以保持宽松。这是一个真正的问题重构：与之前的回归验证工具需要被调用者的完整特征 (RVT 的未解释函数，Reve 的耦合谓词，SymDiff 的关系摘要) 不同，这种重构表明仅需调用者足够的契约即可。深度有界的契约闭包 (引理 L1) 是一种标准的归纳提升，并非新的复杂度增加。该流水线有三个工具，但每个工具都有明确且不重叠的作用 (脚手架 -> 推断 -> 验证)。JUDGE 紧密度比较器是一个独立的贡献 (C3)，解决了真实的评估缺口（先前的工具按语法计算注解数量，这可以通过简单的后置条件来膨胀）。论文没有命名膨胀——“调用者充分”、“安全保留的条件等价”和“契约紧密度”是精确、标准且承载语义的术语。RQ2 结果表明，部分契约已经捕获了几乎所有的可达到紧密度（18/20, 13/15, 14/18 等价对），这是一种可迁移的经验压缩：在调用者充分性处停止几乎不牺牲任何东西。
• Wiki 证据: OMC wiki 对 “contract subsumption” 和 “assume-guarantee partial specification” 查询返回空。论文中与现有工作的对比 (§III) 明确指出：“这项工作与上述所有工作的两个差距。首先，每个此类工具都针对单一版本；没有工具将推断出的契约重用为两版本回归等价性证明中的被调用者抽象，这正是我们要填补的差距。其次，它们通过契约是否通过验证来判断规范，而不是其紧密度。”

公理五：效用公理

• 判定: ⚠️
• 依据: 论文结果在各项指标上均有体现，但在绝对效用上存在显著的局限性：

RQ1 (契约推断)：在 Frama-C-Problems 上，SCRIBE 达到了 70.6%/85.7% (Opus), 78.4%/85.1% (Kimi), 70.6%/81.8% (Qwen) 的决定性/保守成功率，而 AutoSpec 为 60.8%，Preguss 为 79.7% (三次平均值)。这相当具有可比性，但 Preguss 的数字是基于三次运行的平均值，而 SCRIBE 是单次确定的运行。在 X509 上：5/6, 5/6, 3/6 对比 AutoSpec 的 6/6——SCRIBE 并未明确超越 AutoSpec。因此，在契约推断方面，SCRIBE 具有可比性但不卓越。

EqBench-C 健全性：在 272 对中，仅决定了 70 对 (25.7%)——这是一个低到达率。契约将决定数量提高到 105/106/102 (38.6%)，但代价是高误报率 (40/39/38 FP 对比 65/67/63 正确)。因此，契约扩展了范围，但在约 38% 的恢复决策中是误报繁重的。作者将其描述为“可分拣的过度近似而非回归”，这很诚实，但这意味着该方法在等价性检查方面的实际效用是有限的——大多数对超时或产生误报。

RQ2 (紧密度)：一个严重的警告是，约 40% 的轮次比较涉及 JUDGE 无法排序的量化或指针解引用后置条件。因此，饱和度声明仅适用于约 60% 的可比较目标。在那些可比较的目标中，部分契约与强化契约的等价性很高 (18/20, 13/15, 14/18)，但外部的 40% 是未知的，而非已验证的等价。

基准非常小：Frama-C-Problems (~17 LoC)，X509 (六个函数)，EqBench-C (精心构造的例子，非生产代码)。作者在“外部有效性”中诚实地指出了这一点。在实际规模上的效用尚未证明。

• Wiki 证据: OMC wiki 对 “regression verification SOTA” 和 “equivalence checking baseline” 查询返回空。paper-wiki 无相关条目。无法通过 wiki 独立验证 SOTA。基于论文自身的相关工作部分，基准覆盖了已发表的工具 (AutoSpec, Preguss, RVT, Reve, SymDiff, ARDiff)，但比较是单向的（已发表数字，而非重新运行）。

公理六：新颖性公理

• 判定: ✅
• 依据: 新颖性主张是明确且有充分依据的：

1. “第一个基于契约的回归验证工具”——经过交叉验证：相关工作调查 (§III-A) 涵盖了 RVT, Reve/LLREVE, SymDiff, DAC, ARDiff, PEQcheck, PEQtest, PASDA，以及基于 LLM 的测试工具 (Mokav, UnitTenX)。这些工具中没有一个使用 LLM 推断的契约作为被调用者抽象来进行回归等价性证明。基于影响摘要的回归验证 (Backes et al. [26]) 通过路径条件约束将证明限制在更改相关的行为上，但需要全程序符号执行并生成与特定差异绑定的摘要，而非可重用、可强制执行的契约。

2. 单边部分契约 (定理 T1)：先前的工作需要被调用者的完整特征（RVT 使用未解释函数，Reve 使用耦合谓词，SymDiff 使用关系摘要）。对旧版本进行单边、属性相对、调用者足够的抽象——在新版本上具体运行——是一个真正的重构，直接实现了 LLM 推断（契约保持足够小以供模型猜测）。

3. 语义契约紧密度比较器 (JUDGE, C3)：先前的 LLM 契约工具按验证成功或语法注解数量进行评估。JUDGE 通过在允许集上使用带有反例见证的决策过程定义了集合包含的紧密度——这是一个真正的新评估贡献。

4. 来自验证器反例的自动契约推断：CE 引导循环本身是建立的 (CE-GIS [44-47], 用于不变量的 LLM 循环 [36-43])，但将其应用于回归验证环境中的函数级帧条件，并由 BMC 追踪反馈而非 WP 级别的 VC 失败驱动，是一个有意义的改编，而非简单的重命名。

由 LLM 提出并由验证器认证的组件并非微不足道的 A+B+C 组合：定理 T1 将契约可靠性专门与回归等价性证明的调用者充分性联系起来，这是使得部分（而非完整）规范足够的关键见解。

• Wiki 证据: OMC wiki 对 “LLM contract inference first new” 和 “regression verification contract” 查询返回空。论文对 AutoSpec [4] (CAV 2024), Preguss [6] (OOPSLA 2026), “Specify What?” [5] (IFM 2025), ConVer [29], 以及其他 LLM 契约工具 [27,28,35] 的引用涵盖了相关领域。没有发现 2 个月内的同期工作。Sarker et al. [25] 被标注为同期工作（差异符号执行，正交方向），作者对此进行了正确比较（9 个错误标记对比 5 个）。

公理七：可复现公理

• 判定: ⚠️
• 依据: 论文未提及代码发布或公共仓库。这三个工具 (CONTRACTOR, SCRIBE, REGVER) 被描述了架构，但未提供 URL。实验使用了三个 LLM (Opus 4.8 [54], Kimi K2.6 [55], Qwen3.6-27B [56])——Opus 是闭源的，Kimi 和 Qwen 是开源权重的。形式化验证器 (ESBMC 配合 Z3) 是开源的。使用了标准基准 (Frama-C-Problems [53] 是一个公共 GitHub 仓库，EqBench-C [51] 是公共的，X509 解析器带有手动验证的 ACSL)。评估参数已明确说明：温度为 0，300s 超时，5 次细化迭代，104GB 内存限制，k-induction 且无展开界限。这种详细程度原则上允许复现，但如果没有发布的代码，独立验证需要从头重建整个三工具流水线。EqBench 的错误标签发现已提交至上游 (GitHub issue #15 [57])，这为数据集问题提供了可验证的工件。作者在致谢中承认使用了生成式 AI 工具进行开发和稿件准备，但声明所有内容均由作者审查和验证。
• Wiki 证据: OMC wiki 对 “code release” 或 “reproducibility” 查询返回空。论文未明确指出代码可用性，这将其可复现性降低至 ⚠️。

日报摘要

• Strength: 定理 T1 形式化证明了单边部分契约对安全保留条件回归等价性是可靠的，且 RQ2 显示该部分契约在可比较目标中已达到近乎完全的紧密度（18/20, 13/15, 14/18 等价于强化版本），验证了部分规范停止点的合理性。
• Weakness: EqBench-C 上仅决定 25.7% 的配对（70/272），即使加入契约也仅 38.6%，且恢复决策中约 38% 为误报；全部基准为小规模（~17 LoC 或六个函数），缺少生产代码或跨工具公平重跑对比。

总评

• 科学价值: 中 — 定理 T1 和 T2 是该领域内真正的形式化贡献，提供了先前工作未曾建立的“调用者充分部分契约对于回归等价性是可靠的”的证明。紧密度重构为集合包含提供了一种语义而非语法度量。然而，证明相对直接（T1 是单页归纳），且假设 (A1-A3) 虽然标准但限制了范围。
• 方法价值: 中 — 三工具流水线设计良好，关注点分离清晰，且反例驱动的 LLM 推断循环原则上是合理的。然而，单向基线比较（已发表数字，而非重新运行）、不同的成功预言机以及不匹配的函数集 (X509) 削弱了效用证明。EqBench-C 上的低到达率 (25.7%) 和契约恢复决策中的高误报率（约 38%）限制了实际效用。
• 社区价值: 中高 — “第一个基于契约的回归验证工具”填补了 LLM 契约推断和回归验证社区的真正空白。九个错误标记的 EqBench 对的发现具有直接的社区价值。紧密度比较器 (JUDGE) 解决了评估基础设施的缺口。作者诚实地指出了局限性（小规模基准、单向比较、工程范围边界），而非过度声称。

打分

加权总分: 6.6/10（加权分之和 66.0 / 权重之和 9.5） 最终建议: Weak Accept 6.5-8