Verified supervision improves compression of Lean proofs using symbolic edits
LeanPolish: Verified Supervision for Lean Proof Compression
Machine Learning
Summary
Proof assistants help people write complex math proofs on computers, but these proofs can often be very long and complicated. This paper introduces LeanPolish, a tool that uses verified small changes to improve and shorten these proofs while making sure they remain correct. The authors provide a large collection of accepted and rejected small edits to study what models learn from them. Their results show that training on these verified edits helps language models reduce proof length better than previous methods without losing correctness.
What this means in practice
- •For formal verification engineers: Improve automated proof compression tools to shorten formally verified code and proofs while keeping correctness guaranteed.
- •For software development teams using formal methods: Integrate verified editing techniques into proof assistants to generate more compact proofs during software correctness verification.
Authors
Pauline Bourigault
Abstract
Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit is correct, not that its training signal is free of search artifacts. We introduce LeanPolish, a symbolic Lean 4 pipeline that releases 33,402 accepted local edits and 65,596 same-state failed attempts, and use it to study what models learn from this supervision. First-success search admits a goal-independent rule with perfect ranking accuracy; teacher-selected evaluation sites also reward trivial deletions. Continuing menu evaluation beyond the first success removes the ordering shortcut: a trained ranker selects the best candidate on 70.1% of evaluated held-out states, versus 36.9% for the strongest frozen baseline. For compression, iterating the symbolic pass raises miniF2F savings from 19.7% to 27.5%, exceeding the neural hybrids we test there. Verified neural editing helps on other proof sources, but matched frozen-model controls show that its gains need not come from training. The supervision does improve whole-proof rewriting: fine-tuning raises verified token reduction from 2.8% to 5.5% on 19 PutnamBench proofs. Together, the released edits, complete candidate pools, and controlled evaluations separate learning to imitate a search policy from improving on that search. They provide a reproducible basis for studying proof improvement while keeping correctness, compression, and edit policy distinct.