PVS-NASALib

PVS-NASALib数据集提取自美国国家航空航天局（NASA）的PVS库（NASALib），包含该形式化验证库中的声明。该数据集旨在支持与定理证明和形式化方法相关的研究与应用，例如证明项建模、自动形式化、检索以及依赖关系分析。数据集共包含37,110个条目，涵盖91个子库。每个条目代表一个PVS声明，其数据结构包含15个字段，核心字段包括：完整的声明内容（`fact`）、声明签名（`statement`）、证明/主体部分（`proof`）、声明类型（`type`，如引理、定义、定理等）、符号名称（`symbolic_name`）、所属子库（`library`）、源文件路径（`filename`）、文件级导入模块列表（`imports`）、引用的语料库内标识符列表（`deps`）、文档注释（`docstring`）、起止行号、是否包含证明的标志（`has_proof`）以及数据来源的仓库URL和提交哈希。在全部条目中，约30.6%（11,338条）包含证明部分，但均无文档注释。声明类型分布广泛，其中数量最多的是引理（lemma，19,984条）和定义（definition，10,061条），此外还包括定理、判断、函数、公理、推论等多种类型。数据来源于GitHub上的nasa/pvslib仓库的特定提交版本（59714e007f6acc7440fe014ae7ff83bfb2ef0696）。The PVS-NASALib dataset is extracted from NASAs PVS library (NASALib) and contains declarations from this formal verification library. The dataset aims to support research and applications related to theorem proving and formal methods, such as proof term modeling, automated formalization, retrieval, and dependency analysis. It consists of 37,110 entries covering 91 sublibraries. Each entry represents a PVS declaration with a data structure comprising 15 fields, including core fields like the full declaration content (`fact`), declaration signature (`statement`), proof/body part (`proof`), declaration type (`type`, e.g., lemma, definition, theorem), symbolic name (`symbolic_name`), sublibrary (`library`), source file path (`filename`), file-level import module list (`imports`), referenced corpus identifier list (`deps`), documentation comment (`docstring`), start and end line numbers, flag indicating whether it contains proof (`has_proof`), and repository URL and commit hash of the data source. Among all entries, approximately 30.6% (11,338 entries) contain proof parts but have no documentation comments. The declaration types are widely distributed, with the most numerous being lemmas (19,984 entries) and definitions (10,061 entries), along with other types such as theorems, judgments, functions, axioms, and corollaries. The data is sourced from a specific commit version (59714e007f6acc7440fe014ae7ff83bfb2ef0696) of the nasa/pvslib repository on GitHub.

原始信息汇总

数据集概述：PVS-NASALib

• 数据集名称：PVS-NASALib
• 描述：来自 NASA PVS 库（NASALib）的声明数据，用于定理证明、形式化方法和 PVS 相关研究。
• 许可证：other
• 语言：英语（en）
• 任务类型：文本生成、特征提取
• 数据集规模：10,000 < 样本数 < 100,000
• 样本总数：33,871 条记录（均为训练集）

数据集结构

• 配置：default
• 数据拆分：
  • train：33,871 个样本（数据文件路径：data/train-*）

数据特征（Schema）

列名	类型	描述
statement	string	声明签名/主张，去掉了前导关键字的完整声明（不含证明）
proof	string	完整的证明/主体，若无则为空
type	string	声明关键词
symbolic_name	string	声明标识符
library	string	子库名称
filename	string	相对于仓库的源文件路径
imports	list[string]	文件级别的 Require/Import 模块列表
deps	list[string]	数据集中被引用的内部标识符列表
docstring	string	前的文档注释，若无则为空
source_url	string	上游仓库地址
commit	string	提取时的上游提交哈希

统计信息

• 含证明的记录：10,619 条（占比 31.4%）
• 含文档注释的记录：0 条（0.0%）
• 子库数量：91 个

按声明类型统计

类型	数量
lemma	18,703
definition	8,946
theorem	1,305
judgement	1,186
type	1,110
function	910
macro	764
axiom	457
corollary	239
assumption	179
conjecture	42
proposition	19
formula	10
fact	1

数据来源

• 仓库地址：https://github.com/nasa/pvslib
• 提取提交：59714e007f6acc7440fe014ae7ff83bfb2ef0696
• 许可证：other

用途

每条声明被拆分为 statement（签名/主张）和 proof（证明/主体），两者互斥且共同构成完整的声明，适用于证明建模、自动形式化、检索以及通过 deps 进行依赖分析。

引用

bibtex @misc{pvs_nasalib_dataset, title = {PVS-NASALib}, author = {Norton, Charles}, year = {2026}, note = {Extracted from https://github.com/nasa/pvslib, commit 59714e007f6a}, url = {https://huggingface.co/datasets/phanerozoic/PVS-NASALib} }

搜集汇总

数据集介绍

构建方式

PVS-NASALib数据集源自NASA维护的PVS形式化验证库（NASALib），从GitHub仓库特定提交（`59714e007f6a`）中提取所有声明（declaration），并将其拆分为`statement`（签名/声明）与`proof`（证明/主体）两个互补字段。每个条目还包含声明类型、标识符、所属子库、源文件路径、文件级导入模块、库内依赖标识符、文档注释、上游URL及提交哈希，最终整合为33,871条记录，涵盖91个库。

特点

该数据集以PVS形式化证明库为核心，覆盖lemma（18,703条）、definition（8,946条）、theorem（1,305条）等14种声明类型，其中约31.4%的条目带有完整证明体。每条声明均保持原样切片，`deps`字段记录库内引用依赖，便于依赖分析与模块化研究。尽管文档注释占比为0%，但`statement`与`proof`的分离设计为定理证明、自动形式化、检索和依赖分析提供了结构化基础。

使用方法

使用者可直接加载各字段进行多任务处理：基于`statement`与`proof`构建证明序列预测模型，利用`type`和`symbolic_name`进行声明分类与检索，借助`deps`进行依赖图构建与模块相关性分析。数据集以默认配置提供单个训练集（33,871条），文件分片存储于`data/train-*`路径下，适合使用HuggingFace的`datasets`库快速加载。引用时请标注原始NASA PVS库及对应提交版本。

背景与挑战

背景概述

PVS-NASALib数据集由Charles Norton于2026年创建，源自美国国家航空航天局（NASA）的PVS形式化验证库（NASALib），旨在为自动定理证明、形式化方法以及程序验证等领域提供结构化的声明与证明数据。该数据集包含了来自91个子库的33,871条声明条目，涵盖了引理、定义、定理、推论等多种类型，每条记录均提供了声明签名、证明体、依赖关系等丰富元信息。其发布标志着形式化验证数据从分散的证明库向机器可读、可复用的资源转变，为机器学习驱动的形式化推理、自动证明生成以及依赖分析提供了宝贵的基础设施，显著推动了形式化方法与人工智能的交叉研究。

当前挑战

PVS-NASALib所面临的挑战首先体现在领域问题上：形式化定理证明中的数据稀疏性与证明结构复杂性使得模型难以学习到有效的推理策略，而现有神经符号方法在处理高阶逻辑与代换规则时仍存在泛化瓶颈。在数据集构建过程中，挑战亦十分显著：从NASA庞大的PVS库中提取声明时需精确解析复杂的语法结构，确保声明与证明体的无歧义划分；此外，仅有31.4%的条目包含证明体，大量声明缺乏完整证明，限制了监督学习范式的应用；不同子库间采用的命名约定与依赖模式差异巨大，进一步增加了跨库迁移学习的难度。

常用场景

经典使用场景

PVS-NASALib数据集汇聚了来源于NASA PVS形式化定理证明库的33871条声明，涵盖了引理、定义、定理、判定、类型、函数、宏、公理、推论、假设、猜想、命题、公式等多种形式化数学构造。该数据集的经典使用场景聚焦于定理证明领域的深度研究，特别是针对PVS证明环境中的自动定理证明、证明合成、证明检索以及依赖关系分析。研究人员可通过将每条声明拆分为“statement”（签名或断言）与“proof”（证明体）两个正交部分，构建证明建模与自动形式化的基准测试任务。此外，数据集中丰富的“deps”字段（跨语料标识符引用）为依赖图分析和证明结构挖掘提供了宝贵线索，使其成为推动形式化方法智能化发展的关键资源。

实际应用

在实际应用层面，PVS-NASALib的潜力广泛分布于航空航天软件验证、安全协议分析、嵌入式系统建模等对可靠性与正确性要求极高的领域。NASA的PVS库本身即承载了大量真实的航空航天形式化规范，例如针对空中交通管理（如ACCoRD算法）的关键属性验证。基于该数据集训练的智能证明助手能够辅助工程师在系统开发早期发现逻辑缺陷，自动化完成重复性的证明任务，进而缩短认证周期。此外，在形式化方法教育中，该数据集可作为高质量的教学案例库，帮助学习者理解复杂定理的证明结构与模块间依赖关系，提升形式化建模的实践能力。

衍生相关工作

PVS-NASALib的发布已衍生出多条极具影响力的研究路径。基于该数据集的证明-声明配对结构，学界发展出面向PVS的证明步骤预测模型与基于Transformer的证明状态嵌入方法，显著提升了自动定理证明的搜索效率。围绕其丰富的“deps”依赖信息，涌现出一系列关于形式化证明库的图神经网络建模工作，旨在捕捉声明间的逻辑依赖以辅助证明推荐。此外，该数据集与抽象语法树和类型信息结合后，催生了面向形式化数学的代码生成与程序修复技术。某些工作将其与Coq、Isabelle等其它证明助手的语料进行跨平台对齐，推动了统一形式化知识图谱的构建，进一步拓展了形式化方法的跨系统可迁移性研究。