VeriSoftBench

VeriSoftBench包含500个定理证明任务，这些任务来自23个真实的Lean 4仓库，涵盖了编译器验证、类型系统形式化、应用验证（零知识证明、智能合约）、语义框架等多个领域。

VeriSoftBench contains 500 theorem proving tasks, which are sourced from 23 real-world Lean 4 repositories, covering multiple domains including compiler verification, formalization of type systems, application verification (zero-knowledge proofs, smart contracts), semantic frameworks, and more.

原始信息汇总

VeriSoftBench 数据集概述

数据集基本信息

• 数据集名称：VeriSoftBench
• 核心用途：一个用于在 Lean 4 软件验证任务上评估神经定理证明器的基准。
• 任务规模：包含 500 个定理证明任务。
• 任务来源：任务提取自 23 个真实世界的 Lean 4 代码仓库。
• 应用领域：涵盖编译器验证、类型系统形式化、应用验证（零知识证明、智能合约）、语义框架等。

数据内容与结构

• 数据文件：数据集位于 data/verisoftbench.jsonl 文件中。
• 任务内容：每个任务包含定理名称、陈述、源代码位置、过滤后的依赖项（库定义、仓库定义、本地上下文、引理）、真实证明以及元数据（类别、难度指标、Aristotle 子集成员资格）。
• 元数据：任务附带类别、难度指标等信息，支持按类别进行筛选。

获取与使用

• 获取地址：数据集可通过 Huggingface 获取：https://huggingface.co/datasets/maxRyeery/VeriSoftBench
• 依赖环境：验证证明需要针对实际的 Lean 代码仓库进行，可通过 Docker（推荐）或本地构建环境完成。
• 评估配置：提供多种配置文件（如 configs/openai_example.yaml）和命令行选项，支持指定模型提供商（OpenAI、Anthropic、Google）、上下文模式、任务筛选等。
• 上下文模式：
  • filtered_context（默认）：每个任务仅获取通过静态分析识别为相关的定义和引理。
  • full_context：每个任务获取其仓库中的所有定义和引理。
  • full_context_limited：为 ArkLib 和 lean-mlir 这两个最大的仓库预生成完整上下文提示，通过限制上下文大小来避免令牌限制。

评估与结果

• 评估脚本：主评估入口点为 evaluate.py。
• 结果输出：结果保存至 results/data/<run_name>/ 目录，包含整体统计的 summary.json 文件和每个定理的详细结果。
• 结果缓存：每个模型的评估结果会缓存在 results/cache/ 中，后续运行默认跳过已评估任务。
• 性能指标：结果摘要包含证明总数、修复前/后证明成功的定理数量及相应的成功率。

相关资源

• 论文：https://arxiv.org/abs/2602.18307
• 代码仓库结构：包含评估管道核心代码、提示模板、分析工具、构建脚本、配置文件、数据文件及 Docker 构建文件。
• 许可证：评估代码基于 MIT 许可证发布。基准测试中涉及的代码仓库按其原始许可证重新分发。

引用

如需引用，请使用提供的 BibTeX 条目。

搜集汇总

数据集介绍

构建方式

在形式化验证领域，构建高质量的定理证明基准需要兼顾真实性与多样性。VeriSoftBench从23个实际Lean 4代码库中系统性地抽取了500个定理证明任务，涵盖编译器验证、类型系统形式化、零知识证明等关键软件验证场景。其构建过程采用静态分析技术精确识别每个定理的相关定义与引理，确保依赖关系的准确性。所有任务均基于真实开源项目的特定提交版本，通过严谨的代码库构建流程还原原始验证环境，为评估神经定理证明器提供了坚实的现实基础。

使用方法

使用该数据集进行模型评估需要搭建完整的Lean验证环境。用户可通过Docker容器或本地构建两种方式配置依赖环境，其中Docker方案提供了预编译的代码库环境。评估流程通过配置文件或命令行参数灵活控制，支持按任务ID范围、类别或随机子集进行选择性测试。系统采用并行评估架构，最大支持8个工作线程同时运行，并内置证明修复机制进行多轮尝试。评估结果以结构化JSON格式输出，包含总体统计指标与详细定理证明记录，所有结果均采用缓存机制避免重复计算。

背景与挑战

背景概述

在形式化验证与人工智能交叉领域，自动化定理证明技术正逐步从理论探索迈向实际应用。VeriSoftBench数据集于2026年由Yutong Xin、Qiaochu Chen、Greg Durrett与Işil Dillig等研究人员共同创建，旨在为评估神经网络定理证明器在软件验证任务中的性能提供标准化基准。该数据集从23个真实的Lean 4代码库中精心选取500个定理证明任务，覆盖编译器验证、类型系统形式化、零知识证明与智能合约应用验证等多个关键研究方向。通过构建这一大规模、多样化的基准，研究团队试图推动形式化方法在工业级软件验证中的实际部署，并为神经网络与符号推理的融合提供实证基础。

当前挑战

VeriSoftBench所针对的核心挑战在于如何将神经网络模型有效应用于复杂软件系统的形式化验证过程。传统定理证明器依赖人工设计的启发式规则，难以适应大规模代码库中不断演化的逻辑结构。该数据集的构建需克服多重困难：首先，从异构的Lean 4项目中提取具有代表性的定理任务，必须平衡理论深度与实践相关性；其次，确保每个证明任务的可复现性要求精确捕获依赖关系与编译环境，这导致Docker镜像体积达110GB且构建耗时约一小时；最后，设计评估框架时需解决大语言模型的上下文长度限制与Lean证明环境的实时交互问题，从而在过滤上下文与完整上下文模式间取得权衡。

常用场景

经典使用场景

在形式化验证领域，VeriSoftBench作为评估神经定理证明器性能的基准，其经典使用场景聚焦于测试大型语言模型在软件验证任务中的定理证明能力。该数据集从23个真实Lean 4代码库中提取500个定理证明任务，涵盖编译器验证、类型系统形式化、零知识证明与智能合约等应用验证场景。研究者通过配置不同上下文模式（如过滤上下文或完整上下文）来评估模型在生成正确证明方面的准确率与效率，从而系统性地衡量模型在复杂逻辑推理中的表现。

解决学术问题

VeriSoftBench致力于解决形式化验证中神经定理证明器评估标准缺失的学术问题。传统上，软件验证任务的评估往往局限于小规模或合成数据集，难以反映真实代码库的复杂性与多样性。该数据集通过整合多领域实际项目中的定理，为研究者提供了统一且可复现的评估框架，从而促进对模型在语义理解、依赖关系推理及证明生成等核心能力上的量化分析。其意义在于推动了自动化定理证明与程序验证交叉领域的标准化进程，为后续研究奠定了实证基础。

实际应用

在实际应用层面，VeriSoftBench可直接服务于软件工程与安全关键系统的开发流程。例如，在编译器验证中，该数据集可用于测试模型能否自动证明优化转换的正确性；在智能合约形式化验证中，则能评估模型检测合约逻辑漏洞的能力。通过集成到持续集成管道，基于该数据集的评估工具可辅助开发者在代码提交前自动验证关键属性，从而提升软件可靠性并降低人工验证成本。这些应用体现了形式化方法向自动化、智能化方向演进的实际价值。

数据集最近研究

最新研究方向

在形式化验证领域，VeriSoftBench作为首个面向软件验证任务的神经定理证明器基准，正推动着自动推理与程序验证的交叉研究。其前沿探索聚焦于利用大型语言模型处理复杂、真实的Lean 4代码库，涵盖编译器验证、类型系统形式化及零知识证明等热点应用场景。该数据集通过静态分析提取相关定义与引理，构建了过滤上下文模式，旨在评估模型在有限信息下的推理能力，同时支持全上下文模式以测试模型处理大规模知识的能力。相关研究致力于提升模型在代码级定理证明中的泛化性与准确性，对促进智能辅助验证工具的发展、降低形式化验证门槛具有深远意义，为软件安全与可靠性的自动化保障提供了关键基准。