SWE-Proof：语言模型能否用机器检查的证明解决现实世界问题？
SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
另 1 家 · 查看机构详情
- UC Berkeley（加州大学伯克利分校）
- Georgia Tech（佐治亚理工学院）
- UIUC（伊利诺伊大学厄巴纳-香槟分校）
- AWS AI Labs（亚马逊云科技人工智能实验室）
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
本文提出Benchproofer流水线，将真实代码任务转化为形式化验证问题，构建SWE-Proof基准，证明形式化规范能捕获测试遗漏的错误并提升模型解决率，同时揭示规范忠实性合成的开放挑战。
中文摘要 AI 辅助
确保LLM生成代码的正确性是现代软件工程的一个核心挑战。用于智能体代码生成的基准测试通过保留的测试套件来检查正确性，这些测试套件本质上是不完整的，并且越来越容易被记忆。形式化验证避免了这两个问题，但现有工作仅覆盖规范作为输入给出的独立任务，而非涉及大型代码库并以模糊自然语言表达意图的真实问题。我们提出了Benchproofer，一个将带有已知正确补丁的编码任务转化为形式化验证任务的流水线：它为新代码编写规范，用公理总结代码调用的现有函数，并且仅在机械门和对抗门都同意后才接受一个实例。将其应用于SWE-bench Verified，我们得到了SWE-Proof，即500个正确性经过形式化验证而非测试的真实问题，并且它扩展到了SWE-bench Pro。在两个前沿模型上，验证捕获了测试遗漏的内容：四分之一到一半的通过测试的补丁存在反例，而结构化的自然语言规范无法解决这些问题，而正确的形式化规范将Opus 4.8的解决率从85%提升到95%。编写该规范是困难的部分：必须自己编写规范的模型相对于无辅助基线没有获得任何收益，并且它们的规范中只有62%通过了我们的审计。常见的失败是忠实性，即规范约束了部分所需行为，而让其余部分保持自由。规范质量仍然与结果相关，在未解决实例中失败率为89%，而在已解决实例中为47%，这使得忠实的规范合成成为一个具体的开放问题。
英文摘要
Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suites, which are inherently incomplete and increasingly susceptible to memorization. Formal verification avoids both problems, but existing work covers only standalone tasks whose specifications are given as input, not real issues, which touch large repositories and state intent in vague natural language. We present Benchproofer, a pipeline that turns a coding task with a known correct patch into a formally verified one: it writes a specification for the new code, summarizes the existing functions that code calls with axioms, and admits an instance only after mechanical and adversarial gates agree. Applying it to SWE-bench Verified yields SWE-Proof, 500 real issues whose correctness is formally verified rather than tested, and it extends to SWE-bench Pro. Evaluating Claude Opus 4.8, we find that verification catches what tests miss: a quarter of test-passing patches admit counterexamples, which a structured natural-language specification does not fix, while a correct formal one lifts resolution from 85% to 95%. Writing that specification is the hard part: an agent that must write its own gains nothing over an unaided baseline, and only 56% of those specifications pass our audit. The usual failure is faithfulness, a specification that constrains part of the required behavior and leaves the rest free. Specification quality still tracks the outcome, failing on 92% of unresolved instances against 51% of resolved ones, making faithful specification synthesis a concrete open problem.
