月之暗面Kimi开源数学定理证明模型Kimina-Prover

 Kimi 技术团队近日发布了 Kimina-Prover 预览版的技术报告，并开源了1.5B 和7B 参数的模型蒸馏版本、用于数据生成的 Kimina-Autoformalizer-7B 模型以及修订过的 miniF2F 基准测试数据集。Kimina-Prover 是由 Numina 和 Kimi 团队联合研发的一款数学定理证明模型，它在形式化定理证明领域采用了一种新颖的、由推理驱动的探索范式，展现出极佳的性能。

Kimina-Prover 基于 Qwen2.5-72B 模型，并结合 Kimi k1.5的大规模强化学习（RL）流程进行训练。在权威的 miniF2F 形式化数学基准测试中，Kimina-Prover 预览版以更低的采样预算(pass@8192)达到了80.7% 的通过率，显著超越了之前的最佳结果:BFS Prover 的72.95%(pass@2048×2×600+)和 DeepSeek-Prover 的50.0%(pass@65536)。

形式化定理证明是数学和计算机科学领域的一个重要方向，它应用严格的数学逻辑和计算机程序来验证数学定理的正确性。然而，让 AI 掌握形式化证明极具挑战，传统方法往往难以应对复杂、需要深刻洞察力和创造力的数学问题。近年来，大语言模型（LLM）的兴起为这一领域带来了新的希望，但现有方法大多存在局限，如依赖外部搜索、难以捕捉深度推理、缺乏模型规模效应等。

为了克服这些局限，Kimina-Prover 采用了新的路径，将大规模强化学习（RL）与“形式化推理模式”深度结合，直接优化模型生成完整证明的内部“策略”。这种方法使得模型能够在生成 token 的过程中隐式地探索庞大的证明空间，自主地导航推理路径，极大地降低了计算开销，并赋予了模型更灵活、更接近人类直觉的探索方式。此外，Kimina-Prover 还引入了基于最终结果的奖励信号，强化学习的训练过程是目标导向的，只有完全正确、能通过编译的证明才能获得正奖励。

Kimina-Prover 的初步研究成果取得了显著进展。在 miniF2F 基准测试中，Kimina-Prover 达到了80.7% 的通过率，显著超越了之前的最佳结果。它还展现出极高的样本效率，即使在极少采样次数下也能取得有竞争力的结果。此外，Kimina-Prover 的性能随着模型参数规模的增大而持续提升，这是首次在形式化数学领域的神经定理证明器中观察到如此明确的规模效应。与顶尖的通用推理大模型相比，Kimina-Prover 在形式化数学任务上展现出压倒性优势，能够稳定生成形式正确、可通过 Lean 编译器检查的证明。

Kimina-Prover 的思考过程具有很高的可解释性，用户可以查看模型是如何一步步推导出证明的，这为理解模型行为、诊断失败原因提供了便利，也使其具备成为数学教育辅助工具的潜力。研究团队表示，Kimina-Prover 的性能能够随着模型规模和上下文长度的增加而显著扩展，初步验证了“基于推理的神经证明器”的潜力。这种结合了大规模强化学习和类人推理模式的方法，将为自动化推理乃至通用人工智能（AGI）的发展开辟新思路。

为了推动社区的参与和研究进展，Kimi 技术团队开源了 Kimina-Prover 的1.5B 和7B 参数的蒸馏版本，用于数据生成的 Kimina-Autoformalizer-7B 模型，以及修订过的 miniF2F 基准测试数据集。

• Arxiv 技术报告:https://arxiv.org/abs/2504.11354

• GitHub 代码库:‍https://github.com/MoonshotAI/Kimina-Prover-Preview‍

• Hugging Face 模型下载:https://huggingface.co/collections/AI-MO/kimina-prover-preview-67fb536b883d60e7ca25d7f9