Kimina-Prover：用于形式化定理证明的测试时强化学习搜索

概述

Kimina-Prover-72B 是一款专为 Lean 4 语言设计的顶尖自动定理证明 (ATP) 模型，在 miniF2F-test 基准测试中达到了 92.2% 的通过率。通过集成测试时强化学习 (TTRL) 搜索和一种新颖的错误修复机制，该系统超越了单步推理，能够自主地将复杂的数学问题分解为可管理的子引理。

测试时强化学习 (TTRL) 搜索

TTRL 搜索框架将定理证明从随机探索转变为一种目标导向的代理过程。它利用了一种“引理启用模式”，模型被训练用于识别并将中间引理纳入其证明构建中。

TTRL 框架的关键组件包括：

  • 动态引理评分： 系统跟踪搜索范围内引理的效用，优先考虑那些频繁有助于成功证明的引理，同时修剪掉那些未达到最低利用率阈值 (τ=0.10) 的引理。
  • 递归分解： 当定理或引理在 128 次尝试后仍无法证明时，系统会触发子引理生成过程。这使得模型能够递归地将难题分解为更小、可证明的组件。
  • 逻辑稳健性： 为了防止模型利用不一致性来生成平凡证明，系统采用了“否定证明过程”。如果生成的引理的逻辑否定是可证明的，则原始引理将被视为不一致而丢弃。

错误修复与样本效率

Kimina-Prover 通过解释 Lean 的错误消息来执行迭代修正，而不是从头开始重新证明，从而提高了样本效率。团队开发了一个专门的监督微调 (SFT) 数据集，由 (错误证明, Lean 反馈, 正确证明) 三元组组成，并辅以由 Claude 3.7 Sonnet 合成的逐步推理链。

为了将其集成到强化学习循环中，团队实施了“批量失败重放”策略。通过在固定大小的先前失败案例和标准问题的集合上进行训练，模型学会了解决复杂的逻辑错误和语法错误，在同等计算预算下持续优于暴力采样策略。

模型变体与性能

除了旗舰级的 72B 参数模型外，本次发布还包括了支持多样化部署需求的蒸馏变体：

  • Kimina-Prover-72B： 基于 Qwen2.5-72B，在 miniF2F-test 上达到 92.2%。
  • Kimina-Prover-Distill-8B： 基于 Qwen3-8B。
  • Kimina-Prover-1.7B： 基于 Qwen3-1.7B。

性能数据表明，虽然早期模型随采样预算呈线性扩展，但当前系统在 pass@1024 之后表现出边际收益递减，这表明进一步的改进更多依赖于 TTRL 提供的复杂搜索策略，而非单纯的采样量。

Sources