Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
Hugging Face
Numina & Kimi released Kimina-Prover-72B, a Lean 4 theorem-proving model with a test-time RL search framework and an error-fixing mechanism, plus distilled 8B and 1.7B variants. It reports a miniF2F-test pass rate of 92.2% when using the full TTRL search framework (and 84.0% at pass@32). The results shift scaling behavior so gains beyond pass@1024 rely more on improved search strategies than on higher sampling alone.