VeriSoftBench

VeriSoftBench是由德克萨斯大学奥斯汀分校和纽约大学联合创建的Lean 4形式化验证基准数据集，包含500条从23个开源形式化方法仓库中提取的证明任务。该数据集独特地保留了原始项目的多模块结构和跨文件依赖关系，数据来源涵盖编译器验证、编程语言语义等领域。其构建过程通过严格筛选非平凡证明任务，并平衡难度指标与仓库类别分布。该数据集旨在评估大语言模型和专用证明器在软件验证场景下的性能，解决传统数学证明基准与真实项目验证任务间的泛化鸿沟问题。

VeriSoftBench is a Lean 4 formal verification benchmark dataset co-developed by The University of Texas at Austin and New York University. It comprises 500 proof tasks extracted from 23 open-source formal methods repositories. Uniquely, this dataset preserves the multi-module structure and cross-file dependencies of the original projects, with data sources covering domains such as compiler verification and programming language semantics. During its construction, non-trivial proof tasks are strictly screened, and a balance is maintained between difficulty metrics and the category distribution of the source repositories. This dataset aims to evaluate the performance of large language models (LLMs) and specialized theorem provers in software verification scenarios, addressing the generalization gap between traditional mathematical proof benchmarks and real-world software verification tasks.

搜集汇总

数据集介绍

构建方式

在形式化验证领域，现有基准多集中于数学定理证明，而软件验证任务通常嵌入于富含项目特定定义与跨文件依赖的大型代码库中。VeriSoftBench的构建旨在填补这一空白，其从23个开源形式化方法仓库中精心筛选出500个Lean 4证明义务。构建过程首先确保每个任务均具备有效且无漏洞的原始证明，并排除可被标准自动化直接解决的平凡目标。随后，依据证明复杂度与上下文依赖度两个维度进行评分，通过分层抽样平衡不同仓库类别与难度分布，最终形成既保留原始仓库环境与依赖结构，又涵盖编译器正确性、编程语言语义及验证框架等多主题的基准集合。

特点

VeriSoftBench的突出特点在于其高度贴近真实软件验证场景的仓库尺度上下文。与依赖共享数学库的传统基准不同，该数据集中的证明义务深度嵌入项目特定的抽象定义与模块化结构中，形成密集的跨文件依赖图。其任务不仅直接引用大量本地定义，且依赖链的传递闭包常涉及多层嵌套，导致证明需在长链抽象层中进行推理。此外，数据集提供了两种上下文配置：精选上下文仅包含与证明相关的依赖，而完整上下文则暴露整个仓库环境，从而能够系统评估模型在噪声环境下的检索与推理能力。这种设计使得VeriSoftBench能够有效衡量证明自动化工具在面临复杂、项目专属逻辑环境时的泛化性能。

使用方法

为系统评估证明自动化系统的性能，VeriSoftBench设定了标准化的使用流程。评估时，模型接收包含目标定理、本地文件上下文及相应依赖信息的任务输入，并遵循生成-检查-修复的循环机制：首先生成多个候选证明脚本，随后利用Lean 4编译器在预构建的环境中验证其正确性，并对失败脚本依据编译错误信息进行多轮修复。数据集支持两种上下文模式，在精选上下文模式下，模型仅获得与证明直接相关的依赖声明；而在完整仓库上下文模式下，模型需面对整个仓库的庞大定义与引理集合，这对上下文的筛选与利用提出了更高要求。通过比较不同配置下的成功率，研究者能够深入分析模型在处理仓库尺度依赖与项目特定抽象时的核心挑战。

背景与挑战

背景概述

随着大型语言模型在交互式定理证明领域取得突破性进展，特别是在Lean证明助手中的应用，对高质量基准数据集的需求日益凸显。VeriSoftBench由德克萨斯大学奥斯汀分校和纽约大学的研究团队于2026年2月提出，旨在填补现有数学导向基准与软件验证实际需求之间的鸿沟。该数据集的核心研究问题是评估自动化证明器在真实软件验证场景下的泛化能力，即当证明任务深度依赖于特定项目的自定义抽象和跨文件依赖时，现有模型能否有效应对。其影响力在于首次将评估场景从共享的Mathlib数学生态扩展到包含23个独立开源形式化方法项目的代码库环境，为衡量证明自动化在复杂软件验证任务中的进展提供了关键工具。

当前挑战

VeriSoftBench所针对的领域挑战在于软件形式化验证中的定理证明自动化，这要求模型能够理解并操作项目特定的数据类型、操作语义和不变式，而非依赖标准数学库中的固定抽象。构建过程中的主要挑战体现在两个方面：一是数据收集与处理的复杂性，需要从异构的Lean代码库中提取500个证明义务，同时完整保留其原始的项目上下文、跨文件依赖和多模块结构，确保每个任务都能在独立的环境中编译验证；二是评估框架的设计难度，需创建“精选上下文”和“完整代码库上下文”两种配置，以分离模型检索能力与推理能力的影响，并处理部分代码库上下文长度远超当前模型窗口限制的技术难题，这要求精心的工程实现以维持评估的严谨性与可复现性。

常用场景

经典使用场景

在形式化验证领域，VeriSoftBench数据集被设计用于评估大型语言模型在交互式定理证明中的性能，特别是在软件验证和编程语言元理论的实际场景中。该数据集从开源形式化方法项目中提取了500个Lean 4证明义务，每个任务都保留了原始代码库的上下文和跨文件依赖关系，模拟了真实开发环境中证明自动化面临的挑战。通过这种设计，VeriSoftBench能够测试证明器在项目特定库和复杂依赖结构下的泛化能力，为形式化验证的自动化研究提供了贴近实际的评估基准。

实际应用

VeriSoftBench在实际应用中为形式化验证工具的开发提供了关键测试平台。它被用于评估前沿大型语言模型如GPT-5.2、Claude Opus 4.5和Gemini-3-Pro在软件验证任务中的表现，同时测试了专用证明器如Goedel-Prover-v2和Aristotle在代码库规模环境下的适应性。通过对比精选上下文和完整代码库上下文两种配置，该数据集帮助研究者理解上下文检索对证明成功的影响，并为优化证明自动化系统的上下文选择机制提供了实证依据，从而提升形式化验证在编译器正确性、零知识电路验证等实际项目中的效率。

衍生相关工作

VeriSoftBench的推出促进了形式化验证领域一系列相关研究的发展。它启发了对现有证明自动化系统的重新评估，例如揭示了在数学证明基准上表现优异的专用证明器在代码库规模任务中的局限性。该数据集为后续工作如上下文检索算法、多模块依赖分析以及针对项目特定抽象的证明生成方法提供了基准。同时，它推动了形式化验证基准从数学领域向软件验证领域的范式转移，影响了如LeanDojo、Verina等数据集的设计理念，并为开发能够处理长依赖链和密集本地概念的神经证明自动化系统奠定了基础。