Self-Spec Verifiable Code Generation
作者: Jiaru Qian, Yihong Dong, Yongmin Li, Hao Zhu, Bin Gu, Ge Li
分类: cs.SE, cs.AI
发布日期: 2026-09-30
💡 一句话要点
提出VeriCodeBench以解决LLM生成代码的可靠性问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 代码生成 形式验证 大型语言模型 自我规范 软件开发 机器学习 约束引导
📋 核心要点
- 现有方法在评估LLMs生成代码的能力时，主要分阶段进行，忽视了整体成功率的评估。
- 本文提出VeriCodeBench基准，LLM在生成代码时仅依赖自身生成的规范，覆盖多种编程语言。
- 实验表明，CodeNova显著提升了LLMs在自我规范可验证代码生成中的表现，尤其是在规范生成方面。
📝 摘要（中文）
大型语言模型（LLMs）在生成代码时可能会在测试未覆盖的边缘案例中产生不可靠的代码，而形式验证可以提供机器可检查的保证。现有的基准测试主要分阶段评估LLMs的能力，忽视了阶段性表现是否能转化为端到端的成功。此外，现有基准主要集中在单一的证明导向语言和数学结构任务上，覆盖面有限。本文提出了VeriCodeBench，一个自我规范可验证代码生成的基准，LLM在整个过程中仅依赖自身生成的规范和代码。该基准包含400个涵盖C、Java、Rust和Python的语言本地问题，评估规范覆盖、代码有效性和整体问题成功率。我们进一步引入CodeNova，通过约束引导的规范明确需求，并利用验证器反馈指导针对性实现修复。实验结果显示，自生成的规范仍是主要瓶颈，而提供更复杂的规范未必能提高验证成功率。CodeNova在所有评估指标上显著提升了性能，使Claude Sonnet 5在自我规范协议下取得最佳结果。
🔬 方法详解
问题定义：本文旨在解决大型语言模型在生成代码时的可靠性问题，现有方法在评估过程中未能有效考虑整体成功率，且主要集中在单一语言和数学任务上。
核心思路：提出VeriCodeBench基准，LLM在整个代码生成过程中仅依赖自身生成的规范和代码，旨在提高生成代码的可靠性和验证能力。
技术框架：整体架构包括规范生成、代码生成和验证三个主要模块，LLM通过自我生成的规范指导代码实现，并通过验证器反馈进行修复。
关键创新：最重要的创新在于引入了自我规范生成的概念，LLM不再依赖外部规范，从而提高了生成代码的独立性和灵活性。
关键设计：在设计中，使用了约束引导的规范生成方法，并通过验证器的反馈机制来指导代码的针对性修复，确保生成代码的有效性和可验证性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，CodeNova在所有评估指标上显著提升了LLMs的性能，尤其是在自我规范生成方面，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.