ImProver 2：面向神经符号证明优化的迭代自改进语言模型

形式化数学库正迅速扩张，为可维护性而重构已验证证明、以及为神经证明器提升训练数据质量的需求日益增长。然而，可扩展的证明优化受制于异质且依赖启发式设定的目标、稀缺的数据以及高昂的训练与推理成本。为克服这些挑战，我们提出ImProver 2，一个面向Lean 4自动化证明优化的神经符号框架。ImProver 2将数据高效的专家迭代流水线与一个同时暴露形式结构和轻量非形式抽象的脚手架相结合。我们进一步提出一组刻画证明结构性质的指标。利用ImProver 2，我们训练了一个7B参数模型，它在同一模型家族中胜过大了几个数量级的模型，并在各指标上与中档前沿模型相当。我们还证明，该神经符号脚手架能显著提升小模型与前沿模型的性能。我们表明，配合恰当的脚手架与训练，小模型能够依据复杂多样的指标有效重构研究级证明，媲美大得多的系统，并确立证明优化是一个可扩展、可学习的任务。