Kimina-Prover-RL：面向Lean 4定理证明的开源强化学习

概述

Kimina-Prover-RL是一个开源训练流程，旨在教会大型语言模型解决Lean 4中的形式化证明目标。通过采用受DeepSeek-R1启发的结构化推理-生成范式，该系统强制模型将规划与执行分离。此版本包含与Verl框架兼容的训练配方，以及两个新模型：Kimina-Prover-RL-1.7B（在MiniF2F基准上Pass@32为76.63%）和Kimina-Prover-RL-0.6B（在MiniF2F基准上Pass@32为71.30%）。

训练方法

该流程利用组相对策略优化（GRPO）来训练模型生成自然语言推理轨迹，随后生成Lean 4代码。为了缓解GRPO中已知的优化偏差（这些偏差会导致人为地生成过长且不正确的输出），实现采用了DrGRPO，它使用一个全局常数对token级损失进行归一化。

训练架构的关键组件包括：

• 格式奖励： 严格检查输出是否具有特定结构：一个思考...响应块和一个lean4代码块。格式错误的输出将获得零奖励。额外的检查会惩罚重复推理、幻觉策略以及推理与代码之间缺乏语义对齐的情况。
• 错误纠正： 该流程包含一个错误纠正机制，当证明尝试失败时，模型会被提示修改其先前的推理和代码。这允许模型在多轮交互中从Lean 4的反馈中学习。
• 高吞吐量验证： 为了处理证明检查的规模，系统使用kimina-lean-server，这是一个支持并行证明验证的开源服务器，通过kimina-client Python包进行访问。

数据集与配置

模型在Kimina-Prover-Promptset上进行训练，这是NuminaMath-LEAN的一个精选子集。数据集经过处理以移除“简单”问题（历史胜率>0.5），使用Gemini生成变体以增加多样性，并复制困难问题以增加其在训练中的权重。

训练配置针对8-GPU设置进行了优化，微调AI-MO/Kimina-Prover-Distill-1.7B模型（基于Qwen/Qwen3-1.7B）。该过程涉及每步获取256个样本，其中一半指定为错误纠正样本，并为每个样本生成8个rollout。

性能结果

训练流程在准确性和结构遵循性方面随时间持续改进。在8块H100 GPU上训练48小时后，1.7B模型在第85步时准确率提升了4个百分点。这些模型在MiniF2F上为其各自的大小类别设立了新的最先进基准：

模型	Pass@32	带错误修复的Pass@32
AI-MO/Kimina-Prover-RL-1.7B	76.23%	77.87%
AI-MO/Kimina-Prover-RL-0.6B	71.30%	不适用

随着训练的进行，格式错误的频率降低，输出的平均token长度增加，这反映了模型在开发更结构化、更全面的推理轨迹方面的进步。