PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, Jia Li

arXiv:2504.11354v1cs.AI

TL;DR

Neural theorem provers must connect informal mathematical reasoning with formal Lean proofs, a challenge existing approaches have addressed with proof-step generation and external search. Kimina-Prover uses reinforcement learning with a structured formal reasoning pattern for internal, iterative proof exploration. It reaches 80.7% on miniF2F at pass@8192 and reports scaling with model size.

  • Problem

    Existing formal theorem-proving approaches commonly generate proof steps or structures and couple language models with search, while alignment between informal reasoning and formal proofs remains challenging.

  • Method

    Kimina-Prover combines autoformalization, supervised fine-tuning, and large-scale reinforcement learning with a formal reasoning pattern that intersperses informal reasoning and Lean 4 code.

  • Results

    80.7% with pass@8192 gives Kimina-Prover state-of-the-art performance on the miniF2F benchmark.

  • Takeaways & Limitations

    The model demonstrates high sample efficiency, effective scaling with sampling budget and model size, and more explainable reasoning than search-based provers.

Abstract

from arXiv · show

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

1 Introduction

Kimina-Prover introduces reasoning-driven exploration for Lean 4 theorem proving, using large-scale reinforcement learning and structured reasoning patterns instead of external search algorithms. It reports state-of-the-art miniF2F performance and scaling with model size.

  • The model uses internal reasoning capabilities to iteratively generate and refine Lean 4 proof steps without external search algorithms.Its structured reasoning patterns are designed to emulate human problem-solving strategies.
  • Kimina-Prover pioneers large-scale reinforcement learning to elicit long chain-of-thought reasoning for theorem proving.
  • Performance improves as LLM size increases, showing a scaling effect not observed in previous neural theorem-proving systems.
  • 80.7% with pass@8192 establishes Kimina-Prover’s state-of-the-art result on miniF2F, surpassing BFS Prover’s 72.95%.

2 Methodology

The methodology aligns informal mathematical reasoning with Lean 4 code through a formal reasoning pattern, then trains the model with supervised fine-tuning and reinforcement learning. The pipeline uses compiler verification, format filtering, and stabilization measures to refine proof generation.

  • Data construction: Autoformalization creates syntactically valid Lean 4 problems with placeholder proofs to supply a large formal training set.This addresses the cost and time required for manual dataset construction.
  • Formal Reasoning Pattern: The formal reasoning pattern intersperses informal reasoning with Lean 4 snippets inside thinking blocks and aligns most snippets with the final proof.The pattern is intended to address misalignment between informal mathematical reasoning and formal proofs.
  • Formal Reasoning Pattern: The formal reasoning pattern improves explainability by exposing the model’s thinking block, including failure modes and an educational view of proof generation.
  • Supervised fine-tuning: A minimal supervised fine-tuning stage uses about 20K synthesized olympiad-style examples combining natural-language and Lean 4 proofs.
  • Supervised fine-tuning: Informal mathematical thinking data from Kimi k1.5 is mixed into SFT to strengthen informal reasoning capabilities.
  • Reinforcement learning: Reinforcement learning samples N = 1000 problems and k = 8 candidate solutions per problem, then verifies final Lean 4 code with the compiler for binary rewards.
  • Reinforcement learning: Format filtering requires at least one tactic block covering 60% of final Lean code, while discarding negative-gradient samples with probability ω = 0.5 stabilizes training.

3 Results

Kimina-Prover achieves strong miniF2F performance, scaling with sampling budget and model size while exhibiting structured, reflective proof-generation behavior. Comparisons with general-purpose reasoning models highlight a persistent gap between informal mathematical ability and formally verifiable Lean proofs.

  • Comparison with State-of-the-Art Methods: 80.74% miniF2F-test accuracy at pass@8192 establishes Kimina-Prover as state of the art among evaluated prover systems.The model also reaches 52.94% at pass@1 and 68.85% at pass@32.
  • Comparison with State-of-the-Art Methods: Performance increases from 1.5B to 7B to 72B models, with the 72B variant gaining up to 7.87% over 7B at larger sampling budgets.The authors describe this as consistent performance scaling with model size, unlike previous formal reasoning systems.
  • Comparison with General Purpose LLMs: Kimina-Prover outperforms Gemini 2.5 Pro and o3 across miniF2F, IMO, and AIME subsets at both pass@32 and pass@8192.At pass@32, miniF2F scores are 68.85% for Kimina-Prover, 37.70% for Gemini, and 24.59% for o3.
  • Test Time Scaling in Formal Reasoning: As outputs lengthen from 2,500 to over 10,000 tokens during training, miniF2F pass@32 accuracy rises from 61.8% to nearly 69%.The trajectory is volatile, with frequent jumps and regressions, especially between 50–150 iterations.
  • Emergent human-like proof style.: After initialization and RL training, Kimina-Prover explores multiple paths, reflects, refines reasoning, and decomposes proofs into structured steps.Its proofs contain abundant have statements and these behaviors scale with problem difficulty.

4 Conclusion

The conclusion presents Kimina-Prover as a Lean 4 theorem prover trained with autoformalization, supervised fine-tuning, reinforcement learning, and a formal reasoning pattern. It reports scaling with context length and model size, state-of-the-art miniF2F performance, and several directions for improving proof quality and generation.

  • 4 Conclusion: Kimina-Prover combines autoformalization, SFT, and RL with a specific formal reasoning pattern for Lean 4 theorem proving.
  • 4 Conclusion: 80.74% miniF2F pass@8192 is achieved with modest compute while performance scales with context length and model size.The authors contrast this trend with typical tree-search provers.
  • 4 Conclusion: Future work targets proof-quality filtering, Lean compiler-feedback refinement, library search, and computation engines.

C.1 Informal Dataset

The informal dataset forms the foundation for SFT and RL, using filtering, preprocessing, human refinement, and formal proof validation to construct training prompts. Validated statements feed back into later reinforcement-learning iterations.

  • C.1 Informal Dataset: The informal data pipeline feeds curated mathematical problems into supervised fine-tuning and reinforcement learning.
  • C.1 Informal Dataset: The Numina 1.5 dataset is filtered to retain proofs or explicit numeric and symbolic outputs, excluding geometry and combinatorics.
  • C.1 Informal Dataset: Human annotators refine statements, while domain experts provide formal proofs for selected challenging examples.
  • C.1 Informal Dataset: Validated and proven formal statements enrich the SFT dataset and support continuous improvement in subsequent RL iterations.

C.2 Training Details of Kimina-Autoformalizer

Kimina-Autoformalizer is initialized on curated competition-style Lean 4 problems and improved through expert iteration that filters formalizations by compilation and semantic judgment.

  • Dataset construction: The supervised fine-tuning dataset combines formal problem pairs from PutnamBench, miniF2F, ProofNet, and Compfiles.All four sources positively contribute to downstream performance, while Mathlib data degrades performance because its content and statement style differ from competition problems.
  • Model initialization: The initialization model is a Qwen2.5-Coder-7B-Instruct variant fine-tuned to produce syntactically valid Lean 4 statements from informal descriptions.
  • Expert iteration: The structured expert iteration loop samples informal problems, generates candidate formalizations, retains compiling outputs, and adds them to the training data.A training step follows each iteration’s accepted examples.
  • Semantic filtering: A QwQ-32B judge evaluates semantic correctness after compilation, with multiple samples and unanimous voting reducing false positives while preserving most true positives.
  • Quality control: Lean 4 experts monitor outputs and refine the judge prompt because compilation alone does not guarantee semantically correct formalizations.Automated filters are also added as the proving infrastructure improves.

C.2.3 Kimina-Autoformalizer Performance

Kimina-Autoformalizer performance improves across iterations under compilation and semantic-quality filtering, while evaluation is constrained by weak Lean 4 performance from comparison models.

  • Performance: 90% one-shot compilation rate and 66% accuracy are reached after iterative autoformalizer improvement.Accuracy counts samples that both compile and are judged correct by the LLM.
  • Evaluation: The evaluation tracks Lean 4 compilation rate and autoformalization accuracy on an approximately 1,000-problem human-curated test set.
  • Benchmark caveat: Most existing comparison models struggle to generate valid Lean 4 code consistently and instead predominantly produce Lean 3 syntax.
  • Benchmark caveat: Meaningful fair benchmarks against existing approaches cannot be established because comparison models rarely produce compilable Lean 4 code.
  • Demonstrated proofs: Kimina-Prover proves the IMO problem imo_1968_p5_1, which no previous publicly released model had solved.The proof uses an auxiliary lemma, guesses the correct answer, and completes a multi-step reasoning chain.

D.2 Example Proofs of AIME Problems

The examples show Kimina-Prover handling AIME proofs through explicit algebraic, trigonometric, and arithmetic reasoning, including long Lean 4 calculation chains.

  • AIME 1991 Problem 9: The AIME 1991 Problem 9 proof derives sine and cosine values from a trigonometric identity and closes the target with algebraic manipulation.
  • AIME 1991 Problem 9: The formal theorem aims to prove ↑m.den + m.num = 44 from hypotheses involving 1 / cos x, tan x, and m.
  • AIME 1991 Problem 9: The proof uses trigonometric identities, nonzero-denominator reasoning, nonlinear arithmetic, and exact casting between rationals and reals.
  • AIME 1997 Problem 9: Kimina-Prover uses Lean 4 calc blocks for long calculations that require careful attention to the current proof context beyond automation alone.
  • Arithmetic-sequence example: For an arithmetic-sequence example, the proof derives d = 15 / 2 and computes the 21st term as 135 using linear arithmetic.

E Proof Comparison against BFS-Prover

Against BFS-Prover, Kimina-Prover’s comparison emphasizes structured proof decomposition: its have statements make proof purpose clearer than step-by-step tactic search.

  • Coverage: Kimina-Prover correctly proves all five IMO problems previously solved by BFS-Prover.The cited problems are imo_1959_p1, imo_1960_p2, imo_1962_p2, imo_1964_p2, and imo1983_p6.
  • Proof structure: Kimina-Prover decomposes proofs into have statements that produce a clear and readable logical structure.
  • Proof structure: BFS-Prover’s step-by-step tactic search makes the purpose of individual proof steps difficult to discern directly from the code.
  • Interpretation: The comparison highlights Kimina-Prover’s proof-sketch planning capabilities rather than only its ability to find individual tactics.

F.1.1 Success Case: Exploration of Multiple Informal Reasoning paths

Kimina-Prover explores multiple informal proof paths, revisits unsuccessful approaches, and ultimately formalizes a successful substitution-based proof. In the highlighted inequality example, it transforms the goal into a non-negative sum of squares and verifies the construction in Lean.

  • Informal exploration: Kimina-Prover examines several substitution and algebraic-rewriting strategies for the cyclic triangle inequality.The explored paths include Ravi substitution, direct expansion, and standard algebraic identities.
  • Reflection and refinement: The model revisits its initial approach after unsuccessful attempts and identifies a crucial simplification leading to a successful resolution.This reflects iterative exploration, backtracking, and refinement during proof search.
  • Formalization: After substitution and expansion, the target expression becomes a sum of squares multiplied by positive terms, proving non-negativity.The displayed form uses squared differences such as (y −z)^2 and positive factors such as x + y + z.
  • Formalization: The complete Lean proof concludes non-negativity after introducing variables, proving positivity, substituting, and showing equality to the sum-of-squares form.The outlined proof sequence explicitly includes these construction and verification stages.
  • Formalization: The successful construction introduces x, y, and z from the triangle inequalities, then establishes a = x + y, b = y + z, and c = z + x.Lean verifies positivity of the substituted variables and the three equalities before rewriting the goal.
  • Additional constructive example: For the number-theory example, the model fixes constructive values, classifies even n by residue modulo 6, and verifies each case in Lean.The reported solution uses small cases to formulate patterns before systematically checking the residue classes.

F.2.1 Failure Case: Incomplete Case Analysis

The failure case concerns an incomplete case analysis while proving an upper bound on x^2. Although the model checks x = ±3 and x = ±4, it does not establish that larger values are impossible.

  • Incomplete case analysis: The model checks x^2 = 9 and x^2 = 16, corresponding to x = ±3 and x = ±4, while testing whether the resulting values can satisfy the equation.These checks produce 3x^2 + 1 values of 28 and 49, respectively.
  • Attempted bound: The proof attempts to establish x^2 ≤4 from the Diophantine equation before completing the theorem.The reasoning introduces separate cases for x = 0 and x ≠0, then seeks the upper bound.
  • Formal verification: The attempted Lean proof does not close the goal after the nonlinear arithmetic steps.The trace explicitly records that the tactic fails to finish the proof.
  • Incomplete case analysis: The logical gap is that ruling out x = ±3 and x = ±4 does not address larger possible values of x.The model incorrectly treats these checked cases as resolving all cases with n > 2.
Loading 2504.11354v1…