Kimina-Prover：在大规模形式推理模型上应用测试时强化学习搜索

Hugging Face 已发布 Kimina-Prover-72B，这是一款基于 Qwen2.5-72B、通过 Kimi k1.5 RL 流水线训练的最先进形式定理证明模型。通过引入测试时强化学习（Test-Time Reinforcement Learning，TTRL）搜索框架以及集成的错误修复机制，模型在 miniF2F 基准上实现了创纪录的 92.2% 通过率。

除了 72B 主力模型外，还提供了两个蒸馏变体：Kimina-Prover-Distill-8B（基于 Qwen3-8B）和 Kimina-Prover-Distill-1.7B（基于 Qwen3-1.7B）。

在 miniF2F 上的最新性能

Kimina-Prover-72B 在多个采样预算下均超越了之前的形式推理模型。根据提供的基准测试，模型在 pass@1 上达到 63.9%，在 pass@32 上达到 84.0%，在 pass@1024 上达到 87.7%。当完整的 TTRL 搜索框架被应用时，整体通过率提升至 92.2%。

模型	pass@1	pass@32	pass@1024
Kimina-Prover-1.7B	46.7	73.4	—
DSP+	52.5	71.3	80.7
DeepSeek-Prover-V2-7B	58.6	75.6	79.9
Kimina-Prover-8B	61.1	78.3	—
DeepSeek-Prover-V2-671B	61.9	82.4	86.6
Kimina-Prover-72B	63.9	84.0	87.7

测试时强化学习（TTRL）搜索

为了解决需要长时程推理的复杂问题，Kimina-Prover 采用了 TTRL 搜索框架，使模型能够自主发现、组合并复用中间引理。

引理启用模式

在 RL 训练期间，模型会接触到一种 “引理启用模式”，即随机选取一到三个形式引理并将其前置到问题上下文中。为确保模型真正使用这些引理，采用了基于偏好的奖励塑形策略：利用提供的引理的解答会获得更高奖励，而忽略它们的解答则会被惩罚。该策略使引理利用率达到 30%–40%。

递归搜索与过滤

TTRL 通过以下机制从随机探索转向策略搜索：

动态打分：系统为每个候选引理维护一个 “引理利用得分”。在每轮 RL 迭代中，60% 的输入使用得分最高的引理，40% 的输入使用随机引理以鼓励探索。
剪枝：在 50 次尝试后，若引理的利用得分未达到 $ au=0.10$，则将其移除。
递归分解：如果在 $N=128$ 次尝试后仍未解决某个定理或引理，系统会生成新的候选子引理，递归地将问题拆解为更小的子问题。
否定过滤：为防止模型利用逻辑不一致的引理，系统会尝试证明每个新引理的否定；若否定可证，则该引理被丢弃。

集成错误修复能力

Kimina-Prover 能够解析 Lean 4 错误信息并提出针对性的修复方案，这比从头重新生成证明更具样本效率。

SFT 数据与批量失败回放

由于通用大语言模型在处理 Lean 错误信息时表现不佳，团队构建了一个专门的监督微调（Supervised Fine‑Tuning，SFT）数据集，包含三元组：(错误证明, Lean 反馈, 正确证明)。该数据集还通过 Claude 3.7 Sonnet 生成的推理链进行增强。

为稳定训练，团队实现了 批量失败回放 策略。不是在出现错误后立即纠正，而是将第 $N$ 轮的失败尝试收集起来，在第 $N+1$ 轮与标准问题混合使用，从而确保模型持续接触错误纠正任务。

效率提升

错误修复在固定计算预算下显著提升成功率。在对 59 道困难 MiniF2F 题目的测试中，采用 “16+16 尝试‑修复” 策略（16 次初始尝试 + 16 次纠正）实现了 35.6% 的成功率，而使用 32 次独立尝试的 “32×1 暴力” 策略仅为 28.8%。

其他技术增强

连续预训练（Continuous Pre‑training，CPT）：模型在一个 60 亿 token 的数据集上进行 CPT，其中包括 2.6 亿来自 GitHub 的 token 和 55 亿经过编译器验证的 rollout 数据。
随机证明截断增强：为了利用人工标注的证明，团队使用 “Proof truncation”（删除证明结尾）和 “Proof infilling”（用 sorry 替换内部块）来教会模型完成并填补逻辑空缺。
提示集策划：训练集被精炼至约 9 万个面向竞赛的问题，使用动态过滤去除变得过于简单的问题，并对仍然过难的问题进行分解。
非证明问题求解：模型能够处理需要给出最终答案的问题，先推导出答案，再生成形式化证明进行佐证。