SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?

本文由 paper-daily 使用 DeepSeek 自动生成，仅供快速了解论文；关键结论请以原文为准。

论文原文 · PDF · 源文件

【一句话总结】论文提出 Benchproofer 流水线，将真实仓库级编码任务转化为形式化验证基准 SWE-Proof，揭示测试通过不等于正确，并指出忠实规范合成是核心开放问题。

基本信息

属性	内容
作者	George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, Jun Huan, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou, Anoop Deoras
来源	arXiv:2609.21190
发布日期	2026-09-18
抓取领域	自然语言处理
学科方向	机器学习 · 人工智能 · 软件工程
arXiv 分类	cs.LG, cs.AI, cs.SE
适用层次	进阶
标签	【标签】形式化验证, 代码生成评测, 规范合成, 大语言模型, SWE-bench
PDF	在线阅读
代码仓库	暂无

---

问题的初衷（Why - 为什么要做这个研究）

【问题的初衷】大语言模型（Large Language Model, LLM）生成的代码正确性验证，是现代软件工程面临的核心挑战。当前主流的智能体代码生成基准（如 SWE-bench）依赖留出的测试套件（held-out test suites）来判定正确性，但这种方法存在两个根本性缺陷：其一，测试套件本质上是不完备的，只能覆盖开发者预先设想的有限场景，无法穷尽所有可能的输入与边界条件，因此通过测试的补丁（patch）仍可能隐藏错误；其二，随着模型在海量公开代码上训练，测试用例本身可能被记忆（memorization），导致评测结果虚高，无法真实反映模型的泛化能力。形式化验证（Formal Verification）能够从根本上规避这两个问题——它通过机器可检查的证明（machine-checked proof）来保证代码满足规范，而非依赖有限采样。然而，现有的形式化验证工作仅覆盖独立任务（standalone tasks），其规范（specification）作为输入直接给出，而真实世界的软件问题涉及大型代码仓库、依赖复杂的既有函数，且意图以模糊的自然语言表述。因此，如何将真实仓库级别的编码任务转化为可形式化验证的任务，成为一个亟待解决的关键问题。

---

问题的解决（What - 提出了什么方案）

【问题的解决】论文提出了 Benchproofer，一条将带有已知正确补丁的编码任务转化为形式化验证任务的流水线（pipeline）。其核心思路是：给定一个真实 issue 及其正确补丁，Benchproofer 自动为新代码编写形式化规范（specification），并用公理（axioms）总结该代码所调用的既有函数的行为，从而在无需完整验证整个仓库的前提下，对补丁的正确性进行形式化证明。为避免规范本身出错，Benchproofer 引入了机械门（mechanical gate）与对抗门（adversarial gate）双重准入机制：只有当两个门都认可该实例时，才将其纳入基准。将这一流水线应用于 SWE-bench Verified，论文构建了 SWE-Proof——包含 500 个真实 issue 的基准，其正确性由形式化验证而非测试保证，并可扩展至 SWE-bench Pro。与现有方法的本质区别在于：现有基准用测试判定对错，SWE-Proof 用机器可检查的证明判定对错；现有形式化工作假设规范已知，而本文直面'规范从何而来'这一核心难题，并揭示出忠实规范合成（faithful specification synthesis）才是真正的瓶颈。

---

技术方法详解（How - 怎么实现的）

【技术方法详解】

• 任务转化流水线：Benchproofer 接收一个编码任务及其已知正确补丁，自动生成形式化规范。规范描述新代码必须满足的行为，而非描述实现细节。
• 公理摘要机制：对于补丁所调用的既有函数，Benchproofer 不展开其实现，而是为其行为编写公理（axioms），将仓库级别的验证问题降维为局部验证问题，从而避免验证整个大型仓库。
• 双重准入门控：机械门（mechanical gate）检查规范是否可被形式化工具接受、是否与补丁一致；对抗门（adversarial gate）主动尝试构造反例（counterexample），若找到反例则拒绝该实例，确保规范足够强。
• 反例检测能力：论文发现，在通过测试的补丁中，有 25% 到 50% 存在反例，说明测试通过并不等于正确。结构化自然语言规范无法修复这一问题，而正确的形式化规范可将 Opus 4.8 的解决率从 85% 提升至 95%。
• 规范合成瓶颈分析：论文让模型自行编写规范，发现其表现与无辅助基线相比没有提升，且仅有 62% 的规范能通过审计。失败的主要模式是忠实性（faithfulness）不足——规范只约束了部分必需行为，而将剩余行为留空。
• 规范质量与结果的相关性：规范质量与最终结果高度相关，在未解决的实例中失败率高达 89%，而在已解决的实例中失败率为 47%，表明忠实规范合成是一个具体的开放问题。

系统架构图

方法流程图

核心公式与算法

【核心公式】

$$\text{Resolve}(M)=\frac{|\{i\in \text{SWE-Proof}:\text{Verify}({\text{Patch}}_M(i),\text{Spec}(i))=\mathrm{\top }\}|}{|\text{SWE-Proof}|}$$

该公式定义模型 $M$ 在 SWE-Proof 上的解决率，其中 ${\text{Patch}}_M(i)$ 是模型对实例 $i$ 生成的补丁，$\text{Spec}(i)$ 是该实例的形式化规范，$\text{Verify}$ 返回证明是否成功。

$$\text{Faithful}(\text{Spec},\text{Intent})=\mathrm{\forall }x.\text{Spec}(x)\Rightarrow \text{Intent}(x)\wedge \mathrm{\forall }x.\text{Intent}(x)\Rightarrow \text{Spec}(x)$$

该公式刻画规范的忠实性：规范必须与真实意图双向蕴含，既不能过弱（遗漏必需行为），也不能过强（禁止合法行为）。

$$\text{Admit}(i)=\text{MechGate}(i)\wedge \mathrm{\neg }\mathrm{\exists }c.\text{Counterexample}(c,\text{Spec}(i),\text{Patch}(i))$$

该公式定义实例准入条件：机械门通过，且对抗门未能找到反例。

---

应用场景（Where - 在哪落地）

【应用场景】

• 场景一：安全关键软件的高可信评测。在自动驾驶、航空航天、医疗设备等领域，代码错误可能导致严重后果。使用 SWE-Proof 这类基于形式化证明的基准，可以在模型部署前评估其生成代码是否真正满足安全规范，而非仅仅通过有限测试。预期效果是显著降低因测试遗漏而引入的潜在缺陷，提升系统整体安全性。
• 场景二：大型开源仓库的持续集成与代码审查。在 GitHub 等平台上，维护者面对大量由 AI 生成的补丁，传统 CI 测试难以覆盖所有边界。将 Benchproofer 流水线集成到 CI 中，可自动为补丁生成规范并尝试形式化验证，对无法证明的补丁给出反例或警告。预期效果是提高代码审查效率，减少回归缺陷。
• 场景三：编程教育与竞赛评测。在编程教学或算法竞赛中，学生提交的代码通常用测试用例判定。使用形式化规范可以更公平、更严格地评估代码正确性，避免因测试用例泄露或覆盖不足导致的误判。预期效果是提升评测的信度与效度，帮助学生理解规范与实现的关系。

---

具体技术细节示例（How in Action - 算法如何执行）

【具体技术细节示例】假设有一个真实 issue：某 Python 仓库中的函数 merge_intervals(intervals) 需要合并重叠区间。已知正确补丁修改了该函数。Benchproofer 的执行过程如下：

第一步，解析补丁，识别新代码为 merge_intervals 的函数体，并发现它调用了既有函数 sort_by_start(intervals)。

第二步，为 sort_by_start 编写公理：$\mathrm{\forall }L.\text{sorted}(\text{sort\_by\_start}(L))\wedge \text{permutation}(L,\text{sort\_by\_start}(L))$，即输出是按起始位置排序的排列。

第三步，为新代码编写形式化规范：$\mathrm{\forall }L.\text{merge\_intervals}(L)=R\Rightarrow \text{non\_overlapping}(R)\wedge \text{union}(R)=\text{union}(L)\wedge \text{sorted}(R)$。

第四步，机械门检查规范是否可被验证器接受，并确认补丁满足规范。假设通过。

第五步，对抗门尝试构造反例。例如，输入 $L=[(1,3),(2,6),(8,10),(9,12)]$。正确输出应为 $[(1,6),(8,12)]$。对抗门尝试寻找一个满足规范但补丁输出错误的输入，若找不到，则实例准入。

第六步，形式化验证补丁。若证明成功，则该实例被标记为已解决。若模型生成的补丁在输入 $L=[(1,3),(2,6),(8,10),(9,12)]$ 上输出 $[(1,6),(8,10),(9,12)]$，虽然可能通过某些测试，但形式化验证会发现其违反 non_overlapping 性质，从而给出反例。

---

实验结果（Results - 效果如何）

【实验结果】论文将 Benchproofer 应用于 SWE-bench Verified，构建了包含 500 个真实 issue 的 SWE-Proof 基准，并扩展至 SWE-bench Pro。实验在两个前沿模型上进行。关键发现包括：在通过测试的补丁中，有 25% 到 50% 存在反例，即测试通过但形式化验证失败，说明测试套件遗漏了大量错误。结构化自然语言规范无法修复这一问题，而正确的形式化规范将 Opus 4.8 的解决率从 85% 提升至 95%。在规范合成方面，让模型自行编写规范的表现与无辅助基线相比没有提升，且仅有 62% 的规范能通过审计。规范质量与最终结果高度相关：在未解决的实例中，规范失败率高达 89%，而在已解决的实例中失败率为 47%。这些结果共同表明，忠实规范合成是当前的核心瓶颈。

实验结果可视化

---

优势与不足

【优势与不足】

• 优势：
  1. 首次将形式化验证引入真实仓库级别的编码任务基准，从根本上规避了测试套件不完备与记忆化两大问题。
  2. 提出 Benchproofer 流水线，通过公理摘要与双重门控，使仓库级验证在工程上可行。
  3. 实验揭示出测试通过不等于正确这一重要事实，量化了 25% 到 50% 的测试通过补丁存在反例，对社区具有警示意义。
  4. 明确指出忠实规范合成是开放问题，为后续研究提供了清晰的方向。
• 不足：
  1. 规范合成仍依赖人工或模型辅助，模型自行编写规范的效果不佳，仅 62% 通过审计，限制了流水线的自动化程度。
  2. 公理摘要可能引入不忠实或不完备的假设，若公理本身错误，则验证结论不可靠。
  3. 基准规模为 500 个 issue，相对 SWE-bench 全量仍较小，覆盖面可能有限。
  4. 形式化验证工具链的可用性与语言覆盖范围可能限制其推广到更多编程语言。

---

相关工作

【相关工作】

• SWE-bench 与 SWE-bench Verified：本文的直接基础，使用留出测试套件判定补丁正确性，本文指出其不完备性与记忆化风险。
• 形式化验证与程序证明：如 Coq、Lean、Dafny 等工具，本文将其从独立任务扩展到真实仓库级任务。
• 规范合成（Specification Synthesis）：从代码或自然语言生成形式化规范，本文揭示其忠实性是核心瓶颈。
• 大语言模型代码生成评测：关注 LLM 生成代码的正确性评估，本文提供了基于证明的新评测范式。
• 反例生成与模糊测试（Fuzzing）：本文的对抗门借鉴了主动寻找反例的思想，用于验证规范强度。

---

未来研究方向

【未来方向】

• 忠实规范合成的自动化：研究如何让模型生成既不过弱也不过强的规范，可能结合交互式定理证明与人类反馈。
• 公理摘要的可靠性验证：探索如何自动验证公理摘要的忠实性，避免因公理错误导致验证结论不可靠。
• 扩展到更多编程语言与仓库：将 Benchproofer 推广到 Java、C++、Rust 等语言，并处理更复杂的依赖关系。
• 与测试结合的混合验证：研究形式化验证与测试的互补使用，在验证成本过高时回退到测试，并量化两者的覆盖差异。

---

一句话总结

【一句话总结】论文提出 Benchproofer 流水线，将真实仓库级编码任务转化为形式化验证基准 SWE-Proof，揭示测试通过不等于正确，并指出忠实规范合成是核心开放问题。

---

本解读由 DeepSeek AI 自动生成，仅供参考。