构建最大代码形式验证基准，测试大模型自动生成正确代码的能力。
A benchmark for vericoding: formally verified program synthesis
- 用形式化规范生成可验证代码，对比传统自然语言生成方式。
- 在Dafny上成功率达82%，远超Verus/Rust的44%和Lean的27%。
- 适合关注可信AI与自动化编程的研究者与开发者。
我们提出并测试了目前最大的形式化编码（vericoding）基准，用于评估大模型从形式化规范生成可正式验证代码的能力，区别于基于自然语言描述可能产生错误代码的“ vibe coding”。该基准包含12,504个形式化规范，其中3,029个来自Dafny，2,334个来自Verus/Rust，7,141个来自Lean；其中6,174个为全新未见问题。使用现成大模型，验证成功率分别为：Lean 27%，Verus/Rust 44%，Dafny 82%。添加自然语言描述对性能无显著提升。此外，过去一年中，纯Dafny验证任务的成功率从68%提升至96%。基准与结果已公开于https://github.com/Beneficial-AI-Foundation/vericoding-benchmark。
原文摘要 · Abstract (English)
We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。