arXiv 于 2026 年 5 月 21 日收录了一篇题为《ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization》的新论文（编号 arXiv:2605.22885v1，cs.AI 类别），作者为 Riyaz Ahuja 等四人。该研究聚焦于形式化数学证明库快速扩张背景下的一个日益迫切的问题：如何对已经通过验证的证明进行重构，使其更易维护，同时提升面向神经证明器的训练数据质量。
论文指出，可扩展的证明优化面临多重障碍。首先是目标函数异质且往往依赖启发式规则来指定，缺乏统一而清晰的优化方向；其次是训练数据稀缺；第三是训练与推理成本高昂。这些问题共同限制了自动化证明优化在实际中的推广。
为应对上述挑战，研究团队提出了 ImProver 2，这是一个面向 Lean 4 的神经符号（neurosymbolic）框架，用于自动化证明优化。该方法将数据高效的专家迭代（expert-iteration）流水线与一种脚手架（scaffold）机制相结合，后者在暴露形式化结构的同时，提供轻量级的非形式化抽象，从而让模型在形式严谨性与可理解的中间表示之间取得平衡。此外，作者还引入了一套用于刻画证明结构性质的度量指标，使优化效果可以被更细致地评估。
在实验结果方面，研究团队利用 ImProver 2 训练了一个 70 亿参数规模的模型。该模型在同一模型家族内超越了参数量高出数量级的更大模型，并在多项指标上与中端前沿模型具有竞争力。作者进一步表明，其神经符号脚手架能够显著提升小型模型与前沿模型的性能。
论文的核心结论是：在恰当的脚手架设计与训练方法支持下，小型模型同样能够针对复杂多样的指标，有效地重构研究级别的证明，达到与规模大得多的系统相当的水平。这一结果将证明优化确立为一项可扩展、可学习（learnable）的任务。
从时间线看，该论文于 2026 年 5 月 21 日 02:20:26 UTC 提交，PDF 大小约 8,321 KB，DOI 已通过 DataCite 发放（注册尚待完成）。论文主题涵盖人工智能、计算与语言、机器学习以及计算机科学中的逻辑等多个方向。