用自迭代框架让小模型高效优化复杂数学证明。
ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
- 设计专家迭代流程与轻量抽象结构，实现数据高效优化
- 70亿参数模型超越更大规模同类模型，接近主流前沿水平
- 适合想用小模型做数学证明优化的研究者和开发者
形式化数学库迅速扩展，亟需重构已验证的证明以提升可维护性，并改善神经证明器的训练数据质量。然而，可扩展的证明优化受限于目标异构、启发式设定、数据稀缺以及高昂的训练与推理成本。为此，我们提出 ImProver 2，一个面向 Lean 4 的神经符号框架，用于自动化证明优化。ImProver 2 结合数据高效的专家迭代流水线与暴露形式结构的轻量级非形式抽象支架。我们还引入一套捕捉证明结构特性的度量指标。使用 ImProver 2，我们训练了一个 7B 参数模型，其在同类型模型中性能超越数量级更大的模型，并在多数指标上媲美中等规模前沿模型。此外，我们证明了恰当的支架与训练策略显著提升小模型与前沿模型的表现。通过合理架构与训练，小模型可有效重构研究级复杂证明，在多样且复杂的评估标准下表现媲美大型系统，确立证明优化为可规模化学习的任务。
原文摘要 · Abstract (English)
Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers. However, scalable proof optimization is hindered by heterogeneous and heuristically specified objectives, scarce data, and high training and inference costs. To overcome these challenges, we introduce ImProver 2, a neurosymbolic framework for automated proof optimization in Lean 4. ImProver 2 combines a data-efficient expert-iteration pipeline with a scaffold that exposes formal structure alongside lightweight informal abstractions. We further introduce a suite of metrics capturing structural proof properties. Using ImProver 2, we train a 7B-parameter model that outperforms orders-of-magnitude larger models within the same model family, and is competitive with mid-tier frontier models across metrics. We additionally demonstrate that our neurosymbolic scaffold significantly improves performance across both small and frontier models. We show that with proper scaffolding and training, small models can effectively restructure research-level proofs over complex and varied metrics, matching substantially larger systems and establishing proof optimization as a scalable, learnable task.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。