LeanPolish：Lean 证明压缩的验证监督

中文摘要 AI 辅助

经过验证的证明编辑为改进语言模型生成的 Lean 证明提供了一种天然的监督来源。然而，验证仅能确认编辑的正确性，并不能保证其训练信号不受搜索伪影的影响。我们提出了 LeanPolish，一个符号化的 Lean 4 流水线，它发布了 33,402 个被接受的局部编辑和 65,596 个同状态下的失败尝试，并利用它来研究模型从这种监督中学到了什么。首次成功搜索允许一个与目标无关的规则，其排序准确率完美；教师选择的评估位置也会奖励琐碎的删除。在首次成功之后继续菜单评估消除了排序捷径：训练后的排序器在 70.1% 的评估保留状态上选择了最佳候选，而最强的冻结基线仅为 36.9%。对于压缩，迭代符号化过程将 miniF2F 的节省从 19.7% 提高到 27.5%，超过了我们测试的神经混合方法。经过验证的神经编辑对其他证明来源有所帮助，但匹配的冻结模型对照表明，其收益不一定来自训练。这种监督确实改善了整篇证明的重写：微调将 19 个 PutnamBench 证明的验证令牌减少从 2.8% 提高到 5.5%。综合来看，发布的编辑、完整的候选池和受控评估将模仿搜索策略的学习与在该搜索上的改进区分开来。它们为研究证明改进提供了可复现的基础，同时保持正确性、压缩和编辑策略的独立性。

英文摘要

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.

发表机构

• Imperial College London（伦敦帝国理工学院）

机构由 AI 辅助整理，请以论文原文为准。