Kimina-Prover - 月之暗面联合 Numina 推出的数学定理证明模型

Kimina-Prover是什么

Kimina-Prover 是月之暗面跟 Numina 团队合作做的大型数学定理证明模型。训练靠大规模强化学习，推理方式尽量贴近人，最后在 Lean 4 里把定理严谨地证出来。它有个“形式化推理模式”，推理中间会穿插非形式化的想法和 Lean 4 代码片段，相当于把人的解题策略搬了进来。miniF2F 基准测试里它拿到80.7%，比此前最佳水平高出10.6%，是个新高。模型越大、算力越多，性能涨得越明显，样本效率高，扩展性也不错。1.5B和7B参数版本已经开源。

Kimina-Prover的主要功能

• 基于强化学习：第一个用大规模强化学习训出来的大型形式化推理模型，推理像人，证明落在 Lean 4 代码上，严谨性有保证。
• 高效推理模式：用的是叫“形式化推理模式”的结构化推理，中间夹着非形式化的推想和对应的 Lean 4 代码片段，人的解题策略就是这么被模拟出来的。
• 样本效率高：采样次数不多也能出不错的结果，算力加上去，性能涨得也快。
• 模型规模与性能正相关：以前的神经定理证明器不是这样，Kimina-Prover 的规模一大，性能就跟着明显往上走。

Kimina-Prover的技术原理

• 自动形式化：问题集要够杂，所以研究人员专门训了一个模型，把自然语言写的问题陈述自动翻成 Lean 4 代码，末尾留一个占位符的证明。
• 强化学习训练：监督微调（SFT）之后，再靠强化学习把形式化证明能力往上推。每轮迭代从问题集里抽一批题，各生成几个候选解法，交给 Lean 编译器验证对不对。

Kimina-Prover的性能表现

• 基准测试成绩：miniF2F 基准上拿到 80.7%，比此前的最佳水平（SOTA）模型高 10.6%，刷新了记录。
• 与通用大模型对比：miniF2F 以及它的子集（IMO、AIME 这些）上，Kimina-Prover 比 OpenAI 的 o3、Gemini 2.5 Pro 这类通用推理模型强出一截。

Kimina-Prover的项目地址

• Github仓库：https://github.com/MoonshotAI/Kimina-Prover-Preview/tree/master
• HuggingFace模型库：https://huggingface.co/collections/AI-MO/kimina-prover-preview
• arXiv技术论文：https://arxiv.org/pdf/2504.11354

Kimina-Prover的应用场景

• 科研辅助：数学研究里它有用处：复杂的定理可以让它先验一遍，顺带给出严谨的证明过程。
• 软件测试：软件开发时能拿来验逻辑。把算法和逻辑写成数学定理的形式，再看这些定理成立不成立，可靠性多少有点底。
• 算法验证：AI 和机器学习这边，算法对不对、靠不靠得住可以拿它验，至少在理论上先站得住。
• 风险评估：金融里的风险评估模型，数学基础可以先过它一遍，准确性和可靠性才谈得上。
• 工程设计验证：工程设计里，设计背后的数学模型和公式能验。建筑结构、机械设计这些方向，稳定性和安全性都能查。