Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
Numina & Kimi Team
We're excited to announce the release of Kimina-Prover-72B, our state-of-the-art theorem proving model trained with the Kimi k1.5[1] RL pipeline based on Qwen2.5-72B [2]. Alongside it, we are also releasing two distilled variants: Kimina-Prover-Distill-8B and 1.7B (based on Qwen3-8B and Qwen3-1.7B[3] respectively).
Our key innovations include:
Test-Time Reinforcement Learning Search: A trainable agentic proving framework that enables the model to recursively discover, combine and apply multiple lemmas to construct complex proofs, building on a novel lemma-enabled pattern.
Error-Fixing Capability: Kimina-Prover can read and interpret Lean’s error messages and propose targeted fixes, demonstrating significantly higher sample efficiency compared to regenerating proofs from scratch.
These advancements enable Kimina-Prover to solve challenging mathematical problems and surpass prior methods. As shown in Figure 1, on the widely used miniF2F benchmark, Kimina-Prover achieves a state-of-the-art pass rate of 92.2%.
Introduction
We focus on automated theorem proving (ATP) in the Lean 4 language, aiming to automate the construction of formal mathematical proofs. Recent advances in neural theorem proving have significantly improved the ability of AI systems to assist with or automate this process. Notable progress includes AlphaProof[4] from Google DeepMind, which demonstrated strong performance on problems at the level of the International Mathematical Olympiad. Open-source systems such as DeepSeek-Prover-V2[5], which incorporates reinforcement learning, have also achieved state-of-the-art results. In addition, neuro-symbolic agentic approaches like DSP+[6] have shown that competitive performance is possible without large-scale training by leveraging off-the-shelf models in a modular framework.
Our earlier work of Kimina-Prover Preview[7] introduced a large language model for formal theorem proving in Lean, establishing a new performance baseline on the miniF2F benchmark. Trained with a large-scale reinforcement learning pipeline, the model adopted a reasoning-driven exploration paradigm and demonstrated that larger models can serve as stronger formal reasoners. Its structured reasoning pattern enabled efficient proof search and emulated human-like problem-solving strategies.
Following this initial success, we continued to improve the model through further iterations of reinforcement learning. However, single-step reasoning remains insufficient for solving complex problems that require long, multi-stage proofs. To address this limitation, we introduce the Test-Time Reinforcement Learning (TTRL) search framework, which enables the model to discover, combine, and reuse multiple intermediate lemmas autonomously. This framework supports deeper, long-horizon reasoning by decomposing hard problems into reusable subcomponents.
A key ingredient of TTRL search is the lemma-enabled pattern, which allows the model to identify and apply intermediate lemmas as part of its proof construction process. This structured reuse of intermediate results significantly expands the model’s problem-solving capability beyond single-step generation.
To further enhance robustness, we also integrate an error-fixing mechanism that interprets Lean’s error messages and proposes targeted corrections. This allows the model to refine its outputs through iterative feedback, improving proof reliability and overall sample efficiency.
A New State-of-the-Art
| Model | pass@1 | pass@32 | pass@1024 |
|---|---|---|---|
| Kimina-Prover-1.7B | 46.7 | 73.4 | — |
| DSP+ | 52.5 | 71.3 | 80.7 |
| DeepSeek-Prover-V2-7B | 58.6 | 75.6 | 79.9 |
| Kimina-Prover-8B | 61.1 | 78.3 | — |
| DeepSeek-Prover-V2-671B | 61.9 | 82.4 | 86.6 |
| Kimina-Prover-72B | 63.9 | 84.0 | 87.7 |
As the combination of the proposed techniques results in significant improvements in formal theorem proving performance. On the miniF2F benchmark, Kimina-Prover achieves a pass rate of 84.0% with pass@32 and 86.4% with the addition of a single round of error correction. With pass@1024, the pass rate reaches 87.7%. Applying the full Test-Time Reinforcement Learning (TTRL) search framework yields a final pass rate of 92.2%, with an estimated pass upper bound of approximately 42,000. However, this pass budget can be substantially optimized in future versions, as a large portion of the current sampling is spent on proving unhelpful or redundant lemmas.
Notably, these results indicate a shift in the scaling behavior of the prover. While earlier versions exhibited approximately linear improvements in log scale with increasing sampling budget, the current system shows diminishing returns beyond pass@1024. This suggests that further gains are less dependent on increased sampling and instead require more sophisticated search strategies, such as those introduced by TTRL.
Methodology
Lemma enabled pattern
The lemma-enabled pattern is designed to equip the model with the ability to identify and utilize useful lemmas provided in the input. To support this capability, during reinforcement learning (RL) training, a random subset of one to three formal lemmas is prepended to the problem context, exposing the prover to potentially useful intermediate results that can aid in constructing the final proof. These lemmas are prepared through a two-step pipeline: (1) a general-purpose LLM generates candidate lemmas in natural language; (2) these are then translated into formal statements using our
Kimina-Autoformalizer-7b.
Initial observations showed that the model had a low tendency to incorporate the provided lemmas. To address this, we introduced a preference-based reward shaping strategy within the RL framework. When a theorem could be proven through multiple trajectories, solutions that successfully leveraged a provided lemma were assigned a higher reward, while those that did not were penalized. This approach proved effective, increasing the lemma utilization rate to a stable 30–40% after training. Importantly, this method not only encouraged lemma usage but also promoted selectivity: the model learned to apply lemmas strategically when they were useful, while ignoring irrelevant ones, demonstrating more efficient and human-like reasoning behavior.
TTRL search
The lemma-enabled pattern allowed the model to incorporate pre-generated lemmas as intermediate steps in constructing proofs. However, we observed that randomly sampling and inserting lemmas was insufficient for solving complex problems requiring highly structured and deeply nested reasoning. To address this limitation, we developed the Test-Time Reinforcement Learning Search framework—a trainable, agentic approach that systematically organizes, filters, and composes a large set of candidate lemmas to build complete proofs. This framework transitions th