构建首个大规模代码正确性验证基准，挑战AI同时写出代码和证明。
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
- 用Lean 4定理替代单元测试，要求生成代码并证明其正确性
- 在100个样本的306个定理上，Sonnet正确证明率30%，Gemini为18%
- 适合研究程序合成与形式化验证的学者及工具开发者
我们提出形式化验证自动化编程进展标准（FVAPPS），包含4715个样本，是目前最大的形式化验证基准，其中1083个经过精心筛选和质量控制。此前，APPS提供了一个用于编写可通过单元测试验证的编程谜题的基准，常见于软件工程领域的技术评估。FVAPPS借鉴交互式定理证明的最新方法，将单元测试推广为无证明的Lean 4定理（使用Lean的"sorry"关键字）。在随机选取的100个样本共406个定理中，Sonnet成功证明30%，Gemini为18%。我们向机器学习与程序合成领域发起挑战：不仅要解决通用编程问题，还需完成其对应的正确性规范。该基准已开源，地址为https://huggingface.co/datasets/quinn-dougherty/fvapps。
原文摘要 · Abstract (English)
We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4715 samples for writing programs and proving their correctness, the largest formal verification benchmark, including 1083 curated and quality controlled samples. Previously, APPS provided a benchmark and dataset for programming puzzles to be completed in Python and checked against unit tests, of the kind seen in technical assessments in the software engineering industry. Building upon recent approaches for benchmarks in interactive theorem proving, we generalize the unit tests to Lean 4 theorems given without proof (i.e., using Lean's "sorry" keyword). On the 406 theorems of 100 randomly selected samples, Sonnet correctly proves 30% and Gemini correctly proves 18%. We challenge the machine learning and program synthesis communities to solve both each general purpose programming problem and its associated correctness specifications. The benchmark is available at https://huggingface.co/datasets/quinn-dougherty/fvapps.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。