热点事件持续更新
形式化证明压缩框架LeanPolish发布
1 篇报道1 个报道来源4 小时前更新
先了解这件事
AI 综述
2026年10月1日，研究人员推出面向Lean 4形式化证明压缩的符号管道LeanPolish。该框架公开了包含33,402条验证通过的局部编辑及65,596条失败尝试的数据集。实验结果显示，基于该监督训练的排序器在测试集状态下挑选最佳候选的准确率达到70.1%，显著高于冻结基线的36.9%；同时，其迭代符号处理成功将miniF2F的证明压缩率提升至27.5%。
AI 根据报道生成 · 4 小时前更新
最新进展10月1日 12:00
研究人员推出Lean 4证明压缩框架LeanPolish并公开近十万条编辑数据。报道时间线
沿着报道，了解事件的不同侧面。
10月1日
- arXiv 机器学习LeanPolish：面向 Lean 形式化证明压缩的已验证监督框架
研究人员推出 Lean 4 形式化证明压缩符号管道 LeanPolish，并公开了 33,402 条验证通过的局部编辑及 65,596 条失败尝试数据。基于该监督训练的排序器在测试集状态下选择最佳候选的准确率达 70.1%，远超冻结基线的 36.9%，且迭代符号处理将 miniF2F 压缩率提升至 27.5%。
本事件热度走势
当前热度 9·可比范围峰值 10（10月1日 13:00）·近 24 小时可比范围变化 –
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。