摘要
arXiv:2504.11354v1 宣告类型: 新
摘要: 我们介绍了 Kimina-Prover 预览版，这是一种大型语言模型，其开创了一种新颖的推理驱动探索范式，用于形式定理证明，这一点在此次预览版中得到了展示。Kimina-Prover 通过对Qwen2.5-72B进行大规模强化学习训练，展示了在使用我们称为“形式推理模式”的结构化推理模式时在Lean 4证明生成方面的出色表现。这种方法使模型能够模仿人类在Lean中的问题解决策略，逐步生成并细化证明步骤。Kimina-Prover 在 miniF2F基准测试中达到了新的技术水平，得分率为80.7%（通过8192次）。除了基准测试性能的提升，我们的工作还提供了几个关键见解：(1) Kimina-Prover 具有高度的样本效率，在极少采样的情况下（通过1次）也能取得出色的结果，并能够随着计算预算的增加有效扩展，这源于其独特的推理模式和强化学习训练；(2) 我们展示了模型大小与性能的清晰扩展趋势，这是先前未在形式数学的神经定理证明者中观察到的；(3) 学习到的推理风格与传统搜索算法不同，显示出弥合形式验证和直观数学之间差距的潜力。我们开源了包含1.5B和7B参数的Kimina-Prover精简版本