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

论文链接：SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? 发表时间：2026 年 9 月（arXiv v1, 2609.21190） 机构：UC Berkeley + Georgia Tech + UIUC + AWS AI Labs（🌟企业 + 高校，AWS AI Labs 主导，共 11 位作者） 领域标签：cs.LG / Software Engineering / Formal Verification

一、论文背景：SWE 评测的「判定危机」

过去两年，衡量 LLM 编程 Agent 能力的主流范式是执行隐藏测试套件：给 Agent 一个编程任务，用一套开发者预先写好、Agent 看不到的测试用例（held-out tests）来判定对错。这套方法便宜、易实现、能复用代码库里已有的测试，因此成了 SWE-Bench 系基准的事实标准，也驱动了 SWE 求解能力的快速进步。

但论文开门见山地指出：测试是一个很弱的正确性判据，而且「通过测试 ≠ 修对了」。根本上有两道裂缝：

1. 测试天然不完整（incompleteness）。有限的输入集合无法认证它在「没被测试覆盖的输入」上的行为。对 SWE-Bench 的审计发现，许多被判定为正确的 patch，其实只是因为配套测试太弱，分不出「真修复」和「表面修复」（Aleithan et al., 2024）。
2. 可被奖励黑客（reward hacking）钻空子。Agent 可以利用这种不完整性，生成「在给定测试上通过、但泛化能力差」的代码。Zhong et al. (2025) 在 ImpossibleBench 中发现，相当大比例的 SWE-Bench patch 属于「测试通过但实质上不正确」。

更尖锐的是记忆/污染（contamination）问题。Liang et al. (2025) 在 The SWE-Bench Illusion 中给出诊断证据：最强模型仅凭 issue 描述就能以高达 76% 的准确率定位到出错的源文件路径（无需看仓库结构），而在非 SWE-Bench 仓库上仅 53%；函数复现的逐字相似度在 SWE-Bench Verified 上明显高于其他基准。这说明相当一部分「解决率」可能来自对训练数据的记忆，而非真正的推理能力。

形式化验证（formal verification）恰好同时治这两类病：它不是在「采样输入」上检查，而是在「整个被声明的输入域」上证明程序满足规范，因此既不受测试集合有限性的限制，也难以被「恰好骗过几个用例」的 patch 蒙混。但现有形式化代码生成工作大多假设规范已经以形式语言给出，且只覆盖独立的小任务、HumanEval 式题目或竞赛数学——从未把一个「用含糊自然语言描述意图、要嵌入大型多文件代码库」的真实 issue 作为验证对象。

这就是 SWE-Proof 的出发点：把真实软件工程任务与形式化验证「第一次」接起来。

二、论文定位与关联工作

SWE-Proof 处在两条研究谱系的交汇处。

谱系 A：SWE 基准家族。 从 SWE-Bench（Jimenez et al., 2024）到人工校验过的 500 例子集 SWE-Bench Verified（OpenAI, 2024），再到任务规模更大的 SWE-Bench Pro、多模态的 SWE-Bench Multimodal、多语言的 Multi-SWE-bench、用于 Agent 训练/验证器训练的 SWE-Gym，以及去污染的任务流（SWE-rebench 等）。一条平行支线专门质疑判定 oracle 本身：Aleithan 等人指出测试泄漏与测试过弱，Liang 等人把部分性能归因于记忆。社区的对策多是「加强或刷新测试」。SWE-Proof 则干脆用形式化规范替换测试，让验证过的修复在其整个输入域上「可证正确」。

谱系 B：形式化/验证感知的代码生成。 CLOVER（Sun et al., 2024）仅在验证器确认代码、文档、Dafny 规范三者互一致时才接受生成；VERINA（Ye et al., 2025）在 Lean 中联合评测代码/规范/证明，并把 soundness 与 completeness 分开度量（与本文做法同源）；DafnyBench、vericoding 多语言套件衡量模型能否产出可验证产物；VOs 等则推进证明自动化。最接近本文设定的是 VERO（Ye et al., 2026）：它在 LEAN 4 上做仓库级实现+证明合成（43 例），但其规范由人冻结提供、且是上游代码的手动 Lean 改写而非真实仓库，Agent 只是填固定脚手架——规范合成被排除在外。

定位结论：SWE-Proof 不是「又一个形式化验证基准」，而是把「SWE 真实任务」与「形式化验证」两条线首次缝合，并把它做成可审计、可复现、可扩展到新基准的构造流水线。

三、问题定义：判定信号的完备性

抛开工程细节，论文面对的深层结构是一个**「判定信号的完备性」问题**：

• 具体问题：怎么知道一个 patch 真的修复了 issue？
• 抽象问题：给定一个 issue、一个仓库、一个已知正确的 gold patch，我们能否构造一种对所有输入都成立的「正确判据」，使得「满足该判据」严格蕴含「通过隐藏测试（即解决 issue）」？

形式化地，论文给出核心断言 Claim 1（Verify ⇒ Resolve）：

设某实例有规范 S 与公理集 A，I 是用验证后端语言（NAGINI / VELVET / LEAN）写出的实现，P 是仓库中等价于 I 的 Python patch。若 I 在 A 下对 S 验证通过，则 P 能通过 SWE-Bench 的隐藏测试、解决该实例。

这个抽象之所以精妙，在于它把「评测可靠性」从「有限采样」上升为「全域约束」：验证买到的不只是测试能给的——一个被验证的 I 在 S 允许的每个输入上（包括没有任何测试覆盖到的输入）都正确。等价性 I≈P 是 Claim 的前提而非结论；评测时 Agent 自行给出等价 patch，本文用独立的等价性门去审计它。

四、问题解法：BENCHPROOFER 三步 + 13 道门

4.1 两个核心思想

思想一：规范合成（specification synthesis）。 真实任务用含糊、可有多种形式读法的自然语言陈述意图。BENCHPROOFER 让一个 Agent 把描述转成形式化规范并在反馈循环里精炼。注意：构造期可见 gold patch、buggy 代码、测试 patch 与 F2P/PASS-TO-PASS 列表，Agent 据此校准规范的强弱（例如问「一个实现能否满足规范却仍在某个 F2P 测试上失败」）；但评测期这些一概不可见。

思想二：环境公理化（environment axiomatization）——「接口契约摘要」。

类比：你要在别人写的巨型代码库里改一个函数。验证器没法把这个函数调用的每一个下游函数（及其传递闭包）都验证一遍——那会爆炸。于是论文给每个「新代码调用但没修改」的函数写一条公理（axiom）：只声明「这个修复所依赖的被调函数的性质」。这就像给每个外部接口写一张**「契约摘要卡」——你不必证明隔壁部门的内部实现，只需约定「调用它时，它保证返回什么」，把「我们验证的部分」和「我们假设的部分」划清边界。公理可以是过近似**（约束得比被调函数实际保证的更弱）仍无妨，只要证明能闭环。

公理本身是「机器生成 + 可执行校验」的产物：先收集未修改的被调函数 f1, f2…，为每个 fi 造一个 fuzzer（随机输入 + Agent 写的边界用例），Agent 起草候选公理 Ai，然后两个对立循环精炼它——正确性循环用 fuzzer 跑 fi，任何违反 Ai 的输入都把它打回重写；有用性循环让验证器尝试用 Ai 作为引理闭合「参考实现→规范」的证明，失败同样打回。直到公理既与观测行为一致、又强到能收尾证明。

4.2 13 道正确性门（机械门 + 对抗门）

没有任何单点检查能端到端保证 Claim 1，于是 BENCHPROOFER 用一整套门，候选实例必须全部通过才被接收，任何反例都打回修订。

机械门（跑 SMT 求解器 / LEAN 编译器）：

1. 验证（Verification）：参考实现在后端下验证通过。
2. 判别力（Discrimination）：同一规范配上 pre-fix（未修复）实现，必须验证失败——证明规范强到能抓住缺陷。
3. 变异杀灭（Mutation）：对参考实现做一阶变异（逐算子），要求变异体不再验证；存活的变异体意味着规范漏掉了局部扰动，要求高杀灭率（本文报告 99.17%）。
4. 卫生（Hygiene）：只使用验证器可健全检查的特性（import 白名单、规范良构、证明无 sorry 之类逃逸口）。
5. 解决率（Resolution）：在官方 Docker harness 里应用 gold patch，确认实例确实 resolve——它测的是原始基准，是流水线可以安全指向新基准的原因。

对抗门（LLM 审计员试图用具体反例驳倒实例）： 6. 公理健全性（Axiom soundness）：独立对抗审计员重跑 fuzzing，并在实例 Docker 里执行真实被调函数裁决；一次观测违反即拒。 7. 一致性（Conformance）：把参考实现的可执行影子在真实已修复函数上跑 ≥10⁵ 个生成输入，报告任何不一致。 8. 健全性攻击（Soundness）：审计员猎寻「规范与仓库代码不一致的输入」——规范漂得太强会让正确代码也无法验证。 9. 完备性攻击（Completeness）：审计员构造「满足后置条件但没干真活」的错误实现，看它能否蒙混验证通过。 10. 基于性质的伪造（Property-based falsification）：把上述两攻击做成可复跑的性质测试套件（标记好应接收/应拒绝的用例），随基准发布为可复用证据。 11. 等价性（Equivalence）：审计参考实现与 gold patch 的逐步映射，确认每步都是「类型精化 / 公理化被调函数 / 恒等操作」三者之一。 12. 泄漏-机械筛查（Leakage, mechanical）：规范视图（规范+公理，评测时给 Agent 看的那份）若暴露 patched 标识符、路径或修复叙述则拒。 13. 泄漏-对抗审计（Leakage, adversarial）：对抗审计员仅凭视图尝试重建 gold patch，成功即拒——否则等于把答案递给被测 Agent。

4.3 三种后端 + EARS 对照

SWE-PROOF 在每个实例上用四种「规范语言」各构造一遍：

• NAGINI：契约注解的 Python，翻译到中间验证语言再交给 SMT 求解；
• VELVET：嵌入 Lean 4 的命令式验证 DSL；
• 纯 LEAN：证明由 Agent 写、编译器查，而非 SMT 求解；
• EARS：结构化自然语言规范（非形式，作为对照组）。

前三者在「机器可检查」的意义上等价，EARS 则用来分离两个容易混淆的效果：给出精确意图陈述的收益，与该陈述可被机械强制的收益。

五、评估指标与实验证据

评测在全部 500 个 SWE-Bench Verified 实例上，对 Claude Opus 4.8 与 GPT-5.5 两套前沿模型、在 NAGINI/VELVET/LEAN 三后端下跑完整网格。核心是一张「设定 × 指标」表（表 2），其中几个关键行：

这组实验设计为什么能干净地支撑论点？

• 行 0 → 行 1 证明「测试不完整」：行 1 让对抗审计员为行 0 通过的每个 patch 专门写新测试，区分它与 gold patch；26.8% 的 patch 被找到反例，说明「通过全部隐藏测试」远不等于正确。
• 行 6 → 行 7 证明「形式规范才补得上这个洞」：同一份 ground-truth 规范，形式后端验证「证明不存在违反输入」，只损失 0.9/0.3pp；而 EARS 非形式规范下损失 17.8/46.0pp——结构化自然语言规范并不能关闭缺口。
• 行 7 vs 行 3 干净地定位 faithfulness 瓶颈：两者唯一差别是「给不给正确规范」。给定正确规范带来 +11.0（Opus）/ +14.2（GPT）pp 的收益，差距如此之大，只能归因于「自写规范」这道环节——而不是写实现或写证明。

进一步，论文用 5 属性规范审计（admissible / sound / complete / sound-axioms / faithful）拆解「自写规范为何失败」：在 NAGINI 下 Opus 仅 46.0%、GPT 64.2% 通过全审计，VELVET 下 60.0%/72.0%，LEAN 下 61.4%/69.2%。失败高度倾斜——sound axioms、admissibility、completeness 几乎不失败（各 ≤3.9%），faithfulness 占主导：Opus 42.5%、GPT 30.0%，且是每一格中最常被违反的属性。即：模型写出的规范在「它建模的那些函数上」是对的，但覆盖的函数太少，漏掉的行为面依然不受约束。

最关键的证据闭环在 Finding 5：在端到端设定下，把模型自写规范按「patch 是否 resolve」分组重新审计（审计员看不到 patch 或测试结果）。未解决实例的规范 89.4% 被审计判失败，已解决实例仅 47.3%；差距在「约束多少行为」的 faithfulness（平均 44.3pp）与 soundness（26.7pp）上最宽。规范正确性会「追踪」解决正确性——而 faithfulness 解释了其中大部分缺口。

六、效果优势的根源解释

6.1 因果链（论文实验已支持）

方法差异 → 机制变化 → 指标提升，每一步可推理：

1. 隐藏测试只采样有限输入（论文已支持：行 0→行 1 推翻 26.8%）。
2. 这留下一个过拟合/奖励黑客空间：patch 可在未覆盖输入上行为错误却仍通过测试（论文已支持：Zhong 等人的 reward-hack 观测）。
3. 形式化规范在整个被声明的输入域上约束行为（论文已支持：验证门 + 判别力门 + 变异杀灭 99.17% 共同确保规范强到抓住缺陷）。
4. 因此「验证通过」比「测试通过」更逼近「真实修复」，审计稳定性高：给定正确规范后行 7 相比行 6 仅 -0.9pp（论文已支持）。
5. 自写规范卡在 faithfulness：它只约束部分行为面，漏掉的部分仍可过拟合，所以自写规范对解决率零收益（论文已支持：行 3≈行 0；faithfulness 失败占主导）。

一句话：不是「用了验证所以好」，而是「验证把判定从有限采样升级为全域约束，堵死了过拟合空间」——但前提是规范本身 faithfully 覆盖了全部所需行为面。

6.2 相关工作检索与对照

6.3 综合判断与未决问题

• 多项研究共同支持：隐藏测试是不完整且易被利用的弱判据（Liang/Zhong/Aleithan 各自独立指向）；「全域约束」天然优于「有限采样」（验证的门设计有变异测试经典背书）。这部分是强证据。
• 仍属合理推测的机制：faithfulness 之所以成为主导失败，论文给出因果（覆盖行为面不足→漏掉部分仍可过拟合），但从模型能力角度「为何难以覆盖全行为面」尚无更深的机制解释；RMU 类比仅用于直观说明「表层达标 ≠ 底层到位」，不构成因果证明。
• 优势的适用条件与可能失效：当仓库改动落在「前后置条件可观测的值域」内时（SWE-Bench Verified 500 例全部满足，SWE-Bench Pro 242/266 满足），验证收益成立；若改动仅是重命名/ relocation、或涉及导入时序副作用等部分正确性逻辑无法表达的行为，则无法构造可验证孪生（Pro 中 22/266 即因此失败）。此外公理健全性、参考实现到 patch 的精化保真度，属于「经执行/fuzzing/对抗审计确立的信任点」而非证明，与任何验证系统一样依赖其显式假设。

七、必要知识反推

假设一个完全空白的人来做这件事，他最少必须掌握三类知识：

领域知识层：

• 软件验证的基本概念——前置/后置条件、不变量、SMT 求解、证明助手（Lean）的「内核只信被证明的项」。不理解就无法看懂「验证通过」意味着什么。
• SWE-Bench 的运作：issue、gold patch、F2P/PASS-TO-PASS、Docker harness、隐藏测试判定。这是本文要「替换」的旧 oracle。
• Python 生态与大型代码库的依赖/调用结构，才能理解「为什么不能验证每个被调函数」（爆炸）以及为何需要公理。

方法论知识层：

• 规范质量的多维标准（本文借 Feng et al. 的 admissible/sound/complete，并新提出 sound-axioms 与 faithful）。
• 对抗审计与变异测试的思想谱系，才能设计 13 道门而非单点检查。
• 自动形式化（autoformalization）中「faithfulness」的经典难题（动态推断的不变量不健全、循环不变式常非归纳、规范可被空洞满足等），这是本文把 faithfulness 单列为核心的认知来源。

工程知识层：

• 四种后端（NAGINI/VELVET/LEAN/EARS）各自的表达力与成本权衡，决定建模选择。
• 把「参考实现」与「仓库 Python patch」做行为保持映射的可执行影子技术、fuzzer 构造、泄漏防护。

知识融合的关键节点：真正创造性的洞察在于——把「SWE 真实 issue + 已知 gold patch」作为构造期可见信息，用规范合成 + 环境公理化把「不可验证的真实任务」转成「可验证的孪生实例」，再用机械门 + 对抗门把「机器检查」与「LLM 对抗」缝成可信保证。这一步需要同时理解「验证理论的保证边界」与「LLM 会 reward-hack 测试」两件事，并在交汇处设计流水线。

八、可提取的通用性灵感

1. 验证不对称性（Verification Asymmetry）。

   • 核心：对「正确性」的判定，从「抽样检查」升级为「全域约束」，收益是结构性的，不止于本任务。
   • 证据：行 6→行 7 形式后端仅 -0.9pp，EARS 非形式则损失 17.8/46.0pp。
   • 推广：RLHF 的奖励模型过拟合、评测集污染、Agent 的「通过单测但生产翻车」、模型安全红队的「通过测评但真实危险」——凡是「用有限样本判定能力」的场景都值得换成更强的不变式约束。

2. 对抗审计作为信任机制（Adversarial Audit as Trust）。

   • 核心：单点自动检查不足以确立端到端保证，用「对立角色互相找反例」比「自己检查自己」可靠。
   • 证据：13 道门中对抗门（健全性/完备性/等价/泄漏）捕获了机械门抓不到的语义漂移。
   • 推广：数据集质量审计、合成数据合法性校验、Agent 输出的事实性核查、模型对齐的「红队即验证器」范式。

3. Faithfulness 作为新质量维度。

   • 核心：一个规范/说明「覆盖了所需行为的多少面」本身就是独立质量指标，且比「单点正确」更决定成败。
   • 证据：faithfulness 失败占主导（42.5%/30.0%），且解释未解决/已解决规范审计差距的大部分（44.3pp）。
   • 推广：需求工程中的「需求覆盖度」、RAG 中检索对问题的覆盖、prompt 对任务的覆盖、评测 rubric 对能力的覆盖——凡是「用一份声明去约束复杂对象」的场合，faithfulness 都应是显式度量。

4. 「给定正确规范」与「自写规范」的鸿沟即能力边界。

   • 核心：当外部提供正确抽象时模型表现惊艳（96.2%/94.4%），一旦要自己从含糊意图合成抽象就跌回基线——说明当前模型的瓶颈在「意图→精确规约」而非「规约→实现」。
   • 推广：agentic 系统中「规划/规格化」是比「执行」更稀缺的能力；产品上宁可让人提供清晰 spec、把模型放在实现层，也不要指望它无中生有地定义正确目标。这与 CodeSpecBench（Chen et al., 2026）发现「最强前沿 LLM 在仓库级规范生成上通过率仅 20.2%」相互印证。

一句话收束：SWE-Proof 用机器检查的形式化证明，把「通过测试」这一弱信号换成了「全域正确的证明」；但它也冷峻地揭示——当模型必须自己从含糊意图写出那份证明所依赖的规范时，瓶颈不在证明、不在实现，而在 faithful 地理解「到底要正确到什么程度」。这或许是对当下所有「Agent 自动解决复杂任务」叙事最诚实的一句注脚。