ImProver 2：用于神经符号证明优化的迭代自改进语言模型
ImProver 2是一个神经符号框架，用于自动化Lean 4中的证明优化。它通过数据高效的专家迭代流水线和暴露形式结构与轻量级非正式抽象的脚手架，训练出7B参数的模型，在性能上超越同系列大模型，与中端前沿模型竞争。研究表明，通过适当的脚手架和训练，小模型也能有效重构研究级证明。
形式化数学库的快速扩展带来了对已验证证明进行重构以提升可维护性和神经证明器训练数据质量的迫切需求。然而，可扩展的证明优化面临目标异构且启发式指定、数据稀缺、训练和推理成本高等挑战。为此，研究者提出了ImProver 2，一个用于Lean 4中自动化证明优化的神经符号框架。
ImProver 2的核心创新在于结合了数据高效的专家迭代流水线与一个特殊的脚手架，该脚手架既能暴露形式化结构，又能提供轻量级非正式抽象。此外，研究团队还引入了一套度量标准来捕捉证明的结构属性。凭借这一框架，他们训练了一个70亿参数的模型，该模型在性能上不仅超越了同系列中规模大数个数量级的模型，还能与中端前沿模型竞争各项指标。
实验进一步表明，神经符号脚手架能显著提升小模型和前沿模型的性能。通过恰当的脚手架和训练，小型模型能够有效地在复杂且多样的指标上重构研究级证明，其效果可与规模大得多的系统相媲美。这项工作确立了证明优化作为一个可扩展、可学习的任务，为形式化数学的未来发展提供了新的方向。