Formally Verified Automated Programming Progress Standards (FVAPPS)

FVAPPS是一个包含4715个样本的数据集，用于编写程序并证明其正确性，是迄今为止最大的形式验证基准。该数据集由Beneficial AI Foundation和Independent共同开发，基于APPS数据集，包含自然语言问题、难度标记、Python中的正确解决方案以及一些输入输出测试对。数据集通过Anthropic的Claude Sonnet 3.53模型生成，旨在为定理证明和程序合成提供基准。FVAPPS is a dataset comprising 4,715 samples intended for program writing and correctness verification, and it stands as the largest formal verification benchmark to date. Co-developed by the Beneficial AI Foundation and Independent, this dataset is built upon the APPS dataset and includes natural language problems, difficulty tags, correct Python solutions, as well as select input-output test pairs. Generated using Anthropic's Claude Sonnet 3.53 model, the dataset is designed to provide a benchmark for theorem proving and program synthesis.

搜集汇总

数据集介绍

构建方式

FVAPPS数据集的构建基于APPS数据集，首先通过爬取CodeForces和LeetCode等面试准备平台，收集编程谜题及其解决方案。然后，利用Anthropic的Claude Sonnet 3.53模型将这些编程谜题和解决方案转换为Lean 4文件，每个文件包含一个解决方案函数签名和多个定理声明，并通过“sorry”关键字标记为未来证明。最后，通过一系列的质量保证步骤，包括单元测试、属性测试和Plausible框架的评估，筛选出高质量的数据集样本。

特点

FVAPPS数据集具有以下特点：1）规模庞大，包含4715个样本，是最大的形式化验证基准；2）涵盖了1083个经过质量控制的样本，提供了高保证的数据集；3）使用Lean 4作为形式化验证的语言，具有表达任意程序的能力；4）包含不同保证级别的样本，包括未保护、保护和保护且可信的样本，满足不同研究需求。

使用方法

FVAPPS数据集的使用方法如下：1）下载数据集，可以从HuggingFace平台获取；2）根据研究需求选择不同保证级别的样本；3）利用数据集中的函数定义和定理声明进行形式化验证实验；4）评估模型的定理证明能力，并与人类基准进行比较；5）探索形式化验证的自动化解决方案结构，并推动形式化验证的扩展。

背景与挑战

背景概述

在大规模语言模型（LLMs）在软件工程领域的应用中，代码生成能力的迅速发展引发了关于代码安全性和正确性的强烈关注。为了确保生成的代码在运行前得到验证，FVAPPS（Formally Verified Automated Programming Progress Standards）数据集应运而生。该数据集由Quinn Dougherty和Ronak Mehta在Beneficial AI Foundation的赞助下创建，旨在为编写程序和证明其正确性提供一个基准，这是目前最大的形式化验证基准，包括1083个经过精心挑选和严格质量控制的样本。FVAPPS基于APPS数据集，该数据集是一个用于编程谜题解决的基准和数据集，旨在通过单元测试检查Python编写的解决方案。FVAPPS通过将单元测试推广到Lean 4定理（即使用Lean的“sorry”关键字）来扩展这一概念。FVAPPS的发布对于推动机器学习和程序合成社区解决通用编程问题及其相关正确性规范具有重要意义。

当前挑战

FVAPPS数据集面临的主要挑战包括：1)领域问题的挑战：随着LLMs在代码生成领域的应用，确保生成的代码能够通过形式化验证，从而在医疗设备管理、患者记录管理、个人信息安全、自动驾驶车辆控制、网络安全防御系统和军事应用等领域提供安全性和正确性的保证；2)构建过程中的挑战：在构建FVAPPS数据集的过程中，研究人员遇到了将编程谜题转化为形式化验证问题的挑战，以及如何确保生成的定理在数学上是正确的，并能够通过形式化验证。此外，研究人员还面临着如何提高LLMs在形式化验证方面的能力，使其能够自主生成可验证的代码，从而减少对人工评估的依赖。

常用场景

经典使用场景

FVAPPS 数据集，作为正式验证自动编程进度标准，主要用于编写程序并证明其正确性。它是目前最大的正式验证基准，包括 1083 个经过策划和质量控制的样本。FVAPPS 的经典使用场景是作为编程面试问题的基准，用于评估软件工程师在解决实际问题时的技能。此外，FVAPPS 还可用于评估机器学习模型在代码生成和证明方面的能力。

解决学术问题

FVAPPS 数据集解决了在软件工程中保证代码安全性和正确性的问题。随着大型语言模型在代码生成能力方面的快速发展，人们越来越担心这些模型生成的代码的安全性。FVAPPS 通过提供大量经过策划和质量控制的样本，使研究人员能够评估机器学习模型在代码生成和证明方面的能力，从而为提高代码安全性提供了新的思路。

衍生相关工作

FVAPPS 数据集的衍生相关工作包括 Lean 4 程序证明、编程合成和机器学习。Lean 4 是一种形式化验证工具，可用于证明程序的正确性。编程合成是一种自动生成代码的技术，而机器学习可用于提高代码生成的效率和准确性。FVAPPS 数据集为这些领域的研究提供了新的思路和数据支持。