l3lab/ntp-mathlib

miniCTX数据集是一个用于神经定理证明的数据集，特别关注处理长上下文的情况。该数据集包含从Mathlib中提取的Lean 4战术预测示例，这些示例尚未为指令调优格式化。数据集通过`ntptoolkit`的`ntp-training-data`工具生成，使用了特定的配置来提取数据。数据格式包括证明状态、战术调用前的源代码、下一个战术、战术调用前的声明、声明的唯一ID、声明本身以及文件ID。The miniCTX dataset is a neural theorem proving dataset with a particular focus on handling long context scenarios. It contains Lean 4 tactic prediction examples extracted from Mathlib, which have not yet been formatted for instruction tuning. The dataset is generated via the `ntp-training-data` tool included in the `ntptoolkit` using a specialized configuration for data extraction. The data format includes proof states, source code prior to tactic invocation, the next tactic, the declaration preceding the tactic invocation, the unique ID of the declaration, the declaration itself, and the file 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}, }