AI-MO/Kimina-Prover-Promptset
收藏Hugging Face2025-08-13 更新2025-09-13 收录
下载链接：
https://hf-mirror.com/datasets/AI-MO/Kimina-Prover-Promptset
下载链接
链接失效反馈官方服务：
资源简介：
Kimina-Prover-Promptset是一个从NuminaMath-LEAN数据集中精选出来的子集，专为强化学习（RL）训练Lean 4的定理证明器设计。这个子集包含的问题数量较少，但难度较高。数据集通过移除简单问题、生成问题变体和复制难题来创建，以提供高价值的挑战性问题，用于改进Lean 4定理证明模型。
Kimina-Prover-Promptset is a curated subset of NuminaMath-LEAN, designed for reinforcement learning (RL) training of formal theorem provers in Lean 4. This subset contains fewer problems but with higher difficulty. The dataset is created by removing simple problems, generating variants of existing problems, and duplicating hard problems to provide high-value challenging problems for improving Lean 4 theorem proving models.
提供机构：
AI-MO
