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

经过验证的证明编辑为改进语言模型生成的Lean证明提供了天然的监督来源。然而，验证确定编辑是正确的，而不是其训练信号没有搜索伪影。我们引入了 LeanPolish，这是一个象征性的 Lean 4 管道，它发布了 33,402 个已接受的本地编辑和 65,596 个相同状态的失败尝试，并用它来研究模型从这种监督中学到了什么。首次成功搜索承认与目标无关的规则，具有完美的排名准确性；教师选择的评估网站也会奖励琐碎的删除。在第一次成功之后继续进行菜单评估消除了排序捷径：训练有素的排序器在评估的保留状态的 70.1% 上选择最佳候选，而最强的冻结基线为 36.9%。对于压缩，迭代符号传递将 miniF2F 节省从 19.7% 提高到 27.5%，超过了我们在那里测试的神经混合。经过验证的神经编辑有助于其他证据来源，但匹配的冻结模型控制表明其收益不一定来自训练。监督确实改善了整体证明重写：微调将 19 个 PutnamBench 证明的验证词元减少量从 2.8% 提高到 5.5%。发布的编辑、完整的候选池和受控评估将学习模仿搜索策略与改进搜索分开。它们为研究证明改进提供了可重复的基础，同时保持正确性、压缩和编辑策略的独特性。