metamath-proof-graphs

Metamath证明图数据集（10k）包含来自大约45,000个定理的Metamath数据库中的前10,000个证明的图数据集。每个示例都是一个有向无环图（DAG）。节点特征是Metamath语句的768维CodeBERT嵌入。标签是证明中每个节点所需的定理，经过合并罕见的标签后，共有3,358个不同的标签。结论节点进行了遮蔽处理，使得模型必须直接从图结构和其他节点预测最后的逻辑步骤。训练数据中包括了所有的定理语句，因为模型需要将定理本身视为先验知识。在Metamath证明语言中，用于证明一步的任何定理的索引始终小于或等于被证明的定理的索引。因此，后续定理永远不会出现在早期证明中。

原始信息汇总

Metamath Proof Graphs (10k) 数据集概述

数据集基本信息

• 许可证: MIT
• 任务类别: 图机器学习
• 标签: 图、图神经网络、Metamath、PyTorch Geometric、TopoBench
• 数据规模: 10K-100K
• 数据集摘要: 包含前10,000个Metamath证明的基于图的数据集，包括CodeBERT节点嵌入、DAG结构、3,358个经过罕见标签折叠后的标签、结论掩码和固定的训练/验证/测试分割

数据集内容

• 数据文件: data.pt
• 文件内容:
  • data - 存储所有节点特征、边和标签的PyG Data对象
  • slices - 用于重建单个图的索引信息
  • train_idx, val_idx, test_idx - 固定的图级分割

数据集特性

• 数据来源: 来自约45,000个定理的Metamath数据库的前10,000个证明
• 图结构: 有向无环图
• 节点特征: 768维CodeBERT嵌入的Metamath语句
• 标签: 每个节点所需的证明定理（公理和假设共享固定标签）
• 标签处理: 3,358个不同标签，训练集中出现次数≤5的罕见标签被折叠为UNK
• 特殊处理: 结论节点的嵌入被置零，模型必须直接从图结构和其他节点预测最终逻辑步骤
• 训练数据: 包含所有定理语句（不仅是证明）
• 证明语言特性: 用于证明步骤的任何定理的索引始终≤被证明的定理索引

基本使用方法

python import torch

obj = torch.load("data.pt", weights_only=False)

data = obj["data"] slices = obj["slices"] train_idx = obj["train_idx"] val_idx = obj["val_idx"] test_idx = obj["test_idx"]

搜集汇总

数据集介绍

构建方式

在形式化数学证明领域，该数据集基于Metamath证明库的前10,000条定理构建，通过解析严谨的逻辑推导结构生成有向无环图。每个节点采用CodeBERT模型提取768维语句嵌入特征，边缘对应证明步骤间的逻辑依赖关系。标签系统经过优化处理，将训练集中出现频次≤5的稀有标签统一归并为UNK类别，最终形成3,358个区分度良好的标签体系，同时对所有结论节点实施嵌入归零掩码以强化结构推理能力。

特点

该数据集最显著的特征在于其严格的数学逻辑约束，所有证明图均满足拓扑序原则——后续定理永远不会出现在先验证明中。节点特征融合了语义嵌入与结构信息，结论掩码机制迫使模型必须从图拓扑和其他节点特征中推导最终推理步骤。数据规模涵盖10,000个独立证明实例，既包含完整证明链也包含作为先验知识的定理陈述，这种设计使模型能同时学习基础逻辑规则与复杂推导模式。

使用方法

使用者可通过加载标准化PyTorch Geometric数据文件快速部署，数据对象包含整合的图结构信息、节点切片索引及预划分的训练/验证/测试集标识。典型应用流程包括解析data字段获取全量图数据，利用slices重构独立图实例，再通过固定划分的索引集进行模型训练与评估。这种即用型设计支持研究者直接聚焦于图神经网络架构创新，无需额外处理原始证明的逻辑解析与特征工程。

背景与挑战

背景概述

在形式化验证领域，数学定理的机器证明长期面临结构化表示与自动化推理的挑战。Metamath Proof Graphs数据集由拓扑基准研究团队于2024年构建，基于Metamath形式化数学库的前一万条证明记录，将数学证明过程转化为有向无环图结构。该数据集创新性地采用CodeBERT模型生成节点嵌入向量，通过结论掩码机制强化模型对证明逻辑的推理能力，为图神经网络在形式化数学领域的应用提供了标准化基准。

当前挑战

该数据集致力于解决形式化数学证明的自动重构问题，核心挑战在于从图结构推导未暴露的结论节点。构建过程中面临多重技术难点：需将自然语言数学陈述转化为机器可理解的嵌入表示，处理3,358类逻辑标签的长尾分布，同时保持证明图的拓扑约束特性。数据集的稀疏标签与复杂依赖关系对图神经网络的泛化能力提出严峻考验，要求模型在保留数学语义的前提下完成跨定理的推理任务。

常用场景

经典使用场景

在形式化验证与自动推理领域，该数据集作为图结构知识的典型载体，被广泛用于图神经网络模型的训练与评估。其经典应用场景聚焦于数学定理的自动证明任务，通过将Metamath证明库中的逻辑推导过程建模为有向无环图，使模型能够学习从前提条件到结论的复杂推理路径。这种结构化表示不仅保留了数学证明的严谨性，还为机器学习模型提供了可解释的推理框架。

实际应用

在实际工程层面，该数据集支撑的模型已逐步应用于程序验证和数学辅助系统。通过将代码规范或数学猜想转化为图结构，系统能够自动生成验证路径或提供证明建议。这种技术显著提升了形式化验证工具的效率，特别是在操作系统内核验证和密码学协议证明等高可靠性需求场景中，为工程师提供了可靠的自动化辅助手段。

衍生相关工作

基于该数据集衍生的经典研究包括拓扑基准挑战赛中的多项图神经网络创新，这些工作深入探索了结构感知的表示学习机制。后续研究进一步扩展了图注意力网络在逻辑推理中的应用，开发出能够处理长距离依赖的推理路径编码器。这些衍生成果不仅推动了几何深度学习的发展，还为构建可解释的AI推理系统奠定了理论基础。