Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models

Abstract

We present Kimina-Prover, applying test-time reinforcement learning search on large formal reasoning models. This blog post details our approach and demonstrates state-of-the-art performance on formal theorem proving benchmarks.

PhD student in Computer Science, University of Cambridge