在 miniF2F 测试数据集上，不同定理证明方法的性能比较。X轴表示样本预算（即尝试证明的次数，pass@8192代表尝试证明8192次中有一次做对），Y轴表示通过率。这些方法被分为两类：完整证明生成方法和树搜索方法。结果显示，Kimina-Prover 预览版在样本数量较少的情况下实现了最高的通过率，而树搜索方法通常需要更多样本才能达到类似的性能。

AI 形式化推理面临的挑战

1. 依赖外部搜索：许多方法严重依赖经典的搜索算法（如最佳优先搜索 BFS、蒙特卡洛树搜索 MCTS）来探索证明空间，这带来了巨大的计算开销和复杂性，限制了可扩展性。 

2. 难以捕捉深度推理： LLM 擅长模式匹配和序列生成，但要捕捉形式化证明中深层、结构化、甚至非线性的推理逻辑仍然困难重重。 

3. 缺乏模型规模效应： 以往针对形式化数学的神经定理证明器，其性能提升往往不随模型规模的增大而显著增长，这表明模型利用更大参数空间进行复杂推理的能力受限。

Kimina-Prover 的探索之路

为了克服传统方法的局限，Kimina-Prover 采用了新的路径，其核心在于将大规模强化学习（RL）与我们设计的“形式化推理模式”（Formal Reasoning Pattern）深度结合，用以驱动模型自身的内部推理能力。

左侧为 Formal Reasoning Pattern 示意图，右侧为 Formal RL pipeline 示意图

1. 强化学习优化内部策略，实现隐式探索：我们没有将 LLM 仅仅作为外部搜索算法的启发式函数，而是利用强化学习直接训练模型生成完整证明（包含思考过程和最终代码）的内部“策略”。这个被优化的策略使得模型能够在生成 token 的过程中，隐式地探索庞大的证明空间，自主地导航推理路径。这与传统方法依赖外部算法构建和遍历显式搜索树形成了鲜明对比，极大地降低了计算开销，并赋予了模型更灵活、更接近人类直觉的探索方式。

2. 基于最终结果的奖励信号：强化学习的训练过程是目标导向的。模型生成的每个候选证明都会被发送到 Lean 服务器（作为环境）进行严格验证。只有完全正确、能通过编译的证明才能获得正奖励（reward=1），其余则为零。这种清晰、来自最终目标的奖励信号，驱动模型学习那些真正能够导向成功证明的推理路径和代码生成模式。

3. 克服训练挑战，保证学习效率与稳定： 在形式化证明这样结构要求严格的领域应用 RL 并非易事。为解决“格式崩溃”等问题并保证训练稳定，我们实施了关键策略：a) 对生成的样本进行严格的格式过滤；b) 结合关于非形式化数学的混合训练数据；c) 在 RL 优化中引入 KL 散度约束，使得模型在学习新知识的同时不会偏离初始习得的有效模式。

4. 自动化构建大规模训练数据：为了支持 RL 训练对大量多样化问题的需求，我们开发了 Kimina-Autoformalizer-7B 模型，用于自动将自然语言数学问题转化为 Lean 4 的形式化描述，构建了大规模、多样化的训练问题集，为 RL 的有效学习奠定了坚实的基础。

初步研究成果与关键洞察

1. MiniF2F 基准新 SOTA： Kimina-Prover 在权威的 miniF2F 形式化数学基准测试中，以 pass@8192 的采样预算达到了 80.7% 的通过率，显著超越了之前的最佳结果（BFS Prover 的 72.95%）。

2. 卓越的样本效率： 得益于独特的推理模式和 RL 训练，Kimina-Prover 展现出极高的样本效率。即使在极少采样次数下（如 pass@1 达到 52.94%），它也能取得有竞争力的结果，并且随着采样预算的增加，性能有效扩展。（见下图）

不同尺寸 Kimina-Prover 模型的性能扩展情况。

4. 形式化数学推理显著优于通用大模型： 与顶尖的通用推理大模型（如 OpenAI o3-mini 和 Gemini 2.5 Pro）相比，Kimina-Prover 在形式化数学任务上展现出压倒性优势。后者虽然在非形式化数学解题上表现良好，但在生成严格、可验证的 Lean 证明时往往会失败或产生幻觉。Kimina-Prover 则能稳定生成形式正确、可通过 Lean 编译器检查的证明。

研究发现，Kimina-Prover 的性能能够随着模型规模和上下文长度的增加而显著扩展（Scalability），初步验证了 “基于推理的神经证明器” (reasoning-enabled neural provers) 的潜力。也就是说，不再仅仅依赖外部搜索，而是通过强化学习等方式激发和引导模型自身的推理能力，是构建更强大、更高效形式化系统的可行方向。

此外，Kimina-Prover 的思考过程具有很高的可解释性，用户可以查看模型是如何一步步推导出证明的，这为理解模型行为、诊断失败原因提供了便利，也使其具备成为数学教育辅助工具的潜力。

开放研究与未来计划

我们坚信开放研究的力量。为此，我们和 Numina 合作开源了 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

展望未来，我们计划继续提升证明的质量和效率，例如通过过滤掉过度依赖高级自动化策略（tactics）的输出、利用 Lean 编译器反馈进行迭代式错误修正、集成外部工具（如知识库检索、计算引擎）等。

Kimina-Prover 预览版是我们在探索大模型推理能力道路上的重要一步。我们相信，这种在严格的形式系统中锤炼出的深度结构化理解和严谨推理能力，未来将可能迁移并增强 AI 在非形式化数学问题解决，甚至更广泛的复杂推理任务上的表现，从而真正连接起形式逻辑与人类直觉。这种结合了大规模强化学习和类人推理模式的方法，将为自动化推理乃至通用人工智能（AGI）的发展开辟新思路。

↓了解更多 Kimi 研究项目