VERINA

VERINA是一个高质量的基准数据集，旨在全面评估代码、规范和证明的生成及其组合。它包含189个经过人工整理的Lean编程任务，具有详细的问题描述、参考实现、形式规范和广泛的测试套件。VERINA为评估可验证代码生成提供了一个严格和全面的平台，并揭示了当前最先进的语言模型在可验证代码生成方面的挑战。数据集涵盖了从规范引导的代码生成到端到端可验证代码生成的各种实际场景。

VERINA is a high-quality benchmark dataset designed to comprehensively evaluate the generation of code, specifications, proofs, and their combinations. It comprises 189 manually curated Lean programming tasks, complete with detailed problem descriptions, reference implementations, formal specifications, and an extensive test suite. VERINA provides a rigorous and comprehensive platform for evaluating verifiable code generation, and reveals the challenges faced by current state-of-the-art language models in the domain of verifiable code generation. The dataset covers various real-world scenarios ranging from specification-guided code generation to end-to-end verifiable code generation.

原始信息汇总

Verina数据集概述

基本信息

• 许可证: GPL-3.0
• 数据集大小: 609,882字节
• 下载大小: 211,743字节
• 训练集样本数: 189

数据集结构

特征

• id: 字符串类型，唯一标识符
• description: 字符串类型，描述信息
• lean_code: 字符串类型，Lean代码
• signature: 结构体，包含以下字段：
  • name: 字符串类型，名称
  • parameters: 序列，包含以下字段：
    • param_name: 字符串类型，参数名称
    • param_type: 字符串类型，参数类型
  • return_type: 字符串类型，返回类型
• metadata: 结构体，包含以下字段：
  • upstream: 结构体，包含以下字段：
    • name: 字符串类型，上游名称
    • link: 字符串类型，链接
    • task_id: 字符串类型，任务ID
    • student_id: 整数序列，学生ID
• tests: 序列，包含以下字段：
  • input: 字符串类型，输入
  • expected: 字符串序列，预期输出
  • unexpected: 字符串序列，非预期输出
• reject_inputs: 序列，包含以下字段：
  • input: 字符串类型，输入
• difficulty: 字符串类型，难度等级

数据集配置

• 默认配置:
  • 数据文件:
    • 训练集路径: data/train-*

搜集汇总

数据集介绍

构建方式

VERINA数据集的构建过程体现了严谨的质量控制与多源数据整合。研究团队从MBPP、LiveCodeBench和LeetCode等平台精选189个编程任务，通过人工翻译（Dafny转Lean）和原创编写（学生课程作业）两种方式构建。每个样本包含自然语言描述、Lean代码实现、形式化规范、证明及完整测试套件，并经过双重人工校验。测试用例设计采用100%行覆盖率和正负案例平衡策略，通过coverage.py工具验证覆盖率，确保规范与实现的严格对齐。数据集分为基础版（VERINA-BASIC）和进阶版（VERINA-ADV），分别对应不同复杂度任务，其中进阶版代码行数中位数达16行，规范行数中位数7行，显著提升挑战性。

使用方法

使用VERINA需遵循其模块化评估框架。对于代码生成任务，采用pass@k指标通过测试用例验证功能正确性；规范生成任务需通过Lean编译器检查逻辑一致性，并利用正负测试验证其与基准规范的关系；证明生成则依赖Lean交互式定理证明器验证。评估支持三种典型组合场景：1）规范引导的代码生成（输入规范生成代码+证明），2）代码反推规范（输入代码生成规范+证明），3）端到端可验证生成（仅输入描述独立生成代码、规范及证明）。研究建议使用2-shot提示策略，并通过DSPy框架结构化输出。数据集提供HuggingFace和GitHub双平台访问，包含完整评估代码与标准化提示模板。

背景与挑战

背景概述

VERINA（Verifiable Code Generation Arena）是由加州大学伯克利分校和Meta FAIR的研究团队于2025年推出的高质量基准测试数据集，专注于可验证代码生成领域。该数据集包含189个经过人工精心筛选的Lean编程任务，每个任务均配备详细的问题描述、参考实现、形式化规范及全面的测试套件。VERINA的创建旨在解决当前基准测试在端到端可验证代码生成评估方面的不足，为代码、规范及证明生成等核心任务提供模块化评估框架。其创新性在于首次实现了对形式化验证全流程的标准化测评，推动了大型语言模型在可信代码生成领域的研究进程。

当前挑战

VERINA面临的核心挑战体现在两个维度：领域问题层面，当前最先进的大型语言模型在可验证代码生成任务中表现欠佳，尤其在证明生成环节成功率仅为3.6%，凸显出形式化验证能力与实用化要求间的巨大鸿沟；数据构建层面，确保形式化规范与测试套件的完备性需克服三重困难：1) 人工编写数学证明的高专业门槛导致标注成本激增，2) 测试用例需同时覆盖正向功能验证与负向边界情况，3) 防止规范与代码间出现定义等价性而降低验证难度。这些挑战使得构建兼具严谨性与可扩展性的验证基准成为极具复杂性的系统工程。

常用场景

经典使用场景

VERINA数据集在可验证代码生成领域具有重要应用价值，其经典使用场景包括评估大型语言模型（LLMs）在生成代码、规范及证明方面的能力。该数据集通过精心设计的189个编程任务，覆盖了从简单到复杂的多种难度级别，为研究者提供了一个全面评估LLMs在可验证代码生成任务上表现的平台。特别是在Lean编程语言环境下，VERINA能够支持端到端的可验证代码生成评估，包括代码生成、规范生成和证明生成三个关键任务。

解决学术问题

VERINA数据集解决了当前可验证代码生成领域缺乏高质量、全面评估基准的问题。传统基准往往仅关注单一任务，如代码生成或证明生成，而VERINA首次实现了对代码、规范和证明生成及其组合任务的全面评估。该数据集通过严格的质控流程，确保了每个样本的自然语言描述清晰、形式化规范准确，并配备了全面的测试套件，为研究者提供了一个可靠的评估平台。VERINA的引入填补了该领域的空白，为可验证代码生成的研究提供了重要支撑。

实际应用

在实际应用方面，VERINA数据集可广泛应用于软件开发自动化工具的评估与改进。例如，在集成开发环境（IDE）中，基于LLMs的代码补全工具可以利用VERINA来评估其生成代码的正确性和可验证性。此外，该数据集还可用于训练和评估专门用于形式化验证的AI系统，帮助提高软件开发的可靠性和安全性。在教育领域，VERINA可作为教学资源，帮助学生理解形式化规范和证明在软件开发中的重要性。

数据集最近研究

最新研究方向

随着大型语言模型（LLMs）在软件开发中的广泛应用，确保生成代码的正确性成为关键挑战。VERINA（Verifiable Code Generation Arena）作为高质量基准测试集，专注于评估可验证代码生成的全面性和模块化能力。该数据集包含189个精心设计的编程任务，涵盖代码、规范和证明生成三个核心任务，为LLMs在形式化验证领域的性能提供了严谨的评估平台。前沿研究集中在提升LLMs在定理证明领域的表现，特别是在交互式定理证明（ITP）系统中生成正确证明的能力。VERINA的推出不仅填补了当前基准测试在端到端可验证代码生成评估上的空白，还为推动LLMs在自动化软件验证领域的发展提供了重要工具。

相关研究论文

• VERINA: Benchmarking Verifiable Code Generation

  加州大学伯克利分校, Meta FAIR · 2025年