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

As formal mathematics libraries expand, maintaining and improving verified proofs becomes computationally expensive and difficult to automate. Proof optimization—restructuring logical arguments for clarity, efficiency, or training data quality—traditionally relies on hand-coded heuristics and lacks scalable solutions.

ImProver 2 introduces a neurosymbolic framework (combining neural networks with symbolic logic) that uses expert iteration (iteratively training models on their own successful outputs) and a structured scaffold exposing both formal logical structure and informal abstractions. The team trained a 7-billion-parameter language model on this pipeline within Lean 4, a formal verification system.

Results show the 7B model outperformed orders-of-magnitude larger models in the same family and competed with mid-tier frontier models across structural proof metrics. The neurosymbolic scaffold improved performance consistently across both small and large models, demonstrating that proof optimization is learnable and scalable.