SWE-Proof：语言模型可以通过机器检查的证明解决现实世界的问题吗？

确保LLM生成代码的正确性是现代软件工程的核心挑战。代理代码生成的基准检查保留测试套件的正确性，这些测试套件本质上是不完整的，并且越来越容易被记住。形式验证避免了这两个问题，但现有的工作仅涵盖独立任务，其规范作为输入给出，而不是真正的问题，这些任务涉及大型存储库并以模糊的自然语言陈述意图。我们提出了 Benchproofer，这是一种管道，可将具有已知正确补丁的编码任务转变为正式验证的任务：它为新代码编写规范，用公理总结代码调用的现有函数，并且仅在机械门和对抗门一致后才允许实例。将其应用于 SWE-bench Verified 会产生 SWE-Proof，即 500 个实际问题，其正确性经过正式验证而不是测试，并且它扩展到 SWE-bench Pro。在评估 Claude Opus 4.8 时，我们发现验证捕获了测试遗漏的内容：四分之一的测试通过补丁承认反例，这是结构化自然语言规范无法修复的，而正确的形式化规范则将分辨率从 85% 提升到 95%。编写该规范是最困难的部分：必须编写自己的代理在无帮助的基线上不会获得任何收益，并且这些规范中只有 56% 通过了我们的审核。通常的失败是忠诚，一种限制部分所需行为而让其余行为自由的规范。规范质量仍然跟踪结果，92% 的未解决实例失败，而 51% 的已解决实例失败，这使得忠实的规范综合成为一个具体的开放问题。