ChristianZ97/NuminaMath-LEAN-satp-buffer-discard

NuminaMath-LEAN-satp-buffer是一个用于定理证明强化学习任务的数据集，包含了Aesop策略配置和初始Lean目标状态的配对。每个数据行代表一个（定理，aesop配置）→奖励的示例，用于训练SATP-aesop-policy模型。数据集包含5,830行数据，奖励标签为+1.0（表示配置成功关闭目标）。数据来源于NuminaMath-LEAN-SATP-cleaned数据集，使用Lean工具链leanprover/lean4:v4.17.0-rc1构建。数据集的具体特征包括定理UUID、配置UUID、形式化声明、目标状态、策略字符串、奖励值等。

NuminaMath-LEAN-satp-buffer is a dataset for reinforcement learning in theorem proving, containing pairs of Aesop tactic configurations and initial Lean goal states. Each row represents a (theorem, aesop_config) → reward example, intended for training the SATP-aesop-policy model. The dataset contains 5,830 rows with reward labels of +1.0 (indicating successful goal closure). The source theorems are drawn from NuminaMath-LEAN-SATP-cleaned dataset, built using the Lean toolchain leanprover/lean4:v4.17.0-rc1. The dataset features include theorem_uuid, config_uuid, formal_statement, goal_state, tactic_string, reward, etc.