自规约可验证代码生成基准与 CodeNova 方法

arXiv 论文提出 VeriCodeBench，用于评估 LLM 在“自规约可验证代码生成”中的表现：模型需完全依据自己生成的 formal specification 写代码并完成验证。基准包含 C、Java、Rust、Python 四门语言的 400 道原生题目，评估规约覆盖度、代码有效性与端到端成功率；论文同时提出 CodeNova，用约束引导规约与验证器反馈修复实现。

此前的可验证代码生成基准多按阶段分别评估，且代码生成常以 oracle specification 为条件，难以反映端到端能力；同时集中于单一证明导向语言和数学结构任务。VeriCodeBench 改为只用模型自产规约，并覆盖四种通用语言与软件开发常见问题，评估口径由此变化。

该工作把规约与实现视为一条闭环：先由约束引导模型把需求显式写成 formal specification，再生成代码，随后用验证器反馈定位失败并做针对性修复。评估维度拆为规约覆盖度、代码有效性和问题级联合成功率，用于观察阶段指标是否能转化为端到端结果。

对研发流程而言，这意味着可验证代码生成的评测重点从“给定正确规约能否写对代码”转向“模型能否自己写对规约并端到端通过验证”。若采用 CodeNova 类反馈修复机制，代码生成工具可在验证失败后自动迭代，减少人工补规约与定位反例的成本，但实际收益仍取决于基准结果与验证器覆盖范围。

• 在代码生成产品中加入“先写可验证规约、再生成代码”的默认流程，并暴露规约供人工审阅。
• 将验证器反馈接入代码修复循环，对失败用例自动生成针对性补丁并记录修复轨迹。
• 围绕 C、Java、Rust、Python 建立内部自规约验证评测集，用于模型选型和回归测试。

• VeriCodeBench 的 400 道题具体分布与难度分层如何？
• 自生成规约的端到端成功率与 oracle specification 条件下的阶段成功率差距有多大？
• CodeNova 的验证器反馈修复是否依赖特定验证工具或语言？
• 该基准与 CodeNova 是否已公开代码、数据与评测脚本？