NuminaMath-LEAN

NuminaMath-LEAN是一个大规模的数学竞赛问题数据集，包含100K个用Lean 4形式化的问题，主要选自于难度较高的NuminaMath 1.5数据集，专注于IMO和USAMO等著名竞赛的问题。这个数据集是迄今为止最大的人类注释形式化陈述和证明的集合，旨在用于训练和评估自动定理证明器。

NuminaMath-LEAN is a large-scale mathematical competition problem dataset comprising 100K problems formalized in Lean 4. It is primarily sourced from the more challenging NuminaMath 1.5 dataset, focusing on problems from prominent competitions such as the International Mathematical Olympiad (IMO) and the United States of America Mathematical Olympiad (USAMO). This dataset is the largest collection of human-annotated formalized statements and proofs to date, and is designed for training and evaluating automated theorem provers.

原始信息汇总

NuminaMath-LEAN 数据集概述

数据集摘要

• NuminaMath-LEAN 是一个包含10万条数学竞赛问题的大规模数据集，使用Lean 4形式化。
• 数据来源于NuminaMath 1.5数据集的挑战性子集，聚焦于IMO和USAMO等知名竞赛问题。
• 该数据集是最大规模的人工标注形式化语句和证明集合，用于训练和评估自动定理证明器。

数据特征

• uuid: 字符串类型，唯一标识符。
• problem: 字符串类型，问题描述。
• question_type: 字符串类型，问题类型。
• answer: 字符串类型，答案。
• author: 字符串类型，形式化语句的作者（autoformalizer或human）。
• formal_statement: 字符串类型，Lean 4中的形式化语句。
• formal_ground_truth: 字符串类型，人工标注的形式化证明（仅当author == human时可用）。
• ground_truth_type: 字符串类型，标注状态（complete、with_sorry或statement）。
• formal_proof: 字符串类型，模型在RL训练中生成的形式化证明（仅在模型成功证明时可用）。
• rl_data: 结构体，包含RL训练信息：
  • n_correct_proofs: 整型，模型成功解决问题的次数。
  • n_proofs: 整型，模型尝试解决问题的次数。
  • win_rate: 浮点型，成功率（n_correct_proofs / n_proofs）。
• source: 字符串类型，问题来源。
• problem_type: 字符串类型，问题类型。
• exam: 字符串类型，考试名称。

数据拆分

• train: 包含104,155个示例，总大小为171,546,775字节。

方法

• 从NuminaMath 1.5数据集中筛选最具挑战性的部分，移除cn_k12和非数学竞赛问题。
• 过滤掉geometry和combinatorics问题，因其形式化难度较高。
• 新增olympiads-ref子集，包含IMO、IMO短列表、USAMO等竞赛问题。

兼容性

• 所有形式化内容均基于Lean 4编写，并在mathlib v4.15.0中验证。

局限性

• 部分元数据缺失（如question_type）。
• 部分参考答案提取错误。
• 部分形式化语句不准确（主要因autoformalizer的限制）。

许可信息

• 数据集采用Apache License, Version 2.0许可。

引用信息

bibtex @article{kimina_prover_2025, title = {Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning}, author = {Wang, Haiming and Unsal, Mert and Lin, Xiaohan and Baksys, Mantas and Liu, Junqi and Santos, Marco Dos and Sung, Flood and Vinyes, Marina and Ying, Zhenzhe and Zhu, Zekai and Lu, Jianqiao and Saxcé, Hugues de and Bailey, Bolton and Song, Chendong and Xiao, Chenjun and Zhang, Dehao and Zhang, Ebony and Pu, Frederick and Zhu, Han and Liu, Jiawei and Bayer, Jonas and Michel, Julien and Yu, Longhui and Dreyfus-Schmidt, Léo and Tunstall, Lewis and Pagani, Luigi and Machado, Moreira and Bourigault, Pauline and Wang, Ran and Polu, Stanislas and Barroyer, Thibaut and Li, Wen-Ding and Niu, Yazhe and Fleureau, Yann and Hu, Yangyang and Yu, Zhouliang and Wang, Zihan and Yang, Zhilin and Liu, Zhengying and Li, Jia}, year = {2025}, url = {http://arxiv.org/abs/2504.11354}, }

搜集汇总

数据集介绍

构建方式

NuminaMath-LEAN数据集的构建源于对NuminaMath 1.5数据集的精选与扩展，专注于数学竞赛领域的难题。通过剔除中小学数学题目和几何组合类问题，保留了最具挑战性的竞赛题目，如国际数学奥林匹克（IMO）和美国数学奥林匹克（USAMO）的试题。此外，数据集还新增了olympiads-ref子集，收录了来自顶级数学竞赛的题目，并对其解答和参考答案进行了严格校对。所有题目均以Lean 4语言形式化，并通过人工标注和自动形式化模型相结合的方式生成形式化陈述和证明。

特点

NuminaMath-LEAN数据集是目前规模最大的数学竞赛题目形式化集合，包含超过10万道题目，每道题目均配有形式化陈述和部分人工标注的完整证明。数据集特别标注了题目来源、作者信息以及证明的完整性状态（如complete、with_sorry等），并提供了模型在强化学习训练中的表现数据（如尝试次数和正确率）。其形式化内容基于Lean 4和mathlib v4.15.0，确保了技术兼容性，同时为自动定理证明系统的训练与评估提供了丰富资源。

使用方法

使用NuminaMath-LEAN数据集时，需确保运行环境与Lean 4及mathlib v4.15.0兼容，以避免编译错误。数据集适用于训练和评估自动定理证明模型，用户可通过分析formal_statement和formal_proof字段研究形式化证明的生成与验证。rl_data字段提供了模型在强化学习中的表现指标，便于优化算法设计。对于标注不完全的题目（如缺失question_type或存在sorry的证明），建议结合后续版本更新或人工校验以提升数据质量。

背景与挑战

背景概述

NuminaMath-LEAN数据集由AI-MO团队于2025年发布，是目前规模最大的数学竞赛问题形式化数据集，包含10万道基于Lean 4形式化语言的数学问题。该数据集源自NuminaMath 1.5的精选子集，聚焦国际数学奥林匹克（IMO）、美国数学奥林匹克（USAMO）等顶级赛事题目，旨在推动自动定理证明领域的发展。作为Kimina-Prover 72B大模型的训练基础，该数据集通过人类专家标注的形式化命题与证明，为数学推理系统的性能评估提供了重要基准。其创新性体现在将传统数学问题转化为计算机可验证的形式化表达，填补了该领域高质量标注数据的空白。

当前挑战

该数据集面临的核心挑战主要体现在两个方面：领域问题方面，数学命题的形式化转换存在语义保真难题，尤其是几何与组合数学类问题因依赖图形直觉而难以准确编码；构建过程方面，标注工作依赖专业数学家的深度参与，导致人力成本高昂且效率受限。数据质量层面存在三类突出问题：约30%的元数据缺失影响数据可用性，部分参考答案存在提取错误，自动形式化工具生成的命题约有5%存在逻辑偏差。此外，Lean 4语言环境与mathlib v4.15.0的强依赖性，也为数据集的广泛适用性设置了技术门槛。

常用场景

经典使用场景

NuminaMath-LEAN数据集在自动定理证明领域具有重要地位，其经典使用场景主要集中在训练和评估基于强化学习的定理证明模型。数据集中的数学竞赛问题经过精心筛选和形式化处理，涵盖了IMO、USAMO等顶级竞赛的题目，为研究者提供了丰富的训练样本。通过Lean 4的形式化语句和证明，研究者能够高效地验证模型的推理能力，并优化其证明生成算法。

衍生相关工作

围绕NuminaMath-LEAN数据集，已衍生出多项经典研究工作，其中最突出的是Kimina-Prover 72B模型。该模型利用数据集进行强化学习训练，展示了在自动定理证明任务上的卓越性能。此外，数据集还催生了关于形式化数学问题自动生成、证明压缩以及跨领域迁移学习的研究，进一步扩展了自动推理技术的应用边界。

数据集最近研究

最新研究方向

在形式化数学与自动定理证明领域，NuminaMath-LEAN数据集正推动着基于强化学习的大规模推理模型发展。该数据集整合了国际数学奥林匹克（IMO）等顶尖竞赛题目，其标注的正式陈述与证明为训练如Kimina-Prover等模型提供了关键支持。当前研究聚焦于提升自动形式化转换的准确性，解决几何与组合问题形式化的技术瓶颈，并通过强化学习优化证明生成的成功率。数据集特有的RL训练指标（如胜率分析）为评估模型在复杂数学推理中的动态表现提供了新维度，相关成果已被应用于改进形式验证系统的泛化能力。