arXiv cs.AIMonday · May 25, 2026FREE

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

arXiv:2605.22885 introduces ImProver 2, a neurosymbolic framework for automated proof optimization specifically within Lean 4. The framework aims to address critical challenges in formal mathematics, including the growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers. It tackles obstacles such as heterogeneous and heuristically specified objectives, scarce data, and high training and inference costs associated with current methods. ImProver 2 integrates a data-efficient expert-iteration pipeline with a neurosymbolic scaffold that exposes formal structure alongside lightweight informal abstractions, enhancing the model's understanding of proof structures. The researchers also developed a new suite of metrics to capture structural proof properties, enabling more precise evaluation. Using ImProver 2, a 7B-parameter model was trained that demonstrated superior performance compared to models orders of magnitude larger within the same model family. This model also achieved competitiveness with mid-tier frontier models across various metrics. The study further highlights that the neurosymbolic scaffold significantly enhances performance across both small and frontier models. This indicates that with appropriate scaffolding and training, smaller language models can effectively restructure complex, research-level proofs, offering a more efficient and scalable approach to formal verification and the maintenance of expanding formal mathematics libraries.