LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
AuthorsRodney Lafuente-Mercado, Salman Rahman, Jingyan Shen, James Shiffer, Saadia Gabriel, Pavel Izmailov
AffiliationsUniversity of Texas at Austin · University of California, Los Angeles · New York University ✯ Equal contribution
LeanPRM uses Lean-checked formal proofs to generate scalable training labels that help AI models verify each step of mathematical proofs.
Key results
Number of natural-language proofs collected without human annotation.
Step-level labels grounded in Lean 4.
Achieved by Qwen3-4B after 500 updates; the PRM800K-trained verifier scores 60.3%.
Share of selected proofs judged correct, compared with 32.4% for random selection.
GRPO updates used for the main controlled model comparisons.
What the paper found
LeanPRM uses Lean 4 to create step-by-step supervision for natural-language mathematical proofs without human annotation. A model first writes a proof in prose alongside matching Lean steps, without seeing checker feedback; Lean identifies the first failing step, and a second model filters failures caused only by formal syntax. The resulting verifier is trained to read prose alone. The corpus contains 10,634 natural-language proofs and 152,005 labeled steps. With Qwen3-4B, 500 updates of group relative policy optimization raise exact step-label accuracy on LeanPRM-Bench to 74.7%, compared with 48.2% for the untrained model and 60.3% for a PRM800K-trained verifier. LeanPRM training improves models from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify, and IMO-GradingBench. On IMO-GradingBench, selecting among 16 candidate proofs yields a correct proof 35.9% of the time, versus 32.4% with random selection. Proof attempts were generated mainly using Anthropic’s Claude models; the study also compares its Qwen3 verifiers with PRM800K-trained models and prompted Claude and OpenAI GPT-5.6 Sol systems. The approach’s central contribution is turning formal checking into scalable supervision for informal proof verification, while filtering out formalization mistakes that could otherwise produce misleading negative labels.
Original abstract
AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.
Read the original paperMore in AI Reasoning
Browse all 45 papers →Inducing Process Supervision from Outcome-Only Reinforcement Learning
Shengda Fan, Xin Cong, Zhong Zhang, Haotian Chen, Yankai Lin
TIPS trains models to judge their own reasoning steps using only outcome feedback, avoiding the need for costly step-by-step annotations.
LEV: Thinking Fast and Deep with Looped Decision Models
Dingjie Song, Zhiling Yan, Yuxuan Zhang, Lichao Sun
LEV lets a model think longer by looping its layers, improving answers to hard questions while adapting compute to the task.
Self-Conditioning Enables Deep Sequential Reasoning in Flow Matching
Zeyang Zhang, Linxiang Gao, Meiqi Gu, Xingyan Chen, Minrui Luo, Kaifeng Lyu, Tianxing He
Self-conditioning lets flow-matching models use more sampling steps for deeper visual reasoning.