Verina

Verina（可验证代码生成竞技场）是一个高质量的基准测试，用于全面和模块化地评估代码、规范和证明生成及其组合。数据集中的每个数据点都组织为一个文件夹，包含以下文件：`task.json`（描述任务的JSON文件）、`description.txt`（编程任务的描述）、`task.lean`（包含真实代码、规范和证明的Lean 4文件）、`test.json`和`reject_inputs.json`（包含任务的测试用例和拒绝输入的JSON文件）。

Verina (Verifiable Code Generation Arena) is a high-quality benchmark designed for comprehensive and modular evaluation of code, specification, and proof generation, as well as their combinations. Each data point in the dataset is organized into a folder containing the following files: `task.` (a JSON file describing the task), `description.txt` (a description of the programming task), `task.lean` (a Lean 4 file containing actual code, specifications, and proofs), and `test.` and `reject_inputs.` (JSON files containing the task's test cases and reject inputs).

原始信息汇总

Verina数据集概述

数据集简介

• 名称：Verina (Verifiable Code Generation Arena)
• 类型：代码生成验证基准测试数据集
• 用途：用于全面评估代码、规范和证明生成及其组合

数据集内容

• 文件结构：每个数据点包含以下文件
  • task.json：任务描述JSON文件（包含ID、任务签名、数据文件路径等元数据）
  • description.txt：编程任务描述
  • task.lean：包含真实代码、规范和证明的Lean 4文件
  • test.json和reject_inputs.json：测试用例和被拒绝输入的JSON文件

获取方式

• GitHub存储路径：datasets/verina/目录
• HuggingFace版本：https://huggingface.co/datasets/sunblaze-ucb/verina

相关资源

• 项目网站：https://sunblaze-ucb.github.io/verina
• 研究论文：https://arxiv.org/pdf/2505.23135

引用格式

bibtex @article{ye2025verina, title={VERINA: Benchmarking Verifiable Code Generation}, author={Ye, Zhe and Yan, Zhengxu and He, Jingxuan and Kasriel, Timothe and Yang, Kaiyu and Song, Dawn}, journal={arXiv preprint arXiv:2505.23135}, year={2025} }

搜集汇总

数据集介绍

构建方式

Verina数据集作为可验证代码生成领域的基准测试平台，其构建过程体现了严谨的学术规范。研究团队采用模块化架构设计，每个数据点均以独立文件夹形式组织，包含任务描述文件、Lean4格式的代码规范与证明文件，以及标准化测试用例集。通过GitHub和HuggingFace双平台发布，数据集采用版本控制管理，并开放社区贡献机制，确保数据持续优化更新。

特点

该数据集最显著的特征在于其多维评估体系，能够对代码生成、规范生成和证明生成三大核心能力进行独立或组合式测评。数据集包含精心设计的测试用例和拒绝输入样本，采用Lean4定理证明器作为验证基础，保证了评估结果的数学严谨性。其模块化设计支持灵活的任务组合，为研究者提供了细粒度的性能分析可能。

使用方法

使用Verina需配置Lean4环境和Docker容器，通过Prefect工作流管理系统执行基准测试。用户可自定义配置文件选择评估任务类型，支持主流大语言模型接口接入。基准测试分为生成与评估两个阶段，允许分布式并行处理。数据集提供Python API用于结果分析，开发者可通过继承Solution类实现自定义解决方案，其模块化设计便于扩展新的评估维度。

背景与挑战

背景概述

Verina（Verifiable Code Generation Arena）是由加州大学伯克利分校的研究团队于2025年推出的高质量基准测试平台，旨在全面评估代码、规范及证明生成的能力及其组合效果。该数据集由Zhe Ye、Zhengxu Yan等学者主导开发，基于Lean 4语言构建，每个数据点包含任务描述、真实代码、规范及证明文件，为形式化验证领域提供了标准化评估框架。其创新性体现在对可验证代码生成任务的模块化分解，推动了程序验证与人工智能交叉领域的研究进展，相关成果已发表于arXiv预印本平台。

当前挑战

Verina需解决形式化验证中代码与数学证明协同生成的复杂性挑战，包括规范表达的精确性、证明步骤的完备性，以及组合任务中误差传递的控制。数据集构建过程中面临多重技术难点：Lean 4语言的高学习成本导致标注难度增加，测试用例需同时满足代码功能正确性与逻辑证明有效性，而跨任务评估指标的标准化设计也需平衡自动化程度与人工验证需求。此外，大规模语言模型在生成可验证代码时存在的幻觉现象，进一步增加了基准测试的可靠性保障难度。

常用场景

经典使用场景

在形式化验证和代码生成领域，Verina数据集为研究者提供了一个标准化的评估平台，用于测试和比较不同模型在代码、规范和证明生成任务上的性能。该数据集通过精心设计的任务文件夹结构，包括任务描述、Lean 4文件以及测试用例，使得研究者能够全面评估模型在复杂编程任务中的表现。Verina的模块化设计特别适合用于验证生成式模型在形式化验证环境中的能力，为相关研究提供了高质量的基准数据。

实际应用

在实际应用中，Verina数据集可用于开发和测试自动化代码生成工具，特别是在需要高可靠性的领域，如航空航天、金融系统和安全关键型软件。通过使用Verina提供的标准化任务，开发者可以评估其工具在生成可验证代码方面的能力，从而提高软件开发的效率和可靠性。此外，Verina还可用于教育领域，帮助学生和研究者理解形式化验证和代码生成的实际应用。

衍生相关工作

Verina数据集已经催生了一系列相关研究，特别是在形式化验证和代码生成领域。基于Verina的基准测试，研究者开发了多种新型模型和方法，如结合大型语言模型的代码生成技术和自动化证明生成系统。这些工作不仅扩展了Verina的应用范围，也推动了形式化验证技术的发展。Verina的模块化设计还启发了其他领域的研究者开发类似的综合评估基准。