Vericoding Benchmark

Vericoding基准是一个用于形式化验证程序合成的数据集，包含12,504个任务，以Dafny、Lean和Verus语言提供规范文件，并包含CSV格式的元数据和JSONL格式的解析数据，支持AI和人类编码的实验

Vericoding Benchmark is a dataset for formal verification of program synthesis. It contains 12,504 tasks, with specification files provided in Dafny, Lean and Verus languages, and includes CSV-formatted metadata and JSONL-formatted parsed data, supporting experiments involving both AI-generated and human-written code.

原始信息汇总

Vericoding Benchmark 数据集概述

数据集基本信息

• 数据集名称: A Benchmark For Vericoding: Formally Verified Program Synthesis
• 任务数量: 12,504个任务
• 实验数量: 55,397个实验
• 支持语言: Dafny, Lean, Verus

核心文件说明

主要数据文件

• vericoding_benchmark_v1.csv: 包含所有12,504个任务的Vericoding ID、来源和来源ID，以及质量分析的额外元数据
• vericoding_results_v1.csv: 包含所有55,397个vericoding任务实验的结果

目录结构

• specs目录: 包含所有12,504个任务的Dafny、Lean和Verus规范文件

  • 包含可编译文件（包含部分sorry或assume false）
  • 包含不可编译文件（特别是从其他语言翻译后）
  • 文件分解为前导码、规范、代码和后导码等组件

• jsonl目录: 按不同语言分类的任务和问题，解析为不同组件并以JSON行格式存储

  • 包含部分任务的自然语言描述
  • 便于实验使用

• vericoded目录: 将包含AI验证编码器填充解决方案的任务

• handcoded目录: 将包含人工编码器填充解决方案的任务

数据来源

原始数据集

1. DafnyBench

   • 路径: benchmarks/dafny/dafnybench
   • 来源: https://github.com/sun-wendy/DafnyBench

2. NumPyTriple

   • 路径: benchmarks/lean/numpy_triple
   • 来源: NumPy文档派生
   • 规范格式: 新的Hoare三元组格式

3. NumPySimple

   • 路径: benchmarks/lean/numpy_simple
   • 来源: NumPy文档派生
   • 规范格式: 经典Lean格式

4. Verina

   • 路径: benchmarks/lean/verina
   • 来源: https://github.com/sunblaze-ucb/verina

5. APPS

   • 路径: benchmarks/dafny/apps
   • 来源: https://github.com/hendrycks/apps

6. FVAPPS

   • 路径: benchmarks/lean/fvapps
   • 来源: https://huggingface.co/datasets/quinn-dougherty/fvapps

7. VerifiedCogen

   • 路径: benchmarks/verus/verified_cogen
   • 来源: https://github.com/JetBrains-Research/verified-cogen

8. BigNum

   • 路径: benchmarks/dafny/bignum
   • 来源: 从头编写

9. HumanEval和Clever

   • 路径: benchmarks/dafny/humaneval, benchmarks/lean/clever
   • 来源:
     • https://github.com/openai/human-eval
     • https://github.com/JetBrains-Research/HumanEval-Dafny
     • https://github.com/trishullab/clever

数据转换说明

• Dafny文件主要从原始Python源码翻译而来
• 部分Dafny文件来自Jetbrains Research的HumanEval Dafny仓库
• Lean文件来自Clever基准测试，最初源自HumanEval基准测试
• Clever中缺少HumanEval问题22、137、162（原因在Clever论文中说明）

搜集汇总

数据集介绍

构建方式

Vericoding Benchmark的构建过程体现了形式化验证与程序合成领域的严谨性，通过整合多个权威开源项目形成统一评估框架。该数据集从DafnyBench、NumPy文档衍生规范、Verina、APPS等12个来源系统收集了12,504项任务，并采用多语言并行标注策略，为每个任务同步生成Dafny、Lean和Verus三种形式化验证语言的规范文件。在数据清洗阶段，团队保留了包含编译错误或占位符的样本，为规范修复研究提供宝贵资源，最终通过质量分析流程形成包含55,397次实验结果的完整元数据体系。

使用方法

研究者可通过解析vericoding_benchmark_v1.csv文件获取任务索引与元数据，进而根据Vericoding ID在specs文件夹中定位多语言规范文件。对于机器学习实验，推荐使用jsonl文件夹中经预处理的JSON线条目，其标准化结构便于模型输入流水线的构建。vericoded和handcoded文件夹分别提供机器生成与人工编写的参考实现，用户可通过对比vericoding_results_v1.csv中的实验记录，系统评估不同方法在形式化验证任务上的表现。

背景与挑战

背景概述

程序验证领域长期面临着形式化验证与程序生成相结合的挑战，Vericoding Benchmark作为2024年发布的新型基准数据集，由Beneficial AI Foundation等研究机构联合构建。该数据集聚焦于形式化验证程序合成这一核心问题，整合了Dafny、Lean和Verus三种主流验证语言的12,504个任务，其数据来源涵盖DafnyBench、NumPy文档衍生规范、Verina验证库及APPS编程评估系统等多个权威基准。通过构建跨语言的形式化规范与实现代码的对应关系，该数据集为验证增强型程序生成研究提供了标准化评估框架，显著推动了形式化方法在智能编程领域的应用深度。

当前挑战

在领域问题层面，该数据集致力于解决形式化验证程序合成中规范一致性验证的经典难题，包括循环不变式推导、后置条件满足性证明等核心挑战。构建过程中面临多语言规范对齐的技术瓶颈，需处理Dafny到Python的语义转换偏差，以及Lean规范中因原始数据缺失导致的三个任务空白。同时，数据集收录了编译失败案例以支持规范修复研究，但跨验证工具链的兼容性维护与人工标注验证的工作量构成了额外挑战。

常用场景

经典使用场景

在形式化验证与程序合成领域，Vericoding Benchmark通过整合Dafny、Lean和Verus等多种验证语言的任务，为研究者提供了一个标准化的评估平台。该数据集最经典的使用场景在于系统性地测试和比较不同模型在生成可验证代码方面的能力，涵盖了从规范编写到代码实现的完整流程，尤其适用于评估AI驱动验证工具在复杂逻辑约束下的表现。

解决学术问题

该数据集有效解决了形式化方法研究中长期存在的基准测试碎片化问题，通过统一规范格式与评估标准，为程序正确性验证、规范修复及跨语言翻译等核心课题提供了可复现的实验基础。其意义在于首次将大规模真实世界编程任务与形式化验证要求相结合，推动了可信软件构造理论与自动化工具开发的协同发展。

实际应用

在实际工业场景中，该数据集为构建高可靠性软件系统提供了关键支撑，特别是在航空航天、金融交易等对代码正确性要求严苛的领域。通过将自然语言需求转化为形式化规范，工程师能够借助该基准测试验证自动生成代码的功能完备性，显著提升复杂系统开发的效率与安全保障水平。

数据集最近研究

最新研究方向

在形式化验证与程序合成领域，Vericoding Benchmark作为首个大规模集成多语言验证工具的基准数据集，正推动人工智能辅助代码生成的前沿探索。该数据集融合Dafny、Lean和Verus等验证语言，通过12,504个任务构建了程序正确性验证的标准化测试环境。当前研究聚焦于利用大语言模型实现可验证代码的自动合成，尤其在处理未编译代码的规范修复、跨语言形式化转换等挑战中展现价值。随着神经符号计算范式的兴起，该基准通过整合HumanEval、APPS等知名编程数据集，为构建可信AI编程系统提供了关键实验基础，其多模态任务结构亦为可解释性研究开辟了新路径。