CoChat
Sign Up
PreprintCited by 4Logic, programming, and type systemsMathematics, Computing, and Information ProcessingArtificial Intelligence Applications

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

Open access
Wang, Haiming, Unsal, Mert, Lin, Xiaohan, Baksys, Mantas, Liu, Junqi, Santos, Marco Dos, Sung, Flood, Vinyes, Marina +32 more·2025·arXiv
DOI 10.48550/arxiv.2504.11354arXiv 2504.11354
Open this paper in CoChat — free accountOpen PDF

Abstract

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

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2504.11354

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • The hybrid using KiminaProver-7b with GPT-5-mini yielded the highest compilation rates (90.1% spec, 84.5% impl) but certified almost nothing (0 spec, 1 impl), as the pipeline was bottlenecked by parsing issues.

    “This hybrid (Table 1) yielded the highest compilation rates (90.1% spec, 84.5% impl), highlighting GPT-5-mini 's fluency. However, it certified almost nothing (0 spec, 1 impl), as the pipeline was bottlenecked by these same parsing issues.”

    From CLEVER: A Curated Benchmark for Formally Verified Code Generation (2025) · cites this paper as [33]

    The paper’s Table 1 identifies a 7B Kimina-Prover model, supporting the identification of a component of the hybrid. It reports miniF2F proof-solving results, not a GPT-5-mini hybrid, the stated compilation and certification counts, or parsing issues as a bottleneck. The searches for those terms found no supporting passage. (LLM, conf=0.83)

    Experimental — accuracy not yet measured

  • GPT-5-mini with Kimina FS achieves 90.062% spec compiled, 0% spec proved, 84.472% impl compiled, 0.621% impl proved, and 0% end-to-end.

    “GPT-5-mini | FS | Kimina FS | FS | Kimina FS | 90.062% | 0% | 84.472% | 0.621% | 0%”

    From CLEVER: A Curated Benchmark for Formally Verified Code Generation (2025) · cites this paper as [33]

    Tables 1 and 2 (page unavailable in our copy) report miniF2F results for Kimina-Prover Preview and comparisons with o3-mini and Gemini, not GPT-5-mini with Kimina FS. Searches for the quoted percentages and for GPT-5-mini with specification, implementation, and end-to-end metrics found no passage addressing the claimed results. (LLM, conf=0.76)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 26

  1. Azerbayev, Zhangir et al. ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. 2023. arXiv: 2302.12433 [cs.CL]. URL: https://arxiv.org/abs/2302.12433. · arXiv
  2. DeepSeek-AI. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. 2025. arXiv: 2501.12948 [cs.CL]. URL: https://arxiv.org/abs/2501.12948. · arXiv
  3. First, Emily et al. Baldur: Whole-Proof Generation and Repair with Large Language Models. 2023. arXiv: 2303.04910 [cs.LG]. URL: https://arxiv.org/abs/2303.04910. · arXiv
  4. Huang, Yinya et al. MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data. 2024. arXiv: 2402.08957 [cs.AI]. URL: https://arxiv.org/abs/2402.08957. · arXiv
  5. Jiang, Albert Q. et al. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. 2023. arXiv: 2210.12283 [cs.AI]. URL: https://arxiv.org/abs/2210.12283. · arXiv
  6. Jiang, Albert Q., Wenda Li, and Mateja Jamnik. Multilingual Mathematical Autoformalization. 2023. arXiv: 2311. 03755 [cs.CL]. URL: https://arxiv.org/abs/2311.03755. · arXiv
  7. Kimi-Team et al. "Kimi k1.5: Scaling reinforcement learning with llms". In: arXiv preprint arXiv:2501.12599 (2025). · arXiv
  8. Lample, Guillaume et al. "HyperTree Proof Search for Neural Theorem Proving". In: Advances in Neural Information Processing Systems. Ed. by S. Koyejo et al. Vol. 35. Curran Associates, Inc., 2022, pp. 26337-26349. URL: https: //proceedings.neurips.cc/paper_files/paper/2022/file/a8901c5e85fb8e1823bbf0f755053672- Paper-Conference.pdf.
  9. Li, Yang et al. HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving. 2025. arXiv: 2412.20735 [cs.AI]. URL: https://arxiv.org/abs/2412.20735. · arXiv
  10. Lin, Haohan et al. "Lean-STaR: Learning to Interleave Thinking and Proving". In: The Thirteenth International Conference on Learning Representations. 2025. URL: https://openreview.net/forum?id=SOWZ59UyNc.
  11. Lin, Yong et al. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. 2025. arXiv: 2502. 07640 [cs.LG]. URL: https://arxiv.org/abs/2502.07640. · arXiv
  12. Moura, Leonardo de and Sebastian Ullrich. "The Lean 4 Theorem Prover and Programming Language". In: Automated Deduction -CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Berlin, Heidelberg: Springer-Verlag, 2021, pp. 625-635. ISBN: 978-3-030-79875-8. DOI: 10.1007/978- 3-030-79876-5_37. URL: https://doi.org/10.1007/978-3-030-79876-5_37. · DOI · Paper page
  13. Nipkow, Tobias, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media, 2002.
  14. Numina. Numina Lean Server: Technical Report. arXiv preprint forthcoming. 2025.
  15. OpenAI et al. OpenAI o1 System Card. 2024. arXiv: 2412.16720 [cs.AI]. URL: https://arxiv.org/abs/2412. 16720. · arXiv
  16. Polu, Stanislas et al. Formal Mathematics Statement Curriculum Learning. 2022. arXiv: 2202.01344 [cs.LG]. URL: https://arxiv.org/abs/2202.01344. · arXiv
  17. Tsoukalas, George et al. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. 2024. arXiv: 2407.11214 [cs.AI]. URL: https://arxiv.org/abs/2407.11214. · arXiv
  18. Wang, Haiming et al. "Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function". In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2023, pp. 12632-12646.
  19. Wang, Haiming, Huajian Xin, Zhengying Liu, et al. Proving Theorems Recursively. 2024. arXiv: 2405.14414 [cs.AI]. URL: https://arxiv.org/abs/2405.14414. · arXiv
  20. Wang, Haiming, Huajian Xin, Chuanyang Zheng, et al. LEGO-Prover: Neural Theorem Proving with Growing Libraries. 2023. arXiv: 2310.00656 [cs.AI]. URL: https://arxiv.org/abs/2310.00656. · arXiv
  21. Wang, Ruida et al. MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving. 2025. arXiv: 2503.03205 [cs.CL]. URL: https://arxiv.org/abs/2503.03205. · arXiv
  22. Wu, Zijian et al. InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems. 2024. arXiv: 2410.15700 [cs.AI]. URL: https://arxiv.org/abs/2410.15700. · arXiv
  23. Xin, Huajian et al. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. 2024. arXiv: 2408.08152 [cs.CL]. URL: https://arxiv.org/abs/2408.08152. · arXiv
  24. Xin, Ran et al. BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. 2025. arXiv: 2502.03438 [cs.AI]. URL: https://arxiv.org/abs/2502.03438. · arXiv
  25. Zhang, Jingyuan et al. Leanabell-Prover: Posttraining Scaling in Formal Reasoning. 2025. arXiv: 2504 . 06122 [cs.AI]. URL: https://arxiv.org/abs/2504.06122. · arXiv
  26. Zheng, Kunhao, Jesse Michael Han, and Stanislas Polu. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. 2022. arXiv: 2109.00110 [cs.AI]. URL: https://arxiv.org/abs/2109.00110. · arXiv

Cited by

Sorted by citations

Authors
Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., Lu, J., de Saxcé, H., Bailey, B., Song, C., Xiao, C., Zhang, D., Zhang, E., Pu, F., Zhu, H., Liu, J., Bayer, J., Michel, J., Yu, L., Dreyfus-Schmidt, L., Tunstall, L., Pagani, L., Machado, M., Bourigault, P., Wang, R., Polu, S., Barroyer, T., Li, W.-D., Niu, Y., Fleureau, Y., Hu, Y., Yu, Z., Wang, Z., Yang, Z., Liu, Z., & Li, J.
ORCID
Venue
arXiv
Publisher
arXiv
Published
2025
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2504.11354
arXiv
2504.11354
OpenAlex
W4416052712
Cited by
2
References
0
Citations by year
2026: 2
Type
posted content
Language
en
Open access
Licence
Locations
  • arXiv (Cornell University) (submittedVersion, cc-by-nc-nd)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Mathematics, Computing, and Information Processing
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence Applications
Keywords
large language models, formal theorem proving, Lean 4, proof generation, reinforcement learning, sample efficiency, model size scaling, formal verification, Qwen2.5

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review