确保LLM生成代码的正确性是现代软件工程的核心挑战。现有的代理式代码生成基准使用保留测试集检查正确性，但测试集不完整且易受记忆影响。形式化验证可以规避这些问题，但过去仅针对输入中给出规格的独立任务，无法处理涉及大型代码库、意图以模糊自然语言表达的真实问题。我们提出Benchproofer流水线，将已知正确补丁的编码任务转化为形式化可验证的任务：它为新代码编写规格，使用公理概括代码调用的现有函数，并在机械和对抗门都通过后才接受实例。将其应用于SWE‑bench Verified得到SWE‑Proof，包含500个真实问题，其正确性通过形式化验证而非测试，并可扩展到SWE‑bench Pro。实验在两种前沿模型上显示，验证捕获了测试遗漏的错误：约四分之一到一半的通过测试的补丁存在反例，结构化的自然语言规格并未解决，而正确的形式化规格将Opus 4.8的解决率从85%提升至95%。编写规格是难点：需要自行生成规格的模型相比无帮助基线没有提升，只有62%的规格通过审计。主要失败模式是忠实性不足，即规格只约束了部分行为，留下其余自由。规格质量仍与结果相关，未解决实例中有89%规格不合格，而已解决实例中为47%，因此生成忠实规格是一个具体的开放问题。
点评