ChristianZ97/NuminaMath-LEAN-SATP-cleaned-gaps

NuminaMath-LEAN-SATP-cleaned-gaps 是一个 Lean 4 子目标数据集，从自然语言草稿到 Lean 草图，再到真实的 Lean 目标状态提取。数据集包含草图中的开放孔（sorry），并与该孔的确切 Lean 目标状态配对，适合作为每个子目标的证明步骤训练信号。数据集包含 904 个问题，总共有 10,918 个间隙，平均每个问题约 12.1 个间隙。这是一个部分收获：仅包含验证器端到端接受的草图子目标。模式包括问题级别的 UUID、正式声明以及带有各自 UUID 和目标状态的间隙列表。数据集旨在用作下游证明器的目标，而不是作为监督证明跟踪。

NuminaMath-LEAN-SATP-cleaned-gaps is a Lean 4 sub-goal dataset harvested from natural-language draft → Lean sketch → real-Lean goal-state extraction. The dataset contains open holes (sorry) inside a sketch, paired with the exact Lean goal-state at that hole, suitable as a per-sub-goal prove-step training signal. The dataset includes 904 problems with a total of 10,918 gaps, averaging about 12.1 gaps per problem. This is a partial harvest: it ships only sub-goals from sketches that the verifier accepted end-to-end. The schema includes problem-level UUID, formal statement, and a list of gaps with their respective UUIDs and goal states. The dataset is intended for use as targets for a downstream prover, not as supervised proof traces.

搜集汇总

数据集介绍

构建方式

该数据集基于NuminaMath-LEAN形式化语句池，通过自然语言草稿到Lean草图再到真实Lean目标状态的三阶段流水线构建而成。具体而言，利用大型语言模型Qwen3.6-27B-FP8为每个问题生成单一草图，草图中嵌入`prove_with`宏和`sorry`占位符以标识待证明的子目标。随后，通过`sketch_masking.py`工具将所有`prove_with`强制替换为`clear * - hints; trace_state; sorry`序列，确保仅保留结构性的证明骨架。利用`lake env lean --json`验证器对掩码后的草图进行编译，仅接受无错误且每个`prove_with`位点均产生`trace_state`信息的草图，最终从每个接受草图中按位点提取出对应的Lean目标状态，形成每个问题下多个子目标的集合。

特点

该数据集的核心特点在于提供了形式化定理证明中的细粒度子目标级训练信号。总包含904个问题，从中提取出10,918个独立的子目标缺口，平均每个问题约含12.1个缺口，为证明步骤的逐一学习提供了丰富样例。每个样本由问题级UUID、完整形式化语句以及缺口列表构成，列表中的每个缺口具有全局唯一的gap_uuid和经过clear操作修剪后的精确目标状态，确保了数据的一致性与可追踪性。数据集仅收录验证器端到端接受的草图，排除了任何编译失败的尝试，保障了数据质量。此外，缺口在列表中的顺序遵循验证器输出的消息顺序，虽无语义含义，但忠实反映了结构展开路径。

使用方法

使用时可借助HuggingFace Datasets库便捷加载，调用`load_dataset("ChristianZ97/NuminaMath-LEAN-satp-gaps", split="train")`即得训练集。为获得平坦化的（缺口，目标状态）视图以用于训练，可将每个样本中的`gaps`列表展开为独立行，每个独立行包含原问题UUID、形式化语句以及单个缺口的UUID和目标状态。该数据集专为面向子目标的证明器设计，可作为每个开放子目标的输入，而非监督式完整证明轨迹。建议结合配套的入口数据集`NuminaMath-LEAN-satp`使用，它提供问题级的初始目标状态，二者互补以构建层次化的定理证明训练框架。

背景与挑战

背景概述

在人工智能驱动的定理证明领域，形式化数学推理的自动化一直是一项极具挑战性的前沿课题。NuminaMath-LEAN-SATP-cleaned-gaps数据集由ChristianZ97于2026年创建，旨在通过分解自然语言草稿与Lean 4形式化证明之间的鸿沟，为神经定理证明器提供细粒度的子目标训练信号。该数据集从NuminaMath-LEAN语料库中抽取2000个问题，利用Qwen3.6-27B-FP8模型生成草图，并通过验证器筛选出904个通过端到端验证的示例，最终得到10918个独立的证明子目标（gaps）。其核心研究问题在于：如何将复杂的数学定理证明拆解为可独立求解的子步骤，并为每个子步骤提供精确的Lean目标状态，从而训练出能够逐步推理的神经证明器。该数据集为自动定理证明领域提供了一种新的监督范式，推动了形式化数学与语言模型融合的进展。

当前挑战

该数据集所解决的核心领域挑战在于，传统的端到端定理证明方法难以处理复杂证明中的中间步骤，而该数据集通过提取每个子目标的状态，使得模型能专注于局部证明的生成，降低了整体推理的难度。从构建过程来看，主要挑战包括三个方面：首先，草图生成阶段需确保LLM输出的Lean代码在不改变语义的前提下被正确掩码（masking），以保留结构性的证明骨架；其次，验证环节要求每个`prove_with`占位符均能通过`lake env lean --json`产生对应的目标状态，任何编译错误或缺失的跟踪信息都会导致对应示例被丢弃，这导致初始覆盖度仅约45%；最后，目标状态经过`clear * - hints`裁剪后，去除了未实例化的假设，这一预处理虽简化了学习目标，但也可能丢失证明所需的上下文信息，增加了模型的隐性推理负担。

常用场景

经典使用场景

在人工智能辅助定理证明领域，NuminaMath-LEAN-SATP-cleaned-gaps 数据集为细粒度的形式化证明步骤训练提供了宝贵资源。该数据集通过从自然语言草稿到 Lean 草图再到真实 Lean 目标状态的流水线，提取了约一万余个内部子目标（gaps），每个子目标对应一个待填充的证明洞（sorry），并配有精确的 Lean 目标状态。这使得研究者能够以每个证明子步骤为单位，训练模型掌握逐步推理和局部证明的能力，填补了传统数据集只提供完整定理与初始目标状态之间的空白，为分步式定理证明学习开辟了新路径。

实际应用

在实际应用中，该数据集可直接用于训练和评估面向 Lean 4 定理证明器的子目标级证明模型。借助这些子目标状态，研究者可以构建能够逐步生成证明步骤的神经网络系统，例如训练一个序列到序列模型，给定当前目标状态后预测下一步的证明操作。此外，该数据集还可作为强化学习环境中的状态表示库，用于训练在证明树中搜索最优路径的智能体。在数学教育软件中，这些子目标也能帮助系统为学生生成更细致的解题指导步骤，提升交互式定理证明工具的教学实用性。

衍生相关工作

基于本数据集，已衍生出一系列相关工作，其中最典型的是 NuminaMath-LEAN-satp 主训练集及其配套的缓冲区数据集和验证拆分集。主训练集提供了每个问题的完整形式化陈述与初始目标状态，而本数据集作为其增广补充，贡献了内部的子目标结构。此外，配套的 minif2f-satp 验证集为跨数据集的评估提供了标准化的测试基准。这些工作共同构成了一个从问题陈述到子目标分解再到完整证明验证的完整 pipeline，推动了 Lean 4 形式化数学证明领域从宏观到微观的全面研究发展。