Kimina-Prover-RL Release

Hugging Face has introduced kimina-prover-rl, an open-source training pipeline designed for formal theorem proving in Lean 4. This system utilizes a structured reasoning-then-generation paradigm inspired by DeepSeek-R1 to achieve state-of-the-art performance for open-source models in the 0.6B to 1.7B parameter range.

New State-of-the-Art Small Models

The kimina-prover-rl pipeline was used to produce two new models that set new benchmarks for their size categories on the MiniF2F benchmark:

AI-MO/Kimina-Prover-RL-1.7B: Achieves 76.63% Pass@32.
AI-MO/Kimina-Prover-RL-0.6B: Achieves 71.30% Pass@32.

Technical Architecture and Training Paradigm

Kimina-Prover-RL employs a two-stage output structure where the model first generates a natural language reasoning trace (wrapped in <think> blocks) followed by the corresponding Lean 4 code. This separation of planning and execution is designed to improve explainability, error recovery, and generalization.

Reinforcement Learning with GRPO and DrGPO

The pipeline uses Group Relative Policy Optimization (GRPO), implemented via the open-source Verl framework. To mitigate optimization bias—specifically the tendency for GRPO to produce artificially longer responses for incorrect outputs—the team utilized DrGPO, which aggregates token-level losses by normalizing with a global constant to eliminate length bias.

Reward Mechanisms

Rewards are assigned based on two primary criteria:

Verification Reward: A reward of 1 is given if the Lean code is successfully verified by the kimina-lean-server.
Format Reward: To ensure structural consistency, models receive a zero reward if the output is malformed. Format checks include:
- Verifying exactly one <think> block and one Lean 4 code block per output.
- Rejecting repetitive reasoning lines.
- Ensuring a sufficient number of non-comment lines in tactic blocks.
- Applying thresholds on comment density to penalize boilerplate.
- Measuring semantic alignment between described tactics and final code using matching scores (e.g., Intersection-over-Union).
- Penalizing unnecessarily long responses.

Error Correction Mechanism

To enhance learning from failure, the pipeline incorporates an error correction turn. When a rollout fails, the system stores the prompt, response, and Lean feedback to create a new training sample. The model is then explicitly prompted to revise its previous reasoning and code, enabling multi-turn interaction chains where the model is rewarded for successfully debugging its own output.

Data and Infrastructure

Dataset: Kimina-Prover-Promptset

The models were trained on the Kimina-Prover-Promptset, a curated subset of NuminaMath-LEAN. The dataset was refined by:

Removing easy problems (historical win rate > 0.5).
Generating problem variants using Gemini to increase diversity.
Duplicating hard problems to increase their training weight.

High-Throughput Verification

To handle the scale of parallel proof checking required during RL rollouts, the team developed the kimina-lean-server, an open-source server for parallel Lean 4 verification. A companion Python package, kimina-client, is available on PyPI for API interaction.

Performance Results

Training on 8 H100 GPUs for 48 hours showed consistent improvements. By step 85, the best@8 metric reached 70%, increasing to 74% after the error correction turn.

Comparing the RL-tuned models to their distilled predecessors on the MiniF2F benchmark:

Model	Pass@32	Pass@32 with error fixing
AI-MO/Kimina-Prover-Distill-1.7B	72.95%	75.41%
AI-MO/Kimina-Prover-RL-1.7B	76.23%	77.87%

For the 0.6B model, the pipeline improved performance from 68.85% (Distill) to 71.30% (RL) at Pass@32.