VeriContest：可验证代码生成的竞争性编程基准

大语言模型 可以从自然语言生成有用的代码，但它们的输出没有正确性保证。可验证的代码生成提供了一条超越测试的途径，要求模型不仅生成可执行代码，还生成正式规范和机器可检查的证明。然而，这一方向的进展很难衡量：现有的基准测试通常很小，只关注管道的一部分，缺乏 真值 证明或严格的规范验证，或者目标验证设置远离主流软件开发。我们推出了 VeriContest，这是来自 LeetCode 和 Codeforces 的 946 个竞争性编程问题的基准，用于使用 Verus 在 Rust 中生成可验证的代码。每个问题都将自然语言描述与专家验证的形式规范、法官接受的 Rust 代码、Verus 检查的证明以及正负测试套件配对。 VeriContest 是通过一个三阶段管道构建的，该管道从手动验证的种子问题扩展到具有人在环审核的半自动扩展。为了进一步加强基准质量，我们使用测试作为额外的质量保证层来验证后置条件的完整性。 VeriContest 支持规范生成、代码生成、证明生成和端到端验证程序综合的独立评估和组合评估。评估十个最先进的模型揭示了编码能力和可验证代码生成之间的巨大差距：最强的模型在自然语言到代码生成方面达到了 92.18%，但在规范生成方面仅为 48.31%，在证明生成方面仅为 13.95%，在端到端方面仅为 5.29%。这些结果将证明和规范生成确定为模型的中心瓶颈，并将 VeriContest 建立为一个严格的平台，用于测量和训练未来系统，生成具有机器可检查正确性的代码。