LeanPRM works by having a language model produce a natural-language proof together with a corresponding Lean formal proof in a single autoregressive pass, without any feedback from the proof assistant.
Lean proof assistant generates step-level labels to train natural-language proof verifiers.
A verifier trained on 10,634 Lean-labeled proofs outperforms human-annotated verifiers on multiple benchmarks, achieving 74.7% step-label accuracy.
Academic
Rodney Lafuente-Mercado · Salman Rahman · Jingyan Shen · James Shiffer · Saadia Gabriel · Pavel Izmailov
University of Texas at Austin · University of California, Los Angeles · New York University
Research Digest··3 min read
The authors introduce LeanPRM, a framework that uses the Lean proof assistant to generate step-level correctness labels for natural-language proofs without human annotation.
Why this paper
From University of Texas at Austin and 2 others
In one line
Lean-generated step labels train better natural-language proof verifiers than human labels, without human annotation.
What we could check
- ·No code link found
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ✓Limitations stated by the authors (2 noted)
- ✓Reports numbers on named benchmarks (3 benchmarks)
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§