CoqStoq

CoqStoq是由加州大学圣地亚哥分校等机构创建的一个用于Coq定理证明的大型数据集，包含2,226个开源Coq项目中的196,929个定理和2,225,515个证明步骤。数据集从GitHub上通过CoqPyt Python客户端挖掘而来，分为训练数据和评估基准。CoqStoq的创建旨在支持自动化软件验证中的定理证明，特别是通过检索增强生成（RAG）技术来提高证明效率。该数据集的应用领域主要集中在形式化验证和软件可靠性方面，旨在解决自动化证明生成中的效率和准确性问题。

CoqStoq is a large-scale dataset for Coq theorem proving, created by the University of California, San Diego and other institutions. It contains 196,929 theorems and 2,225,515 proof steps across 2,226 open-source Coq projects. The dataset was mined from GitHub via the CoqPyt Python client, and is split into training data and evaluation benchmarks. CoqStoq was developed to support theorem proving in automated software verification, with the specific goal of enhancing proof efficiency through retrieval-augmented generation (RAG) techniques. This dataset is primarily applied in the fields of formal verification and software reliability, aiming to address the efficiency and accuracy issues in automated proof generation.

原始信息汇总

CoqStoq 数据集

概述

CoqStoq 是一个用于评估 Coq 定理证明合成工具的基准数据集。该数据集包含了用于测试证明合成工具的定理和相关环境。

数据集结构

• data_points: 包含 DatasetFile 对象，用于指示在合成证明时可用的前提和证明。每个 .v 文件在 repos 文件夹中都有一个对应的文件。
• repos: 包含所有包含定理的仓库，Rango 将在这些定理上进行评估。

数据集创建示例

假设要创建一个名为 "coqstoq-test" 的数据集，包含 CoqStoq 测试集中的定理，步骤如下：

1. 创建目录：mkdir coqstoq-test

2. 创建符号链接：ln -s CoqStoq/test-repos coqstoq-test/repos

3. 运行脚本生成数据点：

   rm -rf ~/.cache/coqpyt_cache python3 scripts/create_coqstoq_data_points CoqStoq test coqstoq-test/data_points coqstoq-test/coqstoq-test-sentences.db

   • "CoqStoq" 是 CoqStoq 仓库的路径。
   • "test" 是要创建数据的 CoqStoq 分割。
   • "coqstoq-test/data_points" 是保存数据点的位置。
   • "coqstoq-test-sentences.db" 是保存 sentencedb 的位置（包含文件之间的共享前提）。

数据集评估

可以使用以下脚本在数据集上运行 Rango 进行评估：

python3 src/evaluation/eval.py --conf_loc=example_confs/eval/coqstoq-test.yaml --slurm_conf=example_confs/slurm/gpu8.yaml

python3 src/evaluation/eval.py --conf_loc=example_confs/eval/coqstoq-test.yaml --n_workers=1

• 前者需要访问 slurm 集群。
• 后者将在一个工作线程上运行评估。

数据集处理与训练

数据处理

确保在项目的 raw-data/coq-dataset/data_points 子目录中有 CoqStoq 的 data_points 文件。然后，可以通过运行以下命令预处理数据集： bash slurm/example-jobs/create_dataset.sh

数据集整合

在训练模型之前，必须将处理后的数据整合到 sqlite 数据库中。可以使用以下命令整合数据集： python3 src/data_management/consolidate.py <split location> <dataset location> <new dataset location>

模型训练

可以通过运行以下命令训练模型： sbatch slurm/example-jobs/train_decoder.sh

搜集汇总

数据集介绍

构建方式

CoqStoq数据集通过从GitHub上挖掘2,226个开源的Coq项目构建而成，涵盖了196,929个定理及其对应的证明步骤。该数据集的构建过程包括自动编译每个项目，并使用CoqPyt工具验证每个Coq文件的有效性。只有成功编译且无错误的文件才会被纳入数据集。CoqStoq数据集被划分为训练集、验证集和评估基准，其中评估基准包含了CoqGym基准中的所有项目以及CompCert和四个长期维护的Coq社区项目。

使用方法

CoqStoq数据集主要用于训练和评估自动化证明合成工具，如Rango。研究人员可以使用该数据集来训练大型语言模型（LLM），并通过检索增强生成（RAG）技术来提高证明合成的效率。数据集的训练集用于微调模型，验证集用于调整模型超参数，而评估基准则用于比较不同工具的性能。通过使用CoqStoq，研究人员可以评估工具在不同项目中的泛化能力，并探索检索增强证明合成的效果。

背景与挑战

背景概述

CoqStoq数据集由加州大学圣地亚哥分校、里斯本大学和帝国理工学院的研究团队于2023年创建，旨在支持自动化软件验证中的定理证明任务。该数据集包含了从GitHub上挖掘的2,226个开源Coq项目中的196,929个定理及其证明步骤，总计2,225,515个证明步骤。CoqStoq的创建是为了支持Rango工具的训练和评估，Rango是一种基于大语言模型（LLM）的自动化证明合成工具，旨在通过检索增强技术来提高定理证明的效率。该数据集的发布不仅为自动化定理证明领域提供了丰富的训练和评估资源，还为研究者提供了一个基准，用于比较不同工具在定理证明任务中的表现。

当前挑战

CoqStoq数据集的构建面临多个挑战。首先，从GitHub上挖掘和验证大量的Coq项目是一个复杂的过程，需要确保数据的质量和一致性。其次，自动化定理证明任务本身具有高度复杂性，尤其是在处理大型项目和复杂的证明步骤时，如何有效地检索相关的前提和证明是一个关键挑战。此外，如何在大语言模型的上下文中动态调整检索策略，以适应不断变化的证明状态，也是一个重要的研究问题。最后，评估自动化证明工具的性能时，如何避免数据集与预训练模型的数据污染，确保评估的公正性和有效性，也是一个需要解决的难题。

常用场景

经典使用场景

CoqStoq数据集的经典使用场景主要集中在自动化软件验证领域，特别是在使用Coq证明助手进行形式化验证时。该数据集被用于训练和评估自动化证明合成工具，如Rango，以提高其在识别相关前提（如引理和定义）以及从当前项目中检索相似证明的能力。通过在每个证明步骤中进行检索增强，Rango能够适应项目和证明状态的变化，从而提高证明合成的效率和准确性。

解决学术问题

CoqStoq数据集解决了自动化证明合成中的关键学术问题，特别是在如何有效利用本地信息（如项目中的引理和证明）来增强证明生成过程。传统的证明合成工具往往依赖于全局信息或手动选择的前提，而CoqStoq通过提供大规模的Coq项目数据，使得工具能够在每个证明步骤中动态检索相关证明和引理，从而显著提高了证明的成功率。这一方法不仅减少了手动干预的需求，还提升了自动化证明的可靠性和效率。

实际应用

在实际应用中，CoqStoq数据集为自动化软件验证工具的开发提供了宝贵的资源。通过该数据集，开发者可以训练和优化自动化证明工具，使其能够在复杂的软件项目中自动生成证明，从而提高软件的可靠性和质量。例如，在编译器验证领域，CoqStoq已被用于验证CompCert编译器的正确性，展示了其在实际软件验证中的巨大潜力。此外，该数据集还可用于其他形式化验证任务，如安全协议验证和硬件设计验证。

数据集最近研究

最新研究方向

在自动化软件验证领域，CoqStoq数据集的最新研究方向主要集中在利用大规模语言模型（LLMs）和检索增强生成（RAG）技术来提升定理证明的自动化水平。研究者们通过开发Rango工具，展示了在每个证明步骤中动态检索相关前提和相似证明的重要性，从而显著提高了证明生成的效率和准确性。Rango不仅能够自动识别相关前提，还能从当前项目中检索相似的证明，以适应证明状态的变化。这一研究方向不仅推动了形式化验证技术的自动化进程，还为软件可靠性的提升提供了新的技术支持。

相关研究论文

• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

  加州大学圣地亚哥分校 · 2024年