NuminaMath-LEAN-satp-buffer

NuminaMath-LEAN-satp-buffer是一个用于定理证明的数据集，包含在构建SATP（Steering Aesop for Theorem Proving）回放缓冲区期间收集的Aesop策略配置，以及与每个定理初始Lean目标状态的配对。每条数据代表一个`(theorem, aesop_config) → reward`示例，旨在作为训练SATP-aesop-policy的正/负回放材料。数据集包含5,830行数据，每条数据包含定理的唯一标识符、配置唯一标识符、形式化声明、目标状态、策略字符串、奖励分数（仅包含成功的+1.0示例）以及预留的引理名称和分数字段。数据来源于NuminaMath-LEAN-SATP-cleaned数据集，使用Lean工具链leanprover/lean4:v4.17.0-rc1生成。适用于文本生成和定理证明任务。

NuminaMath-LEAN-satp-buffer is a dataset for theorem proving, containing Aesop tactic configurations collected during the construction of the SATP (Steering Aesop for Theorem Proving) replay buffer, paired with the initial Lean goal state of each theorem. Each data point represents a `(theorem, aesop_config) → reward` example, intended to serve as positive/negative replay material for training the SATP-aesop-policy. The dataset contains 5,830 rows of data, each including the theorems unique identifier, configuration unique identifier, formal statement, goal state, tactic string, reward score (only successful +1.0 examples), and reserved lemma name and score fields. The data is sourced from the NuminaMath-LEAN-SATP-cleaned dataset and generated using the Lean toolchain leanprover/lean4:v4.17.0-rc1. Suitable for text generation and theorem proving tasks.

原始信息汇总

数据集概述：NuminaMath-LEAN-satp-buffer

该数据集是一个用于训练 SATP-aesop-policy 的回放缓冲区（replay buffer），记录了在 Lean 定理证明过程中，使用不同 Aesop 策略配置对定理进行证明的结果（成功或失败）。每个样本是一个 (定理, Aesop配置) → 奖励 的元组。

基本信息

• 许可证: Apache-2.0
• 任务类别: 文本生成
• 语言: 英语
• 标签: lean4, mathlib, theorem-proving, aesop, reinforcement-learning, replay-buffer
• 数据集大小: 约 1K - 10K 条记录
• 下载大小: ~2.17 MB
• 数据集大小: ~18.66 MB
• 分片: 仅包含训练集（train），共 12,564 个样本

数据内容与结构

• 行数: 5,830（过滤后仅保留成功样本）
• 奖励标签: 仅包含 +1.0（成功关闭目标），失败样本已被丢弃
• 来源定理: 来自 NuminaMath-LEAN-SATP-cleaned 数据集
• Lean 工具链: leanprover/lean4:v4.17.0-rc1
• Aesop 配置标识: 18af71034f62230b（基于 tactic_string 的 SHA256 哈希）

数据模式 (Schema)

列名	类型	说明
theorem_uuid	string	定理形式化语句的 SHA256 哈希（前16位），可关联到 NuminaMath-LEAN-satp 数据集
config_uuid	string	Aesop 策略配置的 SHA256 哈希（前16位），用于标识配置
formal_statement	string	完整的 Lean 定理声明（以 import Mathlib 开头，以 := by 结尾）
tactic_string	string	完整的 aesop 策略块，包含配置和自定义规则
reward	float64	奖励值：+1.0 表示成功（本版本已丢弃失败样本）
lemma_names	list[string]	预留字段，用于检索式前提名称（本版本为空）
lemma_scores	list[float64]	预留字段，用于检索相似度得分（本版本为空）
goal_state	string	证明入口处的 Lean 目标状态（格式化输出），与 NuminaMath-LEAN-satp.goal_state 字节一致

Aesop 配置详情

每条记录的 tactic_string 都完全一致，包含如下配置：

• 搜索约束: maxRuleApplicationDepth=30, maxRuleApplications=200, maxNormIterations=100, maxGoals=64
• 禁用默认简化: enableSimp=false, enableUnfold=false
• 启用全局简化: useSimpAll=true, useDefaultSimpSet=true
• 终端模式: terminal=true
• 15 条自定义规则: 包括 linarith, nlinarith, ring, positivity, omega, ring_nf, simp, simp_all, field_simp, norm_num, norm_cast 等（均为 unsafe 90% 优先级）

数据来源与构建

• 来源: 基于之前无搜索边界限制的版本（9a97704747726569 配置）重新运行，使用上述有边界的 Aesop 配置过滤成功样本。
• 去重与验证: 仅保留在有限搜索边界下成功关闭目标的记录，且 tactic_string 经过重新验证。
• 关联数据集: 该数据集是 NuminaMath-LEAN-satp 系列数据集的一部分，与之相关的还有：
  • NuminaMath-LEAN-satp（主训练集）
  • NuminaMath-LEAN-satp-gaps（增强训练集，包含子目标记录）
  • minif2f-satp（留出评估和验证集）

使用方式

python from datasets import load_dataset ds = load_dataset("ChristianZ97/NuminaMath-LEAN-satp-buffer", split="train")

引用

bibtex @dataset{numinamath_lean, author = {{Numina Math}}, title = {NuminaMath-LEAN}, year = {2025}, url = {https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN} }

搜集汇总

数据集介绍

构建方式

该数据集源自NuminaMath-LEAN项目，通过SATP（Steering Aesop for Theorem Proving）框架构建，旨在收集Aesop策略配置与定理证明成功率的配对数据。构建过程中，研究者从NuminaMath-LEAN-SATP-cleaned数据集中抽取定理，并使用Lean 4.17.0-rc1工具链，对每条定理应用一组具有严格搜索边界（如最大规则应用深度30、最多规则应用200次等）的Aesop配置进行验证。初始版本采用无界搜索，而本版本则对无界搜索中的成功案例重新应用有界配置，仅保留奖励值为+1.0的正样本，从而形成稳定的回放缓冲区。每条记录包含定理的唯一标识、Aesop配置标识、形式化陈述、初始目标状态、策略字符串及奖励标签，并预留了引理名称与评分字段以备检索增强之用。

使用方法

该数据集的使用方法简洁直接，用户可通过HuggingFace的datasets库加载。具体操作包括：使用`load_dataset`函数指定数据集名称`ChristianZ97/NuminaMath-LEAN-satp-buffer`，并选择训练集划分，即可获取包含定理标识、形式化陈述、目标状态、策略字符串及奖励标签的字典结构。每条记录中的`goal_state`字段与姊妹数据集`NuminaMath-LEAN-satp`格式一致，便于交叉引用。数据集预留的`lemma_names`和`lemma_scores`字段可用于检索增强的归因分析，当前版本虽留空，但为未来扩展提供了接口。研究人员可将此回放缓冲区直接用于训练SATP-aesop-policy模型，通过正样本策略模仿学习或强化学习范式进行策略优化，从而提升自动化定理证明的效率与成功率。

背景与挑战

背景概述

NuminaMath-LEAN-satp-buffer数据集由ChristianZ97等研究者于2025年构建，隶属于NuminaMath项目，旨在推进数学定理的自动化证明。该数据集聚焦于利用强化学习优化Aesop策略的搜索过程，核心研究问题是通过记录定理与Aesop配置之间的奖励映射，训练一个能够智能选择策略配置的策略网络SATP-aesop-policy。数据集包含5830条成功证明的样本，每条样本记录了定理的形式化陈述、初始目标状态以及对应的Aesop策略配置与奖励标签。其构建基于Lean 4证明助手，从NuminaMath-LEAN中筛选定理，通过有界搜索配置生成正例，为强化学习回放缓冲区提供了高质量训练材料，对形式化数学与定理证明的自动化研究具有重要推动作用。

当前挑战

该数据集所解决的领域问题在于，定理证明中的自动策略搜索常因搜索空间过大而效率低下，Aesop等工具虽能利用规则集进行证明，但缺乏动态调整配置的能力。该数据及面临的核心挑战包括：1）如何构建高效的有界搜索配置，在限制搜索深度与规则应用次数的同时确保证明成功率，避免错过有效证明路径；2）数据构建过程中需严格验证每个定理与配置组合的可复现性，通过规范化处理消除注释与空白差异，并确保目标状态的字节级一致性；3）正负样本平衡问题，该版本仅保留成功案例，丢弃失败样本，可能影响策略学习中对失败模式的识别，需依赖先前无界搜索版本提供负例材料。

常用场景

经典使用场景

NuminaMath-LEAN-satp-buffer数据集在数学定理自动证明领域扮演着关键角色，其核心用途在于构建强化学习中的回放缓冲区，为训练基于Aesop策略的定理证明智能体提供高质量的样本。该数据集精心收集了每次定理证明尝试中Aesop策略配置与初始目标状态的配对数据，并附带了明确的奖励标签（成功为+1.0），从而构建了一个正样本反馈池。研究者可利用这些数据来训练策略模型（如SATP-aesop-policy），使其学会根据给定的形式化语句和初始目标状态，选择最有可能闭合证明的Aesop参数组合，从而提升自动定理证明系统的性能。

解决学术问题

该数据集直接回应了形式化数学领域中如何高效探索庞大策略空间这一学术难题。通过记录带奖励的Aesop配置与定理配对，它解决了强化学习方法在定理证明中面临的稀疏奖励与样本效率低下的问题。这些数据使得研究人员能够在离线环境中进行策略学习，避免了反复与复杂证明环境交互的高昂成本。此外，它还为研究策略泛化能力、配置空间剪枝以及证明难度评估提供了基准，推动了从手工规则系统向数据驱动证明系统的范式转变，对形式化验证的自动化具有深远意义。

实际应用

在实际应用中，NuminaMath-LEAN-satp-buffer训练的策略模型可直接集成到Lean等交互式定理证明器中，为数学家或软件工程师提供智能的自动证明建议。例如，当用户在证明环境中输入一条未关闭的定理时，模型可根据目标状态迅速推荐最可能成功的Aesop配置参数，从而降低手动调试证明脚本的繁琐程度。此外，该数据集的回放缓冲设计也适用于其他形式化系统（如Coq、Isabelle）中启发式策略的调优，为构建更通用的数学证明助手奠定了数据基础。

数据集最近研究

最新研究方向

该数据集聚焦于利用强化学习中的回放缓冲区技术优化Lean4定理证明器Aesop的策略选择，为神经符号结合的自动推理开辟了新路径。通过采集Aesop在不同配置下对数学定理的证明成败数据（reward=+1.0），形成结构化经验池，驱动策略网络SATP-aesop-policy的离线训练。前沿方向包括：基于此数据集的证明策略泛化性研究——探索有限搜索边界（如maxRuleApplications=200）下学到的策略能否迁移至更大规模的数学库Mathlib；以及将其与子目标增强数据集NuminaMath-LEAN-satp-gaps结合，构建分层强化学习范式，突破单步证明的局部最优困境。该工作与Lean社区中‘可搜索Tactic’趋势紧密呼应，为后续将大语言模型与形式化验证工具协同进化提供了可复用的数据基座。”