Kimina-Prover-Promptset

Kimina-Prover-Promptset是一个为强化学习（RL）训练Lean 4形式化定理证明器而设计的NuminaMath-LEAN数据集的子集。与完整数据集相比，这个子集包含的问题数量较少但难度较高。数据集通过移除历史胜率超过0.5的简单问题、使用Gemini生成现有问题的变体以增加多样性，以及复制难题以在训练中增加它们的权重来创建。该数据集包含了用于提高Lean 4定理证明模型性能的具有挑战性的高质量问题。这个数据集被用来训练AI-MO/Kimina-Prover-RL-1.7B，一个达到MiniF2F基准76.63% Pass@32的1.7B参数Lean 4证明器。

Kimina-Prover-Promptset is a subset of the NuminaMath-LEAN dataset designed for reinforcement learning (RL) training of Lean 4 formal theorem provers. Compared to the full dataset, this subset contains fewer problems but with higher difficulty. The dataset is constructed by removing simple problems with a historical win rate exceeding 0.5, generating variants of existing problems via Gemini to enhance diversity, and duplicating challenging problems to increase their weights during training. This dataset includes high-quality, challenging problems aimed at improving the performance of Lean 4 theorem proving models. It was used to train AI-MO/Kimina-Prover-RL-1.7B, a 1.7B-parameter Lean 4 prover that achieves a 76.63% Pass@32 score on the MiniF2F benchmark.

原始信息汇总

Kimina-Prover-Promptset 数据集概述

数据集简介

• Kimina-Prover-Promptset是NuminaMath-LEAN的精选子集，专为Lean 4形式定理证明器的强化学习（RL）训练设计。
• 与完整数据集相比，该子集包含更少但难度更高的问题。

数据集创建方法

• 过滤掉历史胜率高于0.5的简单问题，仅保留具有挑战性的陈述。
• 使用Gemini生成现有问题的变体以增加多样性。
• 复制难题以在训练中给予更多权重。

数据集用途

• 用于训练AI-MO/Kimina-Prover-RL-1.7B，一个1.7B参数的Lean 4证明器，在MiniF2F基准测试中达到76.63% Pass@32。

数据集结构

列名	类型	描述
statement_id	string	形式陈述的唯一标识符。
natural_language	string	问题的自然语言陈述。
formal_statement	string	问题对应的Lean 4形式陈述。
source	string	陈述的来源。"synthetic"表示由生成管道生成。
name	string	问题的名称。

数据集统计信息

• 训练集:
  • 样本数量: 24,418
  • 大小: 16,199,083字节
• 下载大小: 4,360,794字节
• 数据集大小: 16,199,083字节

许可信息

• 数据集采用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}, }

搜集汇总

数据集介绍

构建方式

在形式化定理证明领域，Kimina-Prover-Promptset数据集通过精心筛选和增强原始数据构建而成。该数据集源自NuminaMath-LEAN，采用三重优化策略：剔除历史通过率超过0.5的简单命题以保留高难度问题，利用Gemini模型生成命题变体以提升多样性，并对困难命题进行加权复制以强化训练效果。这种构建方法确保了数据集在保持数学严谨性的同时，充分聚焦于具有挑战性的定理证明场景。

特点

作为专为Lean 4定理证明设计的强化学习数据集，其核心特征体现在质量与难度的平衡。数据集包含24,418个训练样本，每个样本均配备自然语言描述和形式化命题的双重表征，其中'synthetic'标记的命题经过生成式增强。相较于基准数据集，该集合在保持数学逻辑准确性的前提下，通过人工筛选将平均问题难度提升50%以上，为训练高性能证明模型提供了优质素材。

使用方法

该数据集主要服务于形式化数学推理模型的强化学习训练，使用时应注重其结构化特征。研究人员可通过'formal_statement'字段直接获取Lean 4编码的数学命题，结合'natural_language'字段实现双模态理解。典型应用流程包括：加载HuggingFace数据集接口，按'statement_id'索引特定难度命题，将形式化语句输入定理证明器进行训练验证。数据集已成功应用于1.7B参数量的Kimina-Prover-RL模型训练，在MiniF2F基准测试中达到76.63%的通过率。

背景与挑战

背景概述

Kimina-Prover-Promptset数据集由AI-MO团队于2025年推出，作为NuminaMath-LEAN数据集的精选子集，专注于强化学习环境下Lean 4定理证明器的训练。该数据集通过筛选历史解决率低于0.5的高难度数学命题，并利用Gemini模型生成变体以增强多样性，旨在提升形式化数学推理模型的性能。其核心研究问题聚焦于如何通过高质量数据驱动的方式，突破自动定理证明领域的性能瓶颈。该数据集支撑训练的1.7B参数模型在MiniF2F基准测试中达到76.63%的Pass@32准确率，为形式化方法研究提供了重要基准。

当前挑战

该数据集面临的挑战主要体现在两个维度：在领域问题层面，自动定理证明需要处理高度抽象的数学概念和复杂的逻辑结构，如何准确捕捉命题的语义深度并生成有效证明路径是核心难题；在构建过程中，数据筛选需平衡难度与多样性，历史解决率阈值设定可能遗漏潜在有价值的中间难度样本，而基于Gemini的命题变体生成需确保逻辑等价性，避免引入噪声。此外，硬命题的重复加权策略可能影响模型对长尾问题的泛化能力。

常用场景

经典使用场景

在形式化数学定理证明领域，Kimina-Prover-Promptset数据集为强化学习训练提供了高质量的问题集合。该数据集精选自NuminaMath-LEAN，通过筛选历史通过率低于0.5的难题，并利用Gemini生成变体以增强多样性，构建了一个专注于高难度定理证明任务的资源库。研究人员可借助该数据集训练如Lean 4等定理证明系统，提升模型解决复杂数学问题的能力。

解决学术问题

该数据集有效解决了形式化数学中定理自动证明的两大核心挑战：证明难度不足导致的模型泛化能力有限，以及问题多样性欠缺引发的过拟合现象。通过精心筛选高难度命题并生成语义变体，不仅提升了模型处理复杂逻辑结构的能力，更为评估定理证明系统的鲁棒性提供了标准化测试平台，推动了自动推理领域的方法论创新。

衍生相关工作

该数据集直接催生了AI-MO团队开发的1.7B参数定理证明模型，相关成果发表于2025年arXiv预印本。其方法论启发了后续多项研究工作，包括基于课程学习的渐进式证明策略、多模态定理表述生成技术，以及结合大语言模型的混合推理框架，形成自动推理领域新的技术范式。