LeanPRM Uses Formal Proofs to Supervise Natural-Language Mathematical Reasoning

Why proof verification is a bottleneck

Language models are increasingly capable of producing long mathematical proofs. Their fluency, however, makes it difficult to tell whether every transition is valid. Checking only a final answer is not enough for open-ended proofs, and asking people to label every step is expensive and difficult to scale. This creates a need for process supervision: training signals that identify where a proof is correct or incorrect, rather than judging only its final outcome.

LeanPRM proposes using the Lean proof assistant as an automated source of such supervision. The central idea is to connect a natural-language proof with a formal proof that can be checked mechanically.

How the framework works

• Paired generation: A model produces a natural-language proof and a corresponding Lean proof. Generation takes place without feedback from Lean, so the setup is not simply interactive formal-proof debugging.
• Step-level checking: Lean checks the formal proof and provides signals for individual steps.
• Error-type filtering: A failed formal step may reflect a syntax or formalization mismatch rather than incorrect mathematics. A second model filters these cases so that negative labels more closely represent mathematical errors.
• Human-free supervision: The resulting LeanPRM collection includes 10,634 proofs and roughly 152,000 labeled steps, with no human annotation.

Reported results

On LeanPRM-Bench, a held-out set of 200 proofs, a Qwen3-4B verifier trained on LeanPRM reaches 74.7% exact step-label accuracy. The same base model trained on PRM800K reaches 60.3%, while the reported base score is 48.2%. LeanPRM also improves best-of-N proof selection on IMO-level problems. Across four external verification benchmarks, the LeanPRM-trained verifier outperforms the PRM800K-trained version on three. The gains are reported across verifier sizes ranging from 0.6B to 8B parameters, including LeanPRM-Bench, Hard2Verify, and IMO-GradingBench.

Why it matters

The contribution is less about treating Lean as a final pass/fail judge and more about turning a formal system into a data-generation engine. A proof assistant supplies executable checks, while language models bridge informal reasoning and formal representations. This can make process-reward-model training less dependent on expensive human review and provide denser feedback for long reasoning chains.

There are also important qualifications. The approach depends on the quality of the natural-language/formal-proof pairing, and its filtering model must distinguish genuine mathematical mistakes from failures of formal expression. A Lean-accepted proof establishes validity within the formal environment; it does not automatically guarantee that the natural-language explanation is complete or faithfully aligned with the intended argument.

LeanPRM therefore should be viewed as a scalable verification-data pipeline, not a universal replacement for mathematical review. Its results nevertheless suggest that formal proof assistants can support training natural-language reasoning verifiers even when the proofs themselves are difficult for humans to inspect step by step.

Source: Hugging Face Daily Papers