Numina 与 Kimi 开源 Kimina-Prover-RL 训练管线并发布 1.7B 和 0.6B 模型

来自 Kimina Prover 的精简训练流水线，具备核心功能并完全兼容 verl。

我们很高兴推出 kimina-prover-rl，这是一个用于 Lean 4 形式化定理证明的开源训练流水线，基于受 DeepSeek-R1 启发的“先推理、后生成”结构化范式。

该训练流水线是我们用于训练 Kimina Prover 的系统的简化版本，保留了系统的关键组件，并完全兼容开源 Verl 框架。

它作为 Verl 的一个分支的一部分发布，其中包含 recipe/kimina-prover-rl 中的完整训练配方，任何人都可以复现我们的实验，或将此设置适配到自己的模型和数据集。有关设置和启动该流水线的所有信息，均可在该配方的 README 中找到。

作为该训练流水线的成果，我们发布两个模型：

AI-MO/Kimina-Prover-RL-1.7B，一个 1.7B 参数模型，在 MiniF2F 基准上达到 76.63% Pass@32——在该规模类别的开源模型中创下新的 state of the art
AI-MO/Kimina-Prover-RL-0.6B，一个 0.6B 参数模型，在 MiniF2F 基准上达到 71.30% Pass@32——同样在该规模类别的开源模型中创下新的 state of the art。

简介

kimina-prover-rl 是一个训练流水线，旨在教会大语言模型求解 Lean 4 中的形式化证明目标，采用两阶段输出结构：先输出自然语言推理轨迹，再输出对应的 Lean 代码。

这一范式受 DeepSeek-R1 启发，使模型能够将规划与执行分离，从而提升可解释性、错误恢复能力和更强的泛化能力。

为了在该推理框架下训练模型，我们采用 GRPO——一种为 LLM 量身定制的强化学习方法。Kimina-prover 训练流水线的这个开源版本使用 RL 库 Verl 实现。

在 GRPO 的 rollout 阶段，模型会为每个提示生成 N 个输出。任何输出的 Lean 代码经我们的 kimina-lean-server 使用 Lean 成功验证后，该输出会被赋予奖励 1。

该框架新增了两个主要特性：

格式检查奖励，用于教会模型组织其输出结构
错误纠正轮次，用于鼓励模型从失败信号中学习

Kimina-Client

训练期间，必须同时验证大量 Lean 4 证明候选。为高效处理这一需求，我们需要一个高吞吐量的验证系统。

为满足这一需求，Numina 和 Kimi 开发了一个名为 kimina-lean-server 的开源服务器，支持使用 Lean 4 进行大规模并行证明检查。

为简化集成，我们还提供了 kimina-client，这是一个轻量级 Python 包（可在 PyPI 上获取），为与该服务器 API 交互提供了简洁的接口。

数据集

我们使用 Kimina-Prover-Promptset 进行训练，它是 NuminaMath-LEAN 数据集的一个精选子集。

对于此训练设置，我们按如下方式过滤和预处理数据集：

移除简单问题，即历史胜率高于 0.5 的问题，以便数据集中只保留有挑战性的命题。
生成变体，使用 Gemini 生成现有问题的变体以增加多样性
复制难题以在训练期间赋予它们更高的权重

生成的数据集包含具有挑战性、高价值的问题，可用于改进 Lean 4 定理证明模型。

NuminaMath-LEAN-RL 也是用于训练 AI-MO/Kimina-Prover-RL-1.7B 和 AI-MO/Kimina-Prover-RL-0.6B 的数据集。

示例输入格式：

Think about and solve the following problems step by step in Lean 4.

# Problem:
Find all primes that are the difference of the fourth powers of two integers.

# Formal Statement:
'''lean4
import Mathlib

theorem number_theory_4487 : {p : ℕ | p.Prime ∧ ∃ a b, p = a ^ 4 - b ^ 4} = ∅ := by
'''

格式奖励

我们推理训练流程的核心思想是将 LLM 的输出结构化为两个阶段。一个思考块后跟一个 lean4 块：

一个推理块（ ... ）
一个 Lean 4 代码块

<think>
To prove the statement, we use induction on n.
The base case is trivial, and the inductive step follows by applying the hypothesis.
</think>

'''lean4
theorem my_thm : ∀ n, f n = g n := by
  induction n with
  | zero => simp
  | succ n ih => simp [ih]
'''

每次 rollout 都会经过验证，以确保遵循此格式。如果输出格式错误——例如缺少 <think> 块或代码位置错误——无论证明是否实际有效，模型都会收到零奖励。

这强制了一致性，并教会模型可靠地组织其输出。

在 kimina-prover 中，这些检查不仅仅验证 <think> 和 lean4 块的存在：

确保每个输出恰好有一个 <think>...</think> 块和一个 lean4 代码块。
拒绝包含重复推理行的输出，这通常表明存在幻觉或退化的生成。
检查思考部分内的 tactic 块是否数量足够，并包含足够的非注释行。
对注释密度（在推理和 Lean 代码中）应用阈值，以惩罚过于冗长或模板化的输出。
使用匹配分数（例如 Intersection-over-Union 或子代码覆盖率）比较块中描述的 tactic 与最终 Lean 代码之间的语义对齐。
惩罚不必要的长响应，鼓励模型更高效地使用 token，同时仍给出完整的回复

只有通过所有这些检查的生成才被视为格式良好，并能获得奖励。这种结构化过滤提高了训练稳定性，并鼓励清晰的推理。

错误纠正

为了使训练更具信息量，我们添加了一个错误纠正机制，让模型有机会修复自己失败的证明。

当 rollout 失败时（例如由于 Lean 错误或证明不正确），我们：

存储完整的提示、响应和 Lean 反馈。
创建一个新的训练样本，其中明确提示模型修改其之前的推理/代码。

这鼓励模型从失败信号中学习，因为训练期间提供了 lean 反馈。

它还支持多轮交互链，其中来自 Lean 的反馈作为提示的一部分注入，模型因成功调试自己的输出而获得奖励。

由于多轮响应可能变得很长，我们只允许一次错误修复轮次，并将错误消息限制在设定的 token 数量内。

流程概述

Understanding R1-Zero-Like Training: A Critical Perspective 这项工作声称 GRPO 中存在优化偏差，导致人为地产生更长的响应，尤其是对于不正确的输出。

我们在实验中也注意到了这种行为，因此我们使用 DrGPO 进行优化。DrGRPO 通过使用全局常数归一化来聚合 token 级损失，以消除长度偏差。

仓库中提供的配置文件适用于 8 个 GPU 的设置。

我们正在微调的模型是 AI-MO/Kimina-Prover-Distill-1.7B。该模型是 Qwen/Qwen3-1.7B 的微调版本，其冷启动数据由我们的 AI-MO/Kimina-Prover-72B 模型生成。

每一步从训练数据集中获取 256 个样本。其中一半是纠错样本。我们对每个样本生成 8 次 rollout，因此共 2048 次生成。如果使用多个节点，可以增加到 16 或 32 次 rollout。

我们每 5 个训练步评估一次模型，使用 verl 的 best@8 指标以加快验证步骤。如果使用多个节点，可以增加到 best@16 或 32。我们评估纠错轮次前后的性能。对于每个失败的回复，我们允许模型再尝试一次以修正其证明。

结果

经过几个训练步后，我们观察到性能持续提升。本节将讨论在 8 块 H100 GPU 上训练 48 小时后的训练指标。

到第 85 步时，该流程将模型的准确率提升了 4 个百分点，best@8 指标达到 70%，纠错轮次后达到 74%：

同时，我们观察到格式错误的数量在训练过程中稳步下降，表明模型正在学习生成结构有效的输出。

最后，正如 DeepSeek-R1 风格训练设置所预期的那样，模型输出的平均 token 长度随训练增加——这表明模型正在学习以更长、更结构化的推理轨迹进行推理。

训练结束后，我们使用 pass@32 在有和没有纠错的情况下评估了模型。我们能够在 MiniF2F 上将 1.7B 模型的 pass@32 性能提升超过 3%：

模型	Pass@32	带纠错的 Pass@32
AI-MO/Kimina-Prover-Distill-1.7B	72.95%	75.41%
AI-MO/Kimina-Prover-RL-1.7B	76.23%	77.87%

使用该训练流程，我们还微调了一个 0.6B 模型，将其性能提升了超过 2%。

模型	Pass@32
AI-MO/Kimina-Prover-Distill-0.6B	68.85%
AI-MO/Kimina-Prover-RL-0.6B	71.30%

结论

借助 Kimina-Prover-RL，我们提供了一个轻量但强大的强化学习流程，用于训练 Lean 4 定理证明器。

通过结合结构化推理、格式奖励和纠错，我们在 0.6B–1.7B 参数范围内的开源模型中取得了最先进的结果。

除模型外，我们还发布了 Verl 的一个分支，其中包含 recipe/kimina-prover-rl 中的完整训练配方，以便社区复现我们的结果或将流程适配到自己的数据集和模型。

我们希望此次发布能为社区在形式推理中实验强化学习训练提供坚实基础，并推动 Lean 4 中开源自动定理证明的极限。