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} }
