自规范可验证代码生成

大语言模型 (LLM) 可能会在测试遗漏的极端情况下生成不可靠的代码，而形式验证可以提供机器可检查的保证。最近，研究人员提出了几个基准来评估LLM生成形式化可验证代码的能力，其中LLM需要制定形式化规范，生成相应的代码，并验证其正确性。然而，现有的基准测试有两个关键限制：（I）它们主要评估规范和分阶段的代码生成，代码生成通常以预言机规范为条件。这种设置忽略了强大的阶段性表现是否会转化为端到端的成功。 (II)它们主要关注单一的面向证明的语言和数学结构的任务，对软件开发中常见任务的覆盖范围有限。在本文中，我们介绍了 VeriCodeBench，一个自规范可验证代码生成的基准，其中大语言模型在整个过程中仅依赖于自己生成的规范和代码。 VeriCodeBench 包含 400 个跨 C、Java、Rust 和 Python 的语言本机问题，涵盖软件开发中的实际问题。我们评估规范覆盖率、代码有效性和联合问题级别的成功。我们进一步引入CodeNova来增强大语言模型在自规范可验证代码生成方面的能力。 CodeNova 通过约束引导的规范明确需求，并使用验证者反馈来指导有针对性的实施修复。实验结果表明，自行生成的规范仍然是主要瓶颈，而提供更复杂的规范不一定会带来更高的验证成功率。 CodeNova 大幅提高了所有评估指标的性能，使 Claude Sonnet 5 在自规范协议下取得了最强的结果。