Kimina-Prover 预览：基于强化学习的大型形式化推理模型探索

我们推出 Kimina-Prover Preview，这是一款开创性地采用新型“推理驱动探索”范式的大型语言模型，用于形式化定理证明，本版本为预览发布。Kimina-Prover 基于 Qwen2.5-72B 通过大规模强化学习管道训练而成，在 Lean 4 定理证明生成任务中展现出卓越性能，其核心在于采用了一种我们称为 形式化推理模式（formal reasoning pattern）的结构化推理框架。该方法使模型能够模拟人类在 Lean 中解决问题的策略，通过迭代生成并逐步优化证明步骤。Kimina-Prover 在 miniF2F 基准测试中达到 80.7% 的准确率（pass@8192），创下当前最先进水平。 除基准性能的显著提升外，本研究还带来了若干关键发现：（1）Kimina-Prover 具备极高的样本效率，在极低采样次数（pass@1）下即可取得优异表现，并能随着计算资源的增加实现有效扩展，这得益于其独特的推理模式与强化学习训练机制；（2）我们首次在形式数学领域的神经定理证明器中观察到模型规模与性能之间清晰的可扩展性关系；（3）模型所学习到的推理风格与传统搜索算法显著不同，展现出在形式化验证与非形式数学直觉之间建立桥梁的巨大潜力。 我们已开源 Kimina-Prover 的轻量化版本，包含 15 亿参数（1.5B）和 70 亿参数（7B）两个版本，以促进社区研究与应用发展。