Kimina-Prover-RL：开源Lean 4定理证明训练管道发布

Kimina-Prover-RL是一个开源训练管道，用于在Lean 4中进行形式定理证明，基于受DeepSeek-R1启发的结构化推理-生成范式。该管道是Kimina Prover系统的简化版本，保留了关键组件，并与开源Verl框架完全兼容。它作为Verl的一个分支发布，包含完整的训练配方，允许任何人复现实验或调整设置以适应自己的模型和数据集。所有设置和启动管道的信息可在配方的README中找到。作为该训练管道的结果，团队发布了两款模型：AI-MO/Kimina-Prover-RL-1.7B是一个1.7B参数模型，在MiniF2F基准测试中达到76.63% Pass@32，为该规模的开源模型设定了新的技术水平；AI-MO/Kimina-Prover-RL-0.6B是一个0.6B参数模型，在MiniF2F基准测试中达到71.30% Pass@32，同样为该规模的开源模型设定了新的技术水平。Kimina-Prover-RL训练管道旨在教导大型语言模型解决Lean 4中的形式证明目标，使用两阶段输出结构：自然语言推理轨迹后跟相应的Lean代码。这种范式使模型能够将规划与执行分离，促进可解释性、错误恢复和更强的泛化能力。为了在此推理框架下训练模型，团队应用了GRPO——一种为LLMs定制的强化学习方法。该开源版本的训练管道使用RL库Verl实现。在GRPO的推出阶段，模型为每个提示生成N个输出。任何其Lean代码通过kimina-lean-server成功验证的输出被分配奖励1。该框架添加了两个主要功能：格式检查奖励以教导模型结构化其输出，以及错误纠正回合以鼓励模型从失败信号中学习。在训练期间，需要同时验证大量Lean 4证明候选。为了高效处理，需要一个高吞吐量的验证系统。为满足这一需求，Numina和Kimi开发了一个名为kimina-lean-server的开源服务器，支持使用Lean 4进行大规模并行证明检查。为简化集成，团队还提供了kimina-client，一个轻量级Python包，提供与服务器API交互的清晰接口。训练使用Kimina-Prover-Promptset数据集，这是NuminaMath-LEAN数据集的精选子集。对于此训练设置，数据集经过过滤和预处理：移除历史胜率高于0.5的简单问题，仅保留数据集中的挑战性陈述；使用Gemini生成现有问题的变体以增加多样性；复制困难问题以提供更多训练样本。