云上速融 Kimi新模型数学反超DeepSeek！北大校友刘征瀛等领衔

Kimi 新模型数学超越 DeepSeek 了！云上速融

在定理证明这块，即便模型参数 72B 也能超越 DeepSeek-Prover-V2 的 671B 版本，实现 SOTA。

这一新模型来自 Numina 组织和 Kimi 团队联合打造，前者曾在 AI-MO 竞赛中荣获进步一等奖，陶哲轩亲自为他们颁奖。

有意思的是，这俩 AGI 团队不是第一次交手。

两个月前 DeepSeek 刚发布了 DeepSeek-Prover V2 版本，然后直接在普特南测试上将记录刷新到49 道。

当时第一名正好是 Kimina-Prover，而它只能做出 10 道题。

现在 Numina 组织和 Kimi 团队这边，再次又在 miniF2F-test 胜了一筹。

双方真是，打得有来有回的 ~

此次模型是基于 Qwen2.5-72B 打造、采用 Kimi k1.5 强化学习训练流程打造。

主要有两大技术创新，分别是提出了一种可训练的代理证明框架；还提出了一种有针对性的错误修复方法。

新模型还有两个精简版本：Kimina-Prover-Distill-8B 和 1.7B，他们分别基于 Qwen3-8B 和 Qwen3-1.7B。

官方有 Demo 可以体验 ~

Kimi 定理证明模型超越 DeepSeek

那就来看看这次 Kimi 定理证明模型是如何超过 DeepSeek 的吧。

据他们介绍，主要有两大技术创新。

首先是引入测试时强化学习（TTRL）搜索框架。

此前他们已经验证推理范式的可行性。其结构化的推理模式可以实现高效的证明搜索，并模拟了类似人类的问题解决策略。

但是单步推理对于解决需要长篇、多阶段证明的复杂问题仍然不足。

新的框架能让模型自主发现、组合和复用多个中间引理，通过将难题分解为可重用的子组件，支持更深层次、更长远的推理。

△IMO 1969 p2 证明依赖关系图

它主要包括三个部分：强化学习训练、子引理生成和否定过滤云上速融。

子引理生成并形式化后，通过动态评分和剪枝集成到训练循环中。否定过滤器通过丢弃无效引理来确保逻辑一致性。

TTRL 搜索的一个关键要素是引理启用模式，它允许模型识别并应用中间引理作为其证明构建过程的一部分。

（引理，也可以叫做辅助定理，为了得到某些更好的结论而作为步骤被证明的命题）。

这种对中间结果的结构化复用显著扩展了模型的解决问题能力，使其超越了单步生成。

TTRL 的一个关键特性是递归搜索机制，搜索范围不仅限于原始定理，也适用于每个引理，这使得框架能够将问题递归地分解为更小的子问题。并行的子引理生成过程贯穿始终，每当一个定理或引理在 N = 128 次尝试后仍未找到证明时，就会生成新的候选子引理。

此外，还引入了一个否定证明过程：对于每个新生成的引理，都尝试证明其逻辑否定。如果否定语句可证明，则表明原始引理在逻辑上不一致，并立即被丢弃。此步骤确保了整个证明构建过程的可靠性和健全性。

回看近期发布的定理证明模型，他们的一个关键限制是，缺乏根据证明助手的反馈来修正证明的能力，这却是人类经常使用的能力。

为了弥补这一缺陷，他们开发了个专门的框架，将错误修复机制集成到模型中，它可以解读 Lean 的错误信息并提出有针对性的修正建议，通过迭代反馈来优化其输出，从而提高证明的可靠性和整体样本效率。

为此，他们构建了个专门用于纠错的 SFT 数据集，还设计了个批量化失败重演策略。

在 RL 的第 N 轮迭代中，系统暂不立即纠正错误，而是完整收集所有失败的证明尝试。进入第 N+1 轮迭代时，训练批次由固定数量的历史失败样本（例如 500 条）与提示集中的标准问题（例如另 500 条）共同组成。这种设计确保模型在每一步训练中都能稳定、高频地接触纠错任务，从而以数据高效的方式逐步掌握有效的错误处理能力。