l3lab/ntp-mathlib

miniCTX数据集是一个用于神经定理证明的数据集，特别关注处理长上下文的情况。该数据集包含从Mathlib中提取的Lean 4战术预测示例，这些示例尚未为指令调优格式化。数据集通过`ntptoolkit`的`ntp-training-data`工具生成，使用了特定的配置来提取数据。数据格式包括证明状态、战术调用前的源代码、下一个战术、战术调用前的声明、声明的唯一ID、声明本身以及文件ID。

原始信息汇总

数据集概述

数据集名称

miniCTX: Neural Theorem Proving with (Long-)Contexts

数据集内容

• 来源：Lean 4 tactic prediction examples extracted from Mathlib.
• 格式：未格式化，不适用于指令调整（包括数据分割）。

版本信息

• 生成工具：ntptoolkit的ntp-training-data。
• 配置详情：
  • 仓库地址：https://github.com/leanprover-community/mathlib4
  • 提交版本：cf8e23a62939ed7cc530fbb68e83539730f32f86
  • Lean版本：leanprover/lean4:v4.4.0
  • 数据集名称：mathlib
  • 导入文件：Mathlib.lean
  • 导入模块：Mathlib

数据集使用示例

bash ds = datasets.load_dataset(l3lab/ntp-mathlib)

print(len(ds[train]))

==> 307049

数据集格式

json { state: proof state, srcUpToTactic: source up to tactic invocation, nextTactic: tactic, declUpToTactic: declariation up to tactic invocation, declId: unique ID for declaration, decl: declaration, file_tag: file ID }

引用信息

@misc{hu2024minictx, author = {Jiewen Hu and Thomas Zhu and Sean Welleck}, title = {miniCTX: Neural Theorem Proving with (Long-)Contexts}, year = {2024}, archivePrefix={arXiv}, }