Kimina-Prover-RL 发布

Hugging Face 推出了 kimina-prover-rl，这是一个专为 Lean 4 形式化定理证明设计的开源训练流水线。该系统采用了受 DeepSeek-R1 启发的“先推理后生成”的结构化范式，在 0.6B 到 1.7B 参数范围内的开源模型中实现了最先进的性能。

新的 SOTA 小参数模型

kimina-prover-rl 流水线用于生成两个新模型，它们在 MiniF2F 基准测试中为同规模类别树立了新的标杆：

  • AI-MO/Kimina-Prover-RL-1.7B：实现了 76.63% Pass@32。
  • AI-MO/Kimina-Prover-RL-0.6B：实现了 71.30% Pass@32。

技术架构与训练范式

Kimina-Prover-RL 采用两阶段输出结构，模型首先生成自然语言推理过程（封装在 <think> 块中），随后生成相应的 Lean 4 代码。这种规划与执行的分离旨在提高可解释性、错误恢复能力和泛化能力。

使用 GRPO 和 DrGPO 进行强化学习

该流水线使用通过开源 Verl 框架实现的 Group Relative Policy Optimization (GRPO)。为了减轻优化偏差——特别是 GRPO 倾向于为错误输出生成人为更长的响应——团队利用了 DrGPO，它通过使用全局常量进行归一化来聚合 token 级别的损失，从而消除长度偏差。

奖励机制

奖励基于两个主要标准分配：

  1. 验证奖励：如果 Lean 代码被 kimina-lean-server 成功验证，则给予 1 分奖励。
  2. 格式奖励：为确保结构一致性，如果输出格式错误，模型将获得零分奖励。格式检查包括：
    • 验证每个输出中恰好包含一个 <think> 块和一个 Lean 4 代码块。
    • 拒绝重复的推理行。
    • 确保 tactic 块中有足够数量的非注释行。
    • 对注释密度应用阈值以惩罚模板化内容。
    • 使用匹配分数（例如 Intersection-over-Union）测量描述的 tactic 与最终代码之间的语义对齐度。
    • 惩罚不必要的长响应。

错误修正机制

为了增强从失败中学习的能力，该流水线引入了错误修正环节。当 rollout 失败时，系统会存储 prompt、响应和 Lean 反馈，以创建一个新的训练样本。随后，模型会被明确提示去修正其之前的推理和代码，从而实现多轮交互链，使模型因成功调试自己的输出而获得奖励。

数据与基础设施

数据集：Kimina-Prover-Promptset

这些模型是在 Kimina-Prover-Promptset 上训练的，这是 NuminaMath-LEAN 的一个精选子集。该数据集通过以下方式进行了优化：

  • 移除了简单问题（历史胜率 > 0.5）。
  • 使用 Gemini 生成问题变体以增加多样性。
  • 通过复制难题来增加其训练权重。

高吞吐量验证

为了处理 RL rollout 期间所需的并行证明检查规模，团队开发了 kimina-lean-server，这是一个用于并行 Lean 4 验证的开源服务器。配套的 Python 包 kimina-client 已在 PyPI 上可用，用于 API 交互。

性能结果

在 8 个 H100 GPU 上训练 48 小时后，结果显示出持续的改进。到第 85 步时，best@8 指标达到了 70%，在经过错误修正环节后增加到了 74%。

将 RL 微调后的模型与其蒸馏版本的前身在 MiniF2F 基准测试上进行对比：

Model Pass@32 Pass@32 with error fixing
AI-MO/Kimina-Prover-Distill-1.7B 72.95% 75.41%
AI-MO/Kimina-Prover-RL-1.7B 76.23% 77.87%

对于 0.6B 模型，该流水线在 Pass@32 指标上将性能从 68.85% (Distill) 提升到了 71.30% (RL)。

Sources

相关