标题： VERINA：可验证代码生成的基准测试 显示英文标题

标题： VERINA: Benchmarking Verifiable Code Generation

摘要： 大型语言模型（LLMs）在软件开发中的应用日益广泛，但确保LLM生成代码的正确性仍然具有挑战性，并且通常需要耗费高昂的人工审查成本。 可验证代码生成——即联合生成代码、规范以及代码与规范一致性的证明——提供了一种解决这一局限性并进一步释放LLM在编码方面优势的有前景的途径。 然而，目前在评估方面存在显著差距：现有的基准测试往往缺乏对端到端可验证代码生成的支持。 在本文中，我们引入了Verina（可验证代码生成竞技场），这是一个高质量的基准测试集，能够全面而模块化地评估代码、规范和证明生成及其组合。 Verina由189个手动精心策划的Lean编程任务组成，每个任务都有详细的问题描述、参考实现、形式化规范以及广泛的测试套件。 我们的广泛评估揭示了当前最先进的LLMs在可验证代码生成方面的重大挑战，尤其是在证明生成方面，这凸显了改进基于LLM的定理证明器在验证领域的重要性。 最佳模型OpenAI o4-mini在每个任务上仅生成了61.4%的正确代码、51.0%的准确且完整的规范以及3.6%的成功证明。 我们希望Verina能通过提供一个严谨且全面的基准测试集推动可验证代码生成的进步。 我们将数据集发布在https://huggingface.co/datasets/sunblaze-ucb/verina上，并将评估代码发布在https://github.com/sunblaze-ucb/verina上。 显示英文摘要

摘要： Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often lack support for end-to-end verifiable code generation. In this paper, we introduce Verina (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. Verina consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o4-mini, generates only 61.4% correct code, 51.0% sound and complete specifications, and 3.6% successful proofs, with one trial per task. We hope Verina will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.