Kimina-Prover-72B Achieves State-of-the-Art Theorem Proving with Test-Time RL Search

Numina and the Kimi Team have announced Kimina-Prover-72B, a formal theorem-proving model trained with test-time reinforcement learning on top of Qwen2.5-72B. The release also includes two distilled variants (8B and 1.7B versions) that make the approach more accessible.

The model achieves a 92.2% pass rate on the miniF2F benchmark—surpassing prior open-source and closed systems. This represents a significant step forward in automated formal reasoning for mathematical proof construction in Lean 4.

Key Technical Innovations#

Test-Time Reinforcement Learning Search (TTRL) is the breakthrough. Rather than generating proofs in a single pass, the model recursively discovers and combines intermediate lemmas—breaking hard problems into reusable subcomponents. A preference-based reward mechanism encourages the model to strategically apply lemmas when useful, while ignoring irrelevant ones, mimicking human-like reasoning.

The system tracks a lemma utilization score within each problem's search scope. During training, it constructs multiple input variants: 60% use top-ranking lemmas (exploitation), while 40% add random lemmas alongside them (exploration). Low-performing lemmas are pruned after 50 failed attempts. Crucially, the search is recursive—each lemma maintains its own lemma library, allowing multi-layer decomposition. If a theorem or lemma fails after 128 attempts, new candidate lemmas are auto-generated.

To prevent logically unsound proofs, the system attempts to prove the negation of every newly generated lemma. If the negation is provable, the original lemma is discarded, ensuring soundness.

Error-Fixing Capability adds robustness. Rather than regenerating proofs from scratch on failure, Kimina-Prover can read Lean's error messages and propose targeted fixes. The team trained this with a specialized supervised fine-tuning dataset: triplets of (incorrect proof, feedback, correct proof), enriched with reasoning chains synthesized by Claude 3.5 Sonnet.

To make error correction effective during RL training, they developed a Batched Failure Replay strategy. Failed proofs from iteration N are collected and compose 50% of the training batch in iteration N+1, ensuring consistent exposure to error-correction tasks. In benchmarks, a 16+16 attempt-and-fix strategy (16 proof attempts, each followed by one error-fixing attempt) reached 35.6% success—outperforming 28.8% from 32 independent attempts.

Supporting Techniques#

Additional improvements include: