SWE-Proof：通过证明检查，为什么仍可能修错代码

图 2 的 Benchproofer 门控，能把哪些结论交给机器，哪些仍依赖审计？

1. 1

   用正确补丁构造评测，但不能把它当作求解输入

   构造阶段读取 issue、参考补丁和测试，写出新行为的规格，并用公理概括未改变的被调函数。求解阶段再按不同设置给出 issue、定位或规格；这些设置提供的信息不同，必须分开比较。

2. 2

   通过三种形式后端建立可检查对象

   Nagini 在 Python 合约上检查；Velvet 使用命令式 Lean 表示；纯 Lean 用内核检查证明。EARS 结构化英语是非形式对照。对后两种后端，把真实 Python 转成模型本身就是信任边界，验证模型不能自动覆盖整个仓库。

3. 3

   图 2 中的机械门控先排除空证明

   参考实现必须通过，修复前的实现必须失败；加入反例、变异测试和防逃逸检查。未改变函数的公理要探测，模型与真实程序要做差分运行。十万级生成输入能够查出不一致，但有限测试不是程序等价性的完整证明。

4. 4

   再审计规格是否真正表达任务

   独立模型审计公理、可接受输入、可靠性、区分能力和忠实性。模型投票是经过测量的审计方法，仍不是形式证明；参考行为不充分的 issue 还会出现信息冲突：给出精确规格可能透露公开问题中没有的答案。相关实例需要单独标注或剔除分析。

5. 5

   用附录 I 的失败案例理解抽象损失

   Django 的日期组件会产生 ValueError 或 OverflowError。一个候选规格把两者合成“回退”，因此候选补丁与证明一致、证明也通过；隐藏测试却要求溢出返回精确的 0-0-0，而另一错误保留原输入。丢掉返回字符串的抽象无法辨别两种补丁，继续加证明步骤也补不回来。

6. 6

   比较收益时先控制定位与规格提示量

   主实验覆盖 500 个 SWE-bench Verified issue，扩展到 SWE-bench Pro 的 242 个可用 Python 实例。已提供规格常能帮助旧基准，但 Pro 上没有一致收益；自写规格也不自动提升修复成功率，不能把“形式验证工具可运行”变成“真实修复可靠”的同义词。

以下为作者报告；已阅读 v1 全文及附录，本站未独立执行研究实验。实验条件与编辑解读分别列出。

附录 J 声明拟发布的自有管线和规格采用 MIT；本次未核实可下载正式仓库。MIT 声明不覆盖上游 issue、参考补丁、容器或模型 API，不能视为全部制品已开源。

LICENSE论文 arXiv 非独占分发；自有制品声明 MIT，实际发行待核实；引用的仓库内容各遵循原项目许可。