Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
Hugging Face has released Kimina-Prover-72B, a state-of-the-art formal theorem proving model based on Qwen2.5-72B and trained via the Kimi k1.5 RL pipeline. By introducing a Test-Time Reinforcement Learning (TTRL) search framework and an integrated error-fixing mechanism, the model achieves a record 92.2% pass rate on the miniF2F benchmark.
Alongside the 72B flagship model, two distilled variants are available: Kimina-Prover-Distill-8B (based on Qwen3-8B) and Kimina-Prover-Distill-1.7B (based on Qwen3-1.7B).
State-of-the-Art Performance on miniF2F
Kimina-Prover-72B outperforms previous formal reasoning models across multiple sampling budgets. According to the provided benchmarks, the model achieves a pass@1 of 63.9%, a pass@32 of 84.0%, and a pass@1024 of 87.7%. When the full TTRL search framework is applied, the pass rate increases to 92.2%.
| 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 |
Test-Time Reinforcement Learning (TTRL) Search
To solve complex problems requiring long-horizon reasoning, Kimina-Prover utilizes a TTRL search framework that allows the model to autonomously discover, combine, and reuse intermediate lemmas.
Lemma-Enabled Pattern
During RL training, the model is exposed to a "lemma-enabled pattern" where a random subset of one to three formal lemmas is prepended to the problem context. To ensure the model actually uses these lemmas, a preference-based reward shaping strategy is employed: solutions that leverage provided lemmas receive higher rewards, while those that ignore them are penalized. This resulted in a lemma utilization rate of 30–40%.
Recursive Search and Filtering
TTRL transitions from random exploration to a strategic search through the following mechanisms:
- Dynamic Scoring: The system tracks a "lemma utilization score" for each candidate lemma. In each RL iteration, 60% of inputs use top-ranking lemmas, while 40% include random lemmas to encourage exploration.
- Pruning: Lemmas that fail to achieve a utilization score of $\tau=0.10$ after 50 attempts are removed.
- Recursive Decomposition: If a theorem or lemma remains unsolved after $N=128$ attempts, the system generates new candidate sublemmas, recursively decomposing the problem into smaller subproblems.
- Negation Filtering: To prevent the model from exploiting logically inconsistent lemmas, the system attempts to prove the negation of every new lemma. If the negation is provable, the lemma is discarded.
Integrated Error-Fixing Capability
Kimina-Prover can interpret Lean 4 error messages and propose targeted fixes, which is more sample-efficient than regenerating proofs from scratch.
SFT Data and Batched Failure Replay
Because general LLMs struggle with Lean error messages, the team created a specialized Supervised Fine-Tuning (SFT) dataset consisting of triplets: (incorrect proof, Lean feedback, correct proof). This was augmented with reasoning chains generated by Claude 3.7 Sonnet.
To stabilize training, the team implemented a Batched Failure Replay strategy. Instead of immediate correction, failed attempts from iteration $N$ are collected and mixed with standard problems in iteration $N+1$, ensuring the model has consistent exposure to error-correction tasks.
Efficiency Gains
Error-fixing significantly improves success rates under fixed computational budgets. In a test of 59 difficult MiniF2F problems, a "16+16 attempt-and-fix" strategy (16 initial attempts + 16 corrections) achieved a 35.6% success rate, compared to only 28.8% for a "32x1 brute-force" strategy using 32 independent attempts.
Additional Technical Enhancements
- Continuous Pre-training (CPT): The model underwent CPT on a 6-billion-token dataset, including 260M tokens from GitHub and 5.5B tokens of compiler-validated rollout data.
- Random Proof Cut Augmentation: To utilize human-annotated proofs, the team used "Proof truncation" (removing the end of a proof) and "Proof infilling" (replacing internal blocks with
sorry) to teach the model to complete and bridge logical gaps. - Prompt Set Curation: The training set was refined to approximately 90K competition-focused problems, using dynamic filtering to remove problems that became too easy and decomposing those that remained too difficult.
- Non-proof Problem Solving: The model can handle problems requiring a final answer by first deducing the answer and then generating a formal proof to justify it.