用强化学习训练大模型，让机器像人一样逐步推理证明数学定理。
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
- 通过结构化推理模式和强化学习，模拟人类解题过程。
- 在miniF2F上达到80.7%准确率（pass@8192），刷新纪录。
- 模型小到1.5B参数仍有效，适合研究形式化证明与AI推理者。
我们提出Kimina-Prover Preview，一个基于Qwen2.5-72B大规模强化学习训练的大型语言模型，首次引入以推理驱动的探索范式用于形式化定理证明。该模型在Lean 4中采用名为“形式化推理模式”的结构化推理策略，可迭代生成并优化证明步骤，模仿人类解题方式。其在miniF2F基准上达到80.7%的准确率（pass@8192），创下新纪录。此外，模型展现出高样本效率，即使仅使用一次采样（pass@1）也能表现良好，并随计算资源增长持续提升；同时首次在神经定理证明器中观察到模型规模与性能正相关趋势。其独特的学习推理风格区别于传统搜索算法，有望弥合形式化验证与非形式数学直觉之间的差距。我们开源了1.5B和7B参数的精简版本。
原文摘要 · Abstract (English)
We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release. Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation by employing a structured reasoning pattern we term \textit{formal reasoning pattern}. This approach allows the model to emulate human problem-solving strategies in Lean, iteratively generating and refining proof steps. Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192. Beyond improved benchmark performance, our work yields several key insights: (1) Kimina-Prover exhibits high sample efficiency, delivering strong results even with minimal sampling (pass@1) and scaling effectively with computational budget, stemming from its unique reasoning pattern and RL training; (2) we demonstrate clear performance scaling with model size, a trend previously unobserved for neural theorem provers in formal mathematics; (3) the learned reasoning style, distinct from traditional search algorithms, shows potential to bridge the gap between formal verification and informal mathematical intuition. We open source distilled versions with 1.5B and 7B parameters of Kimina-Prover
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。