AutoRocq-bench

AutoRocq-bench是一个从真实C代码中提取的Rocq/Coq证明义务的语料库，旨在评估交互式或自动定理证明工作流程。

AutoRocq-bench is a corpus of Rocq/Coq proof obligations extracted from real-world C code, designed to evaluate interactive or automated theorem proving workflows. This benchmark targets Rocq (formerly known as Coq) 8.18.0, and includes obligations sourced from SV-COMP programs and Linux kernel modules.

原始信息汇总

AutoRocq-bench 数据集概述

数据集简介

AutoRocq-bench 是一个从真实 C 代码中提取的 Rocq/Coq 证明义务语料库，旨在用于评估交互式或自动化定理证明工作流。

技术规格

• 目标证明系统： Rocq (原名 Coq) 8.18.0。
• 数据来源： 证明义务衍生自以下两类程序：
  1. SV-COMP 程序 (svcomp)。
  2. Linux 内核模块 (verker)。
• 基准条目构成： 每个条目包含：
  1. 一个包含单个未证明定理 wp_goal 的 .v 文件。
  2. report.json 中的一个关联条目，指向其在 source_programs/ 中的源代码起源。

仓库内容结构

• benchmarks/
  • svcomp/： 基准目录。
  • verker/： 基准目录。
  • svcomp-ablation.txt： 来自 svcomp/ 的 70 个采样目标列表。
  • svcomp-ablation.txt： 来自 svcomp/ 的 571 个剩余目标列表。
  • verker-assert.txt： 来自 verker/ 的 60 个断言目标列表。
• source_programs/
  • svcomp/： benchmarks/svcomp 的原始 C 源文件。
  • verker/： benchmarks/verker 的原始 C 头文件/源文件。
• libautorocq/
  • 用于编译 Coq 基准文件的库。

引用信息

若在学术研究中使用本工作，请引用以下论文：

@article{autorocq, title={Agentic Verification of Software Systems}, author={Tu, Haoxin and Zhao, Huan and Song, Yahui and Zafar, Mehtab and Meng, Ruijie and Roychoudhury, Abhik}, journal={Proceedings of the ACM on Software Engineering}, volume={1}, number={FSE}, year={2026}, publisher={ACM New York, NY, USA} }

搜集汇总

数据集介绍

构建方式

在形式化验证领域，AutoRocq-bench 数据集的构建体现了从实际软件系统中提取证明义务的严谨方法。该数据集通过从真实的 C 语言源代码中系统性地提取 Rocq（原 Coq）证明义务而构建，具体来源包括 SV-COMP 竞赛的标准程序集和 Linux 内核模块。每个基准条目由一个包含单个待证明定理 `wp_goal` 的 `.v` 文件，以及一个在 `report.json` 中记录其对应原始源代码位置的条目组成，确保了证明义务与源程序之间的可追溯性。

特点

AutoRocq-bench 的核心特点在于其专注于评估交互式或自动化定理证明工作流，并紧密贴合实际软件验证场景。数据集针对 Rocq 8.18.0 版本设计，包含从 SV-COMP 程序和 Linux 内核模块衍生出的多样化证明义务，涵盖了不同复杂度和领域的验证问题。此外，数据集提供了明确的分类列表，如对 `svcomp` 部分进行采样的消融列表和 `verker` 中的断言目标列表，便于研究者进行有针对性的实验和分析。

使用方法

使用 AutoRocq-bench 时，研究者可将其作为基准平台，评估定理证明器或验证工具在自动化证明生成方面的性能。典型工作流程包括：利用 `benchmarks/` 目录下的 `.v` 文件作为输入，运行定理证明器尝试证明其中的 `wp_goal` 定理；通过 `report.json` 追溯证明义务的源代码起源，以进行深入分析；同时，可借助提供的分类列表（如 `svcomp-ablation.txt`）进行子集测试或消融研究。数据集附带的 `libautorocq` 库支持 Coq 基准文件的编译，为实验提供了技术便利。

背景与挑战

背景概述

在形式化验证领域，确保软件系统尤其是底层C代码的正确性一直是一项核心研究课题。AutoRocq-bench数据集于2026年由Haoxin Tu、Huan Zhao、Yahui Song、Mehtab Zafar、Ruijie Meng及Abhik Roychoudhury等研究人员共同创建，旨在为交互式或自动化定理证明工作流提供评估基准。该数据集从真实的C代码中提取Rocq/Coq证明义务，其来源包括SV-COMP程序与Linux内核模块，直接针对形式化验证工具在复杂软件验证任务中的性能评估。这一数据集的构建推动了形式化方法在工业级代码验证中的应用，为定理证明与程序验证社区提供了重要的实验基础。

当前挑战

AutoRocq-bench所针对的领域挑战在于如何高效验证大规模、真实世界的C代码，尤其是操作系统内核等关键系统的正确性，这要求定理证明工具能够处理复杂的语义和状态空间。在数据集构建过程中，研究人员面临从异构C源代码中准确提取并形式化证明义务的难题，包括处理指针操作、并发行为及底层硬件依赖等特性，同时需确保生成的Coq文件与原始代码语义一致，且基准覆盖具有代表性和多样性。

常用场景

经典使用场景

在形式化验证与程序分析领域，AutoRocq-bench数据集为评估交互式或自动化定理证明工作流提供了标准化的测试平台。该数据集从真实的C代码中提取Rocq/Coq证明义务，覆盖了SV-COMP程序与Linux内核模块两大关键来源，使得研究人员能够系统地检验定理证明器在复杂软件验证任务中的性能与可靠性。通过提供结构化的.v文件与详尽的元数据报告，该数据集促进了证明自动化技术的比较与优化，成为形式化方法社区中不可或缺的基准工具。

解决学术问题

AutoRocq-bench数据集有效应对了形式化验证中证明义务生成与管理的核心挑战。它通过从实际C代码中派生证明目标，解决了传统验证基准往往脱离真实软件环境的问题，为研究自动化定理证明算法的可扩展性与精确性提供了实证基础。该数据集支持对交互式证明策略的评估，有助于揭示在大型代码库中验证条件的形式化转换规律，从而推动程序正确性验证理论向更实用、更高效的方向发展。

衍生相关工作

围绕AutoRocq-bench数据集，学术界衍生出一系列经典研究工作，主要集中在自动化证明生成与验证策略优化方面。例如，基于该数据集的实验推动了定理证明器中机器学习增强技术的探索，如利用神经网络预测证明步骤或生成辅助引理。同时，它也催生了针对大型代码库的增量验证方法，以及形式化验证工具与静态分析框架的集成方案，这些工作显著丰富了程序验证领域的方法论体系。