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

Hugging Face Daily Papers Papers
process-reward-model formal-verification lean mathematical-reasoning proof-verification step-level-labels

Summary

LeanPRM提出利用Lean证明助手自动为自然语言数学证明生成步骤级正确性标签，无需人工标注即可训练过程奖励模型（PRM）。Qwen3-4B验证器在该数据上训练后，步级标签准确率从48.2提升至74.7，并在IMO级问题的最佳-of-N选择和多个外部验证基准上超越PRM800K训练的验证器。

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.
Original Article
View Cached Full Text

Cached at: 10/16/26, 07:06 PM

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

Source: https://huggingface.co/papers/2610.17697

Abstract

LeanPRM uses the Lean proof assistant to automatically generate step-level correctness labels for natural-language mathematical proofs, enabling scalable training of learned verifiers without human annotation.

AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. Alearned verifiercould 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 introduceLeanPRM, a framework that uses theLean proof assistantto createstep-level labelsfornatural-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.LeanPRMcontains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained onLeanPRMraises 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 onPRM800K. It also selects better proofs inbest-of-N selectiononIMO-level problems, and outperforms thePRM800K-trained verifier on three of four external verification benchmarks. Training onLeanPRMimproves verifiers at every size from 0.6B to 8B parameters onLeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation,LeanPRMcan 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.

View arXiv pageView PDFProject pageAdd to collection

Get this paper in your agent:

hf papers read 2610\.17697

Don’t have the latest CLI?curl \-LsSf https://hf\.co/cli/install\.sh \| bash

Models citing this paper0

No model linking this paper

Cite arxiv.org/abs/2610.17697 in a model README.md to link it from this page.

Datasets citing this paper0

No dataset linking this paper

Cite arxiv.org/abs/2610.17697 in a dataset README.md to link it from this page.

Spaces citing this paper0

No Space linking this paper

Cite arxiv.org/abs/2610.17697 in a Space README.md to link it from this page.

Collections including this paper0

No Collection including this paper

Add this paper to acollectionto link it from this page.

Similar Articles

Verifier-Grounded Agentic RL for Provably Correct Code

arXiv cs.LG

提出一种以程序验证器为奖励信号的智能体强化学习框架，通过读取验证器诊断信息（而非二元判决）并加入完整性审计，显著提升Qwen3系列模型在DafnyBench和SWE-Proof等验证基准上的正确率（最高达100%）。

LeanPolish: Verified Supervision for Lean Proof Compression

arXiv cs.LG

The paper introduces LeanPolish, a symbolic Lean 4 pipeline releasing 33k+ verified proof edits and failed attempts, showing that verified supervision can suffer from search artifacts and that iterating the symbolic compression pass beats neural hybrids on miniF2F while modestly improving whole-proof rewriting on PutnamBench.

Unsupervised Process Reward Models

Hugging Face Daily Papers

This paper proposes unsupervised Process Reward Models (uPRM) that eliminate the need for human annotations by using LLM next-token probabilities to identify erroneous reasoning steps, achieving up to 15% accuracy improvements over LLM-as-a-Judge and performing comparably to supervised PRMs as verifiers and reward signals.