ImProver 2：用于神经符号证明优化的迭代自我改进 LM

arXiv:2605.22885v1 公告类型：新 摘要：正式数学库正在迅速扩展，因此越来越需要重构经过验证的证明以实现可维护性并提高神经证明者的训练数据质量。然而，可扩展的证明优化受到异构和启发式指定目标、稀缺数据以及高训练和推理成本的阻碍。为了克服这些挑战，我们引入了 ImProver 2，这是一种用于 Lean 4 中自动证明优化的神经符号框架。ImProver 2 将数据高效的专家迭代管道与暴露正式结构和轻量级非正式抽象的支架相结合。我们进一步引入了一套捕获结构证明属性的指标。使用 ImProver 2，我们训练了一个 7B 参数模型，该模型的性能优于同一模型系列中的较大模型，并且在各个指标上与中层前沿模型具有竞争力。我们还证明，我们的神经符号支架显着提高了小型模型和前沿模型的性能。我们表明，通过适当的脚手架和训练，小型模型可以有效地在复杂且多样的指标上重组研究级证明，匹配更大的系统，并将证明优化建立为可扩展的、可学习的任务。