发表机构
Peking University; aiXcoder; Shanghai Jiao Tong University; Beijing Institute of Control Engineering（北京大学; aiXcoder; 上海交通大学; 北京控制工程研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对LLM生成可验证代码的端到端挑战，提出VeriCodeBench基准和CodeNova方法，通过约束引导规格与验证器反馈修复，显著提升自规格代码生成成功率。
AI 中文摘要
大型语言模型（LLMs）可能在测试遗漏的边界情况下生成不可靠的代码，而形式化验证可以提供机器可检查的保证。近期，研究人员提出了多个基准来评估LLMs生成形式化可验证代码的能力，其中LLMs需要制定形式化规格、生成相应代码并验证其正确性。然而，现有基准存在两个关键局限：（I）它们主要分阶段评估规格和代码生成，代码生成通常以预言机规格为条件。这种设置忽略了强分阶段性能是否能转化为端到端成功。（II）它们主要关注单一面向证明的语言和数学结构化任务，对软件开发中常见任务的覆盖有限。在本文中，我们引入了VeriCodeBench，一个用于自规格可验证代码生成的基准，其中LLM在整个过程中仅依赖其自身生成的规格和代码。VeriCodeBench包含400个跨C、Java、Rust和Python的语言原生问题，涵盖软件开发中的实际关注点。我们评估了规格覆盖率、代码有效性和联合问题级成功率。我们进一步引入CodeNova来增强LLMs在自规格可验证代码生成中的能力。CodeNova通过约束引导的规格使需求显式化，并利用验证器反馈指导有针对性的实现修复。实验结果表明，自生成规格仍然是一个主要瓶颈，而提供更复杂的规格不一定导致更高的验证成功率。CodeNova在所有评估指标上显著提升了性能，使Claude Sonnet 5在自规格协议下取得了最强结果。
英文摘要
Large language models (LLMs) may generate unreliable code on corner cases missed by testing, while formal verification can provide machine-checkable guarantees. Recently, researchers have proposed several benchmarks to evaluate the capabilities of LLMs in generating formally verifiable code, where LLMs need to formulate formal specifications, generate the corresponding code, and verify its correctness. However, existing benchmarks have two key limitations: (I) They primarily evaluate specification and code generation stage-wise, with code generation typically conditioned on an oracle specification. This setup overlooks whether strong stage-wise performance translates into end-to-end success. (II)They mainly focus on a single proof-oriented language and mathematically structured tasks, offering limited coverage of tasks common in software development. In this paper, we introduce VeriCodeBench, a benchmark for self-spec verifiable code generation, where the LLM relies solely on its own generated specification and code throughout the entire process. VeriCodeBench contains 400 language-native problems across C, Java, Rust, and Python, covering practical concerns in software development. We evaluate specification coverage, code validity, and joint problem-level success. We further introduce CodeNova to enhance the capabilities of LLMs in self-spec verifiable code generation. CodeNova makes requirements explicit through constraint-guided specification and uses verifier feedback to guide targeted implementation repairs. Experimental results reveal that self-generated specifications remain a major bottleneck, while providing more sophisticated specifications may not necessarily lead to higher verification success rates. CodeNova substantially improves performance across all evaluation metrics, enabling Claude Sonnet 5 to achieve the strongest results under the self-spec protocol.
