NuminaMath-LEAN-Filterd

Aesop RL Warm-up 数据集是一个专注于 Lean 4 定理证明的数据集，旨在为 Aesop 策略配置提供优先级标签。数据集包含安全策略（7种）和不安全策略（9种），并提供了三种不同的配置（DEFAULT_AESOP、EXPERT_AESOP、DSP_PLUS_AESOP）来测试这些策略的有效性。数据集结构包含5个字段：uuid（唯一标识符）、formal_statement（Lean 4 定理）、config_name（使用的配置名称）、is_positive（配置是否成功解决定理）、priority_levels（16个整数表示策略优先级）。数据集通过为每个定理和每种配置生成样本（正样本和负样本）来评估策略性能，总计包含107,896个源问题，生成323,688个样本，其中正样本占2.93%。每种配置的解决率分别为：DEFAULT 1.45%、EXPERT 2.52%、DSP_PLUS 4.83%。

原始信息汇总

NuminaMath-LEAN-Filterd 数据集概述

数据集基本信息

• 名称: Aesop RL Warm-up Dataset
• 语言: 英语 (en)
• 许可证: Apache-2.0
• 主要标签: lean4, theorem-proving, aesop, reinforcement-learning, warm-up
• 任务类别: 文本分类
• 数据规模: 1K<n<10K

数据集内容与目的

本数据集包含带有优先级标签的 Lean 4 定理陈述，用于 Aesop 策略配置。

策略说明

安全策略 (7种)

1. ring - 交换（半）环方程
2. abel - 阿贝尔群方程
3. norm_num - 数值归一化
4. norm_cast - 类型转换归一化
5. push_neg - 否定分布
6. field_simp - 域简化
7. zify - ℕ 到 ℤ 的转换

非安全策略 (9种)

1. linarith - 线性算术
2. nlinarith - 非线性算术
3. omega - Omega 算法
4. gcongr - 同余/单调性
5. positivity - 正性证明
6. interval_cases - 实数区间情况
7. ext - 外延性
8. exfalso - 反证法
9. split - 析取拆分

配置方案

DEFAULT_AESOP

仅使用默认策略的基本 Aesop。 优先级水平: [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

EXPERT_AESOP

安全策略（优先级 1）+ 高置信度非安全策略（100%）。 优先级水平: [9,0,9,0,0,9,0,0,9,9,0,9,0,0,0,0]

DSP_PLUS_AESOP

置信度为 90% 的决策过程。 优先级水平: [0,0,0,0,0,0,0,8,8,8,0,8,0,0,0,0]

数据集模式

包含 5 列：

• uuid (str): 唯一标识符
• formal_statement (str): Lean 4 定理
• config_name (str): 使用的配置（"DEFAULT"、"EXPERT" 或 "DSP_PLUS"）
• is_positive (bool): 该配置是否能证明该定理
• priority_levels (list[int]): 对应于配置的 16 个整数策略优先级

样本生成

对于每个定理和每种配置，创建一个样本：

• 正样本: 当 is_positive = true（配置成功证明定理）
• 负样本: 当 is_positive = false（配置未能证明定理） 每个定理产生 3 个样本（每种配置一个）。

数据集统计信息

总体统计

指标	值
总源问题数	107896
总样本数	323688
正样本数	9493
负样本数	314195
正样本率	2.93%

按配置统计

配置	正样本数	负样本数	解决率
DEFAULT	1569	106327	1.45%
EXPERT	2718	105178	2.52%
DSP_PLUS	5206	102690	4.83%

搜集汇总

数据集介绍

构建方式

在形式化定理证明领域，NuminaMath-LEAN-Filterd数据集通过系统化的方法构建而成。该数据集以Lean 4定理陈述为基础，为Aesop策略配置生成带有优先级标签的数据。针对每个定理，研究团队应用了三种预定义的配置——DEFAULT_AESOP、EXPERT_AESOP和DSP_PLUS_AESOP，分别代表基础、专家级以及侧重决策过程的策略组合。对于每种配置，系统会评估其是否能够成功证明定理，从而生成对应的正负样本。最终，每个定理产生三个样本，共计形成超过32万个数据点，构建过程兼顾了策略的多样性与证明结果的可靠性。

特点

该数据集展现出若干显著特征，其核心在于为自动定理证明中的策略调度提供结构化监督信号。数据集包含16种战术的优先级标签，涵盖环运算、线性算术、非线性和正性证明等多种推理机制。数据分布呈现高度不平衡性，正样本比例仅为2.93%，这反映了自动证明任务的固有难度。不同配置的解决率存在明显差异，从DEFAULT配置的1.45%到DSP_PLUS配置的4.83%，为研究策略组合的有效性提供了天然对比。每个样本均包含唯一标识符、形式化陈述、配置名称、二值标签及完整的优先级向量，形成了多维度、可追溯的数据结构。

使用方法

该数据集主要服务于定理自动证明与强化学习领域的研究与应用。使用者可将其用于训练和评估策略选择模型，通过学习优先级向量与证明结果之间的映射关系，优化Aesop战术的配置。在具体应用中，研究人员可将形式化陈述与配置名称作为输入特征，将is_positive标签作为训练目标，构建分类或排序模型。数据集的三种配置变体允许进行消融实验，以探究不同战术组合对证明成功率的影响。此外，优先级向量的结构化表示为设计可解释的推理系统提供了便利，支持从数据中归纳出有效的战术调度启发式规则。

背景与挑战

背景概述

NuminaMath-LEAN-Filterd数据集诞生于形式化数学与自动化定理证明领域的前沿探索中，由专注于交互式定理证明器Lean 4及Aesop自动化策略配置的研究团队构建。该数据集的核心研究问题聚焦于如何通过数据驱动的方法，优化定理证明过程中自动化策略的优先级配置，从而提升证明搜索的效率和成功率。其构建基于大量形式化数学定理陈述，通过标注不同策略配置下的证明结果，为机器学习模型，特别是强化学习算法，提供了关键的训练与评估基准。这一工作显著推动了定理证明自动化从依赖专家经验向数据智能决策的范式转变，对增强证明助理的实用性与可访问性具有深远影响。

当前挑战

该数据集旨在应对自动化定理证明中策略选择与配置优化的核心挑战。定理证明空间通常具有组合爆炸性，且不同数学领域所需的推理策略差异显著，使得设计通用、高效的自动化策略配置极为困难。在构建过程中，挑战主要源于数据生成与标注的复杂性：需要基于Lean 4代码库生成海量形式化定理陈述，并针对多种预定义的Aesop策略配置（如DEFAULT、EXPERT、DSP_PLUS）运行证明搜索以确定其有效性，这一过程计算开销巨大。同时，数据集中正样本（证明成功）比例极低（约2.93%），导致了严重的类别不平衡问题，这为后续训练能够稳健学习策略优先级的机器学习模型带来了显著困难。

常用场景

解决学术问题

该数据集有效解决了自动定理证明中策略选择与优先级调度的核心学术问题。传统证明系统常依赖固定策略，难以适应多样化的定理结构；NuminaMath-LEAN-Filterd通过标注16种战术的优先级水平，为机器学习模型提供了结构化训练数据，使系统能够学习何时应用环化简、线性算术或非线性能量算法等特定战术。这不仅降低了证明搜索的复杂度，还推动了可解释AI在形式化数学中的应用，为定理证明的自动化与智能化奠定了数据基础。

衍生相关工作

围绕该数据集衍生的经典工作包括基于强化学习的定理证明器训练框架，如将优先级标注作为奖励信号，引导模型学习策略配置；同时，研究者开发了多配置对比分析工具，用于评估不同战术组合在复杂定理上的泛化能力。这些工作进一步催生了针对形式化数学的迁移学习模型，能够将训练成果应用于其他证明助手如Coq或Isabelle，推动了跨平台自动化证明技术的协同发展。