hoskinson-center/proof-pile
收藏数据集概述
数据集描述
proof-pile 是一个 13GB 的预训练数据集，包含 83 亿个使用 gpt-neox 分词器的数学文本标记。数据集由多种来源组成，包括：
- ArXiv.math (10GB)
- 开源数学教科书 (50MB)
- 形式数学库 (500MB)
- Lean mathlib 和其他 Lean 仓库
- Isabelle AFP
- Coq 数学组件和其他 Coq 仓库
- HOL Light
- set.mm
- Mizar 数学库
- Math Overflow 和 Math Stack Exchange (2.5GB)
- Wiki 风格来源 (50MB)
- ProofWiki
- Wikipedia 数学文章
- MATH 数据集 (6MB)
数据集的构建可以通过 proof-pile Github 仓库 中的代码和说明进行重现。
支持的任务
该数据集旨在用于语言模型的预训练和微调。预计在 proof-pile 上训练的模型将有许多下游应用，包括非正式定量推理、形式定理证明、形式数学的语义搜索和自动形式化。
语言
proof-pile 中的所有非正式数学文本均以英语和 LaTeX 编写（arXiv 文章中的其他语言使用 languagedetect 进行过滤）。数据集中包含的形式定理证明语言有 Lean 3、Isabelle、Coq、HOL Light、Metamath 和 Mizar。
评估
数据集中的 set.mm 版本有 10% 的证明被替换为 ? 字符，以保留用于 Metamath 证明器的验证和测试集。验证和测试集的精确分割可以在以下链接找到：验证 和 测试。
数据集中使用的 Lean mathlib 提交版本为 6313863。后续提交的定理可用于评估 Lean 定理证明器。
该数据集仅包含 MATH 数据集 的训练集。但由于包含 ProofWiki、Stacks Project、Trenchs Analysis 和 Steins Number Theory，因此无法在 NaturalProofs 数据集 上进行评估。
数据预处理
本节描述了对数据集各子集进行的重要过滤和转换。
arXiv.math arXiv.math 数据集庞大、异构且包含大量噪声。我们使用以下启发式方法选择要包含在数据集中的文件：
- 仅保留扩展名为
.tex的文件。 - 仅包含使用
utf-8/16/32或latin-1文本编码的文件。 - 丢弃不包含部分、章节、节、小节、段落或小段落标题的文件。
- 删除包含关键字
gnuplot的文件。 - 仅包含由 langdetect 库 确定为英语的文章。
- 排除少于 280 个字符的文件（字符计数在删除子字符串后进行）。
此外，我们对 arXiv.math 文本应用以下转换：
- 删除
egin{document}和end{document}之外的所有内容。 - 删除
Refs、egin{thebibliography}或egin{bibdiv}及其之后的内容。 - 删除注释。
- 将三个以上的连续换行符替换为三个连续换行符。
Stack Exchange 我们仅包含至少有 5 个赞和答案的问题。Stack Exchange 帖子的格式如下：
QUESTION [{num_upvotes} upvotes]: {text of question}
REPLY [{num_upvotes} votes]: {text of reply}
REPLY [{num_upvotes} votes]: {text of reply}
. . .
set.mm
我们通过遵循 mm-extract 仓库 中的说明，将 set.mm 转换为人类可读形式。
贡献者
作者：Zhangir Azerbayev, Edward Ayers, Bartosz Piotrowski。
我们感谢 Jeremy Avigad, Albert Jiang 和 Wenda Li 的宝贵指导，以及 Hoskinson Center for Formal Mathematics 的支持。
