l3lab/ntp-mathlib-instruct-context

miniCTX数据集是一个用于神经定理证明的数据集，特别关注长上下文环境下的证明。数据集包含从Mathlib中提取的Lean 4战术预测示例，每个示例包括提示（指令、前置文件内容、证明状态）和完成（战术）。文件内容被截断至1024个令牌。数据集生成使用了`ntptoolkit`的`ntp-training-data`和`instruction_tuning.py`工具，并提供了生成配置的详细信息。

原始信息汇总

数据集概述

数据集名称

miniCTX: Neural Theorem Proving with (Long-)Contexts

数据集内容

• 来源：Lean 4 tactic prediction examples extracted from Mathlib.
• 示例组成：
  • prompt：
    • 包含instruction, preceding file content, proof state 或 instruction, proof state
  • completion：tactic
• 文件内容：已截断至1024 tokens。

数据集配置

• 配置名称：default
• 数据文件：
  • split：train, dev, test
  • path："with_context_mathlib_only/with_context_train*", "with_context_mathlib_only/with_context_dev*", "with_context_mathlib_only/with_context_test*"

版本信息

• 生成工具：ntptoolkit的ntp-training-data和instruction_tuning.py
• 配置详情： json { "repo": "https://github.com/leanprover-community/mathlib4", "commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86", "lean": "leanprover/lean4:v4.4.0", "name": "mathlib", "import_file": "Mathlib.lean", "imports": ["Mathlib"] }

引用信息

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

搜集汇总

数据集介绍

构建方式

在数学定理证明领域，l3lab/ntp-mathlib-instruct-context数据集的构建基于Lean 4定理证明系统的Mathlib库。该数据集通过ntptoolkit的ntp-training-data工具，以及instruction_tuning.py脚本，从Mathlib 4的GitHub仓库中提取tactic预测示例。数据集包含了训练、开发和测试三个部分，其构建过程中截取了前文内容至1024个token，以提供上下文信息。

特点

本数据集的特点在于，它不仅提供了指令和证明状态，还包括了前文内容，这为理解定理证明过程中的上下文提供了重要支持。数据集专注于Lean 4的tactic预测，其样本来源于实际的数学定理证明过程，具有高度的专业性和实用性。此外，该数据集遵循学术规范，提供了详尽的引用信息，便于学术交流。

使用方法

使用l3lab/ntp-mathlib-instruct-context数据集时，用户需遵循其提供的文件结构，分别加载训练、开发和测试集。数据集以JSON格式存储，其中包含了prompt和completion字段，分别代表输入提示和输出完成。用户可以通过这些字段来训练和评估神经定理证明模型，以提升其在数学定理证明任务上的性能。

背景与挑战

背景概述

在数学定理证明这一研究领域，l3lab团队开发的ntp-mathlib-instruct-context数据集应运而生。该数据集于2024年，由Jiewen Hu、Thomas Zhu和Sean Welleck等研究人员构建，旨在通过提供_Lean 4战术预测示例，推进神经网络在数学证明中的应用。数据集的核心研究问题是提高定理证明的自动化水平，其对数学定理证明领域的科研工作产生了深远影响。

当前挑战

该数据集面临的挑战主要体现在两个方面：一是解决领域问题中的挑战，即如何通过神经网络处理数学证明中的长文本上下文信息，实现高效的定理证明；二是构建过程中的挑战，包括如何从_Lean 4的Mathlib库中提取并处理大量的战术预测示例，以及如何确保数据集的质量和实用性。

常用场景

经典使用场景

在数学定理证明的领域内，l3lab/ntp-mathlib-instruct-context数据集的经典使用场景在于，它提供了含指令和上下文的 Lean 4 tactic 预测示例，这些示例来源于 Mathlib 的实际证明过程。研究人员和开发者可以利用该数据集进行神经定理证明模型的训练，以提高模型对复杂数学证明的理解和预测能力。

实际应用

在实际应用中，l3lab/ntp-mathlib-instruct-context数据集的应用范围广泛，它不仅能够辅助数学研究者在定理证明上的工作，还可以为自动化数学教育、智能问答系统等领域提供技术支持，推动数学知识的普及和智能化。

衍生相关工作

基于l3lab/ntp-mathlib-instruct-context数据集，衍生了一系列相关工作，包括但不限于改进神经定理证明算法、探索更高效的上下文处理机制以及结合自然语言处理技术来提升模型的指令理解能力，这些研究进一步拓展了数据集的应用范围，并对数学自动化证明领域产生了深远影响。