ReForm-Python2Dafny-Dataset

该数据集包含与使用强化学习在大型语言模型中进行形式软件验证的论文相关的数据集。主要包括两个数据集：Python2Dafny和DafnyComp。Python2Dafny数据集包含将Python程序映射到Dafny代码的18000个样本，主要用于监督微调阶段。DafnyComp数据集是一个包含300个具有自动形式化规范的组合形式程序的基准，用于规范推理和评估泛化能力。这两个数据集都提供了JSON格式。

This dataset contains resources associated with the paper on formal software verification using reinforcement learning with large language models. It primarily includes two datasets: Python2Dafny and DafnyComp. The Python2Dafny dataset contains 18,000 samples that map Python programs to Dafny code, and is mainly used for the supervised fine-tuning stage. The DafnyComp dataset is a benchmark comprising 300 compositional formal programs with automated formal specifications, which is employed for specification reasoning and generalization capability evaluation. Both datasets are provided in JSON format.

原始信息汇总

Re:Form Datasets 数据集概述

数据集基本信息

• 任务类别: 文本生成
• 标签: 代码生成、形式化验证、Dafny、强化学习

数据集来源

• 关联论文: "Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny"
• 项目主页: https://veri-code.github.io/ReForm-page
• 代码仓库: https://github.com/Veri-Code/Veri-Code

数据集内容

包含两个主要数据集:

1. Python2Dafny

   • 规模: 18,000个样本
   • 用途: 用于监督微调(SFT)阶段
   • 内容: Python程序到Dafny代码的映射

2. DafnyComp

   • 规模: 300个组合式形式化程序
   • 特点: 包含自动形式化的规范
   • 用途: 规范推理和评估泛化能力

数据格式

• 所有数据集均以JSON格式提供

使用说明

• 预处理脚本: python -m src.data_preprocess
• 详细使用指南请参考代码仓库文档

引用信息

bibtex @misc{yan2025reformreducinghuman, title={Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny}, author={Chuanhao Yan and Fengdi Che and Xuhan Huang and Xu Xu and Xin Li and Yizhi Li and Xingwei Qu and Jingzhe Shi and Zhuangzhuang He and Chenghua Lin and Yaodong Yang and Binhang Yuan and Hang Zhao and Yu Qiao and Bowen Zhou and Jie Fu}, year={2025}, eprint={2507.16331}, archivePrefix={arXiv}, primaryClass={cs.CL}, url={https://arxiv.org/abs/2507.16331}, }

搜集汇总

数据集介绍

构建方式

在形式化软件验证领域，ReForm-Python2Dafny-Dataset的构建体现了跨语言代码转换的前沿探索。该数据集通过系统化采集18,000个Python程序样本，并人工标注其对应的Dafny形式化验证代码，构建了高质量的监督微调训练集。数据采集过程严格遵循形式化验证的规范要求，确保每个样本都能准确反映Python到Dafny的语义映射关系，为基于强化学习的大语言模型训练提供了可靠的基础数据支撑。

特点

作为形式化验证领域的重要资源，该数据集最显著的特点是实现了命令式编程语言与形式化验证语言之间的桥梁作用。数据集不仅覆盖了Python的各类语法结构，还精心设计了对应的Dafny契约规范和循环不变式，使得模型能够学习到严格的数学验证逻辑。特别值得注意的是，数据集采用了JSON格式存储，既保留了完整的代码结构信息，又便于机器学习管道的预处理和转换。

使用方法

该数据集的使用需要结合特定的形式化验证工作流程。研究人员可通过提供的预处理脚本将JSON数据转换为适合模型训练的parquet格式，继而应用于监督微调阶段。典型的使用场景包括：训练大语言模型理解Python与Dafny的语义对应关系，开发自动形式化验证工具，以及评估模型在代码转换任务中的泛化能力。使用时应严格遵循配套代码库中的训练流程说明，确保模型能够充分学习数据集蕴含的形式化验证知识。

背景与挑战

背景概述

ReForm-Python2Dafny-Dataset是由Veri-Code团队于2025年推出的创新型数据集，旨在推动形式化软件验证领域的自动化进程。该数据集源于论文《Re:Form——在LLMs中通过强化学习降低形式化软件验证中人类先验的初步研究》，核心研究聚焦于利用大型语言模型中的强化学习技术，减少对人工标注先验知识的依赖。作为首个专注于Python与Dafny代码转换的大规模数据集，其18,000个样本为程序自动形式化验证提供了重要基准，显著提升了代码生成与数学可验证推理的结合能力。

当前挑战

该数据集面临双重技术挑战：在领域问题层面，如何准确实现非形式化语言（Python）向形式化验证语言（Dafny）的语义转换，需解决程序行为等价性证明与规格说明自动生成等关键问题；在构建过程中，需克服训练样本的语法-逻辑对齐难题，确保生成的Dafny代码既符合形式化语法规范，又能通过验证器证明。此外，300个组合式形式化程序的基准测试集设计，要求对程序语义的组合性进行精确建模，这对数据标注的严谨性与评估指标的完备性提出了极高要求。

常用场景

经典使用场景

在形式化软件验证领域，ReForm-Python2Dafny-Dataset为研究者提供了从Python程序到Dafny代码的映射样本，极大促进了自动代码转换技术的发展。该数据集特别适用于监督微调阶段，通过18,000个高质量样本，帮助模型学习如何在形式化语言空间中精确表达程序语义。

衍生相关工作

基于该数据集衍生的研究推动了形式化方法与其他前沿技术的交叉融合。相关经典工作包括将强化学习引入程序合成领域、开发混合形式化验证框架等，这些成果发表在PLDI、CAV等顶级会议，形成了软件工程与形式化方法研究的新方向。

数据集最近研究

最新研究方向

在形式化软件验证领域，ReForm-Python2Dafny-Dataset的出现标志着大语言模型与强化学习技术的深度融合。该数据集通过18,000个Python到Dafny的代码转换样本，为降低形式化验证对人类先验知识的依赖提供了重要支撑。当前研究聚焦于如何利用强化学习优化大语言模型在Dafny等形式化语言空间的推理能力，特别是在自动生成数学可证明的验证逻辑方面展现出突破性潜力。随着可信软件需求的激增，这类能够桥接传统编程语言与形式化验证工具的数据集，正在推动智能代码生成与形式化方法交叉领域的发展。