InternLM2-StepProver
Expert iteration over 20,000+ Lean 4 Mathlib repositories combining a critic-guided best-first tree search in which Lean executes each tactic the prover proposes.
The loop
- Proposes
An 8B tactic model proposes Lean 4 proof steps conditioned on the current goal state.
- Judged by
Lean executes each tactic the prover proposes, and a trained critic network estimates the distance (number of steps) to close the remaining subgoals.
- Steers
Critic-guided best-first tree search expands open states, and completed proofs are fed back into expert iteration to retrain both prover and critic.
Headline result
Reached 65.9% pass@64 on miniF2F-test and 54.5% on ProofNet, and proved 177 PutnamBench problems in Lean 4.
What this does not prove
Requires thousands of CPU hours of Lean 4 environment interaction during expert-iteration data collection.
How it generalizes the harness
- The algorithm is the solver
- Inverted control
- A domain authority judges
- Feedback retrains the generator
- Search over a population
- An infallible formal kernel
- Intra-algorithmic surgery (inside the while-loop)
Critic-guided tree search and Lean execution of each proposed tactic drive both inference-time proof search and multi-round expert iteration.
Classification
| What it proposes | Proof tactic |
|---|---|
| Generative model | InternLM2-StepProver 8B tactic and critic models |
| Algorithmic authority | Lean 4 (executes each proposed tactic) and critic-guided best-first tree search |
| Feedback | Proof state |
| What gets updated | Search tree and model weights |
| When it runs | During training |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Original system |