arXiv：cs.LG（机器学习，全量分类）· Pauline Bourigault·· 5 小时前AI 评分42
LeanPolish：为 Lean 证明压缩提供可验证监督
LeanPolish: Verified Supervision for Lean Proof Compression
AI 导读
LeanPolish 是一个符号化 Lean 4 流水线，发布了 33,402 条被接受的局部编辑和 65,596 条同状态失败尝试，用于研究模型能从这类监督中学到什么。
正文
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.
| Subjects: | Machine Learning (cs.LG) |
| Cite as: | arXiv:2609.38384 [cs.LG] |
| (or arXiv:2609.38384v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2609.38384 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Pauline Bourigault [view email]
[v1]
Tue, 29 Sep 2026 18:40:00 UTC (67 KB)
来源：arXiv：cs.LG（机器学习，全量分类） · arxiv.org