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