★ 3
LeanPolish：Lean证明压缩的验证监督
论文提出LeanPolish符号化Lean 4流水线，发布33402条被接受的局部编辑与65596条同状态失败尝试，研究模型从验证监督中学到什么。实验表明延续菜单评估可消除排序捷径，迭代符号化处理将miniF2F节省率从19.7%提升至27.5%，微调将PutnamBench验证token缩减从2…
arXiv cs.LG32 天前
共 1 篇相关资讯，按重要度与时间排序，每 3 小时更新。
论文提出LeanPolish符号化Lean 4流水线，发布33402条被接受的局部编辑与65596条同状态失败尝试，研究模型从验证监督中学到什么。实验表明延续菜单评估可消除排序捷径，迭代符号化处理将miniF2F节省率从19.7%提升至27.5%，微调将PutnamBench验证token缩减从2…