025 · 返回值被唯一确定，就算规格完整了吗？

核心问题：SpecAgent 的完备性探针若能证明同一输入下两次调用的返回值相等，这说明后置条件排除了返回值的歧义，还是已经足以说明形式规格完整地表达了程序语义？

论文卡片

• 原题： SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
• 作者： Lezhi Ma、Han Wang、Shangqing Liu、Jiawan Wang、Lei Bu。
• 机构： 南京大学。
• 版本： 2026-10-04，arXiv v1；cs.SE。
• 定位： 面向 C 程序的 Agent 化 ACSL 规格合成，使用 Frama-C/WP 检查正确性，并尝试在证明成功之后继续判断规格强度。
• 阅读入口： alphaXiv · arXiv · HTML 全文 · PDF

论文讲了什么

演绎验证依赖函数契约、循环不变量等辅助规格，把复杂程序拆成可组合的局部证明。已有 LLM 方法通常按依赖顺序向前生成：一份规格通过当前检查后就被固定；下游证明失败时，也只在失败位置附近修改。论文指出，下游失败的根因可能是上游规格虽然可证明、却不够强，局部修补因此会反复处理症状而不是根因。

SpecAgent 把规格合成组织为四个阶段：

1. Planning： 从函数调用、循环位置等结构信息中确定需要哪些规格、语义目标和依赖顺序。
2. Generation： 生成 requires、ensures、assigns 与循环不变量；最多检索三个结构相似的 ACSL 官方教程示例作为上下文。
3. Verification and Repairing： 用 Frama-C/WP 检查候选，Repairing Agent 可读取失败位置、调用关系与值分析结果，也可以回到依赖链上游修改已经生成的规格。
4. Critique and Refinement： 规格通过验证后，Critique Agent 继续寻找过弱后置条件、过强前置条件和空洞契约，并在 ACCEPT、局部 IMPROVE 与重新规划 REPLAN 之间选择。

整体流程由确定性状态机控制；各 Agent 不能改变流程，只通过共享工作区交换规格、验证结果和诊断文档。每次 Planning/Critique 最多 10 个 ReAct 步骤，Generation/Repairing 最多 30 步；整条轨迹最多调用 Agent 10 次。

完备性探针究竟检查什么

作者把一组正确后置条件视为真实程序行为的过近似：它必须允许程序实际产生的行为，也可能额外允许程序不可能产生的行为。规格越强，额外允许的行为越少。

对确定性函数，论文构造一个临时验证 harness：以相同参数调用函数两次，只根据函数契约证明两次返回值相等。如果证明失败，说明后置条件仍允许同一输入对应多个返回值，是“返回值描述不足”的具体证据；失败义务和反例再交给 Critique Agent 修改规格。

这个探针比单纯询问 LLM“规格够不够强”更稳定，但它检查的是一个必要维度，而不是完整语义。返回值唯一仍可能唯一地约束到错误函数；它也没有直接覆盖内存副作用、全局状态变化、时序关系、异常行为或规格是否表达了真正关心的性质。过强甚至不可满足的前置条件也可能让证明变得容易，论文主要依靠 Critique Agent 识别这种问题。

主要结果

规格质量实验包含来自 14 个开源仓库的 50 个 C 程序，平均 456.44 行，其中 7 个超过 1,000 行；每个程序带有可验证的人工 ground-truth 规格。论文的 precision 表示“生成规格中被证明正确的比例”，recall 表示“ground truth 中有多少被至少一条同等强度的生成规格覆盖”。等价性和强度关系通过 Frama-C/WP 验证双向蕴含来判断。

这些数字是 14 个仓库结果的宏平均，而不是把所有规格合并后的微平均。它们表明 SpecAgent 在这套 ground truth 上同时保持较高正确率与覆盖率；并不直接等价于对任意程序语义的 88.95% 完整表达。

消融中，DeepSeek-V4 的 Generation-only 为 89.78% precision、80.93% recall；加入规划和修复后为 94.79%/82.08%；再加入 Critique 与 refinement 的完整系统达到 96.82%/88.95%。作者据此认为修复主要提高正确性，强度审查进一步提高覆盖率。不过各组件会改变后续轨迹和 Agent 调用次数，论文明确承认该消融不能把每个组件解释为严格独立的因果效应。

第二组实验考察生成规格能否帮助证明 811 个目标：其中 542 个来自 X509-parser、Contiki 和 Atomthreads 的运行时安全目标，另有 269 个来自平均仅 27.79 行的 SV-COMP 小程序。SpecAgent 证明了 604 个，Codex 为 523 个，Preguss 为 512 个。SpecAgent 并非每个子集都领先：在 Atomthreads 上证明 109 个，略少于 Preguss 的 112 个。

证据边界

实验最有力的结论是：在同一 Frama-C/WP 环境和既定 ground truth 下，依赖感知的回溯修复与证明后审查能提高规格覆盖，并让更多既定目标可被证明。它没有证明 Critique Agent 已经解决了“规格是否表达设计意图”这一开放问题。

首先，recall 的上限由人工 ground truth 定义。若 ground truth 遗漏某种重要语义，生成结果不会因此受罚；若两份不同抽象都足以支持目标证明，双向蕴含又可能把合理但不等价的规格判成未覆盖。Frama-C/WP 和底层求解器也不完备，证明失败可能只是工具未能完成证明，作者把这列为潜在假阴性。

其次，完备性探针只对确定性返回值给出单一证据。论文没有单独报告探针或 Critique Agent 判断“过弱、过强、空洞”的 precision/recall，因此完整系统指标无法说明它们分别漏掉或误报了多少强度问题。

最后，方法只在 C、ACSL 与 Frama-C 生态中评测；50 个质量评测程序仍是有限样本。所谓 811 个“真实验证目标”也混合了三个开源项目与 269 个 SV-COMP 小程序，不能把总数当成 811 个同等复杂度的真实项目任务。

重点读哪里

先读 §2.2 与图 1，理解为什么下游失败可能由上游弱规格造成；再读 §3.3–3.5，重点看验证门、跨依赖修复、完备性探针和确定性 orchestrator。随后细读 §4.3–4.4 与表 2–4，核对 benchmark 构成、precision/recall 定义、baseline 与验证目标；最后读 §6.2，看作者如何限定随机性、消融解释、语言范围与求解器不完备性。

思想启发

以下是由论文引出的理解角度，不是作者额外验证过的结论。

SpecAgent 把“形式证明通过”分成了两道门：第一道问规格是否与实现一致，第二道问规格是否足以排除无关行为。这一区分很重要，因为弱规格可以正确且易证，却无法给调用者提供足够信息。论文真正推进的不是把 LLM 输出接到 verifier，而是让后续失败和强度信号能够推翻先前已经“通过”的规格。

但第二道门仍然需要自己的规格。返回值确定性、人工 ground truth 和目标证明数，分别定义了三种“足够强”：唯一约束输出、接近参考规格、足以完成当前证明。它们彼此相关，却没有任何一种能单独替代“完整表达预期语义”。

三个思考问题

1. 返回值确定性是规格完整性的必要条件，还是只是一种局部充分信号？

如果契约能唯一确定返回值，却没有完整描述内存写入、全局状态或允许输入，它应当被称为“完整”吗？

2. 以 ground truth 覆盖率衡量规格强度，会偏好哪一种“正确答案”？

当两份规格采用不同抽象、但都足以证明同一个高层性质时，要求与人工规格达到同等强度是否会低估其中一份？

3. 下游证明失败，何时足以推翻已经验证通过的上游规格？

Agent 沿依赖链回溯能修复弱上游契约，也可能把求解器能力不足或下游规格错误误判为上游问题；什么证据才足够支持重新规划？