Kimina-Prover-RL: Open-Source Reinforcement Learning for Lean 4 Theorem Proving

Overview

Kimina-Prover-RL is an open-source training pipeline designed to teach large language models to solve formal proof goals in Lean 4. By employing a structured reasoning-then-generation paradigm—inspired by DeepSeek-R1—the system forces models to separate planning from execution. This release includes the training recipe, compatible with the Verl framework, and two new models: Kimina-Prover-RL-1.7B (76.63% Pass@32) and Kimina-Prover-RL-0.6B (71.30% Pass@32) on the MiniF2F benchmark.

Training Methodology

The pipeline utilizes Group Relative Policy Optimization (GRPO) to train models to generate a natural language reasoning trace followed by Lean 4 code. To mitigate known optimization biases in GRPO that lead to artificially long, incorrect outputs, the implementation uses DrGRPO, which normalizes token-level losses with a global constant.

Key components of the training architecture include:

  • Format Rewards: Outputs are strictly checked for a specific structure: one <think>...</think> block and one lean4 code block. Malformed outputs receive a zero reward. Additional checks penalize repetitive reasoning, hallucinated tactics, and lack of semantic alignment between the reasoning and the code.
  • Error Correction: The pipeline includes an error correction mechanism where, upon a failed proof attempt, the model is prompted to revise its previous reasoning and code. This allows the model to learn from Lean 4 feedback in a multi-turn interaction.
  • High-Throughput Verification: To handle the scale of proof checking, the system uses kimina-lean-server, an open-source server supporting parallel proof verification, accessed via the kimina-client Python package.

Dataset and Configuration

Models are trained on the Kimina-Prover-Promptset, a curated subset of NuminaMath-LEAN. The dataset is processed to remove "easy" problems (historical win rate > 0.5), generate variants using Gemini to increase diversity, and duplicate hard problems to increase their weight during training.

The training configuration is optimized for an 8-GPU setup, fine-tuning the AI-MO/Kimina-Prover-Distill-1.7B model (based on Qwen/Qwen3-1.7B). The process involves fetching 256 samples per step, with half designated as error-correction samples, and generating 8 rollouts per sample.

Performance Results

The training pipeline demonstrates consistent improvement in accuracy and structural adherence over time. After 48 hours of training on 8 H100 GPUs, the 1.7B model achieved a 4-point accuracy gain by step 85. The models set new state-of-the-art benchmarks for their respective size categories on MiniF2F:

Model Pass@32 Pass@32 with error fixing
AI-MO/Kimina-Prover-RL-1.7B 76.23% 77.87%
AI-MO/Kimina-Prover-RL-0.6B 71.30% N/A

As training progresses, the frequency of format errors decreases, and the average token length of outputs increases, reflecting the model's development of more structured and comprehensive reasoning traces.

Sources