LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification

LeanPRM. Lean-Grounded Process Supervision for Natural Language Proof Verification. By Rodney Lafuente-Mercado and five others, from the University of Texas at Austin, the University of California, Los Angeles, and one other institution. Published on the thirteenth of October. No code repository is linked to it.

AI systems now write long, difficult mathematical proofs, and checking them step by step is becoming a bottleneck. A learned verifier could do that checking cheaply, but training one needs a correctness label on every step, and for open-ended proofs those labels are hard to come by. Human annotators are costly. Labels derived from final answers do not work, because proofs do not have final answers. And formalizing each proof in Lean takes expert effort. LeanPRM is a collection of step-labelled proofs built to get around all three: ten thousand six hundred and thirty-four proofs, carrying one hundred and fifty-two thousand labelled steps, with no human annotation at all.

Each entry is a natural-language proof, broken into steps, with every step marked as valid or not. Alongside it comes a held-out evaluation set of two hundred proofs, called LeanPRM-Bench, for measuring how exactly a verifier reproduces the step labels.

The labels come from the Lean proof assistant, by an indirect route. A model writes a natural-language proof together with a paired formal proof, and it does so without any feedback from Lean. Lean then checks the formal side and labels every step. Some failures, though, are only about formal syntax rather than mathematics, so a second model discards those. What remains is a set of negative labels that mark genuine errors in the mathematics.

This is for anyone training a verifier for proofs. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on LeanPRM-Bench from forty-eight point two to seventy-four point seven. The same base model trained on PRM800K reaches sixty point three. The verifier trained on LeanPRM also picks better proofs in best-of-N selection on IMO-level problems, and it beats the PRM800K-trained verifier on three of four external verification benchmarks.

The gains are not tied to one size. Training on LeanPRM improves verifiers at every size from zero point six billion to eight billion parameters, measured on LeanPRM-Bench, Hard2Verify, and IMO-GradingBench.

Because no human sits in the labelling loop, the dataset's growth is limited only by the supply of formal statements. The authors present that as a path to step-level feedback on AI-generated proofs, including the ones that are hard for people to check. The pairing is the quiet trick: Lean checks the formal twin, and its verdict is carried back to the steps written in ordinary language.