proofcheck/prooflang

ProofLang Corpus数据集包含从1992年至2020年间在arXiv.org上发布的论文中机械提取的370万条证明（5.58亿字）。该数据集专注于证明中使用的语言，而非数学内容，过滤掉了具体的数学内容，生成了如`Let MATH be the restriction of MATH to MATH.`这样的句子。数据集分为proofs和sentences两个主要部分，分别按证明和句子进行划分。此外，还提供了tags和raw两个辅助数据集。该数据集反映了人们如何偏好书写（非形式化的）证明，并适用于自然语言处理技术的统计分析和实验，旨在辅助开发基于语言的证明助手和检查器。

原始信息汇总

数据集概述

数据集名称： ProofLang Corpus

许可证： cc-by-4.0

任务类别： text-generation

语言： en

数据集大小： 1B<n<10B

数据集结构

配置名称：

• proofs
• sentences
• tags
• raw

数据集信息：

• proofs

  • 字节数：3197091800
  • 示例数：3681901
  • 特征：
    • fileID (字符串)
    • proof (字符串)

• sentences

  • 字节数：3736579062
  • 示例数：38899130
  • 特征：
    • fileID (字符串)
    • sentence (字符串)

下载大小： 6933683563

数据集大小： 6933670862

数据集使用

数据以压缩的TSV文件形式提供，也可通过Datasets库以编程方式访问。

数据集创建

数据集从1992年至2022年提交至arXiv.org的1.6M篇论文的LaTeX源中提取，使用Python脚本模拟LaTeX部分功能进行提取和清理。