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

• URL: http://arxiv.org/abs/2605.22885v1
• Date: Thu, 21 May 2026 02:20:26 GMT
• Title: ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
• Abstract summary: We introduce ImProver 2, a neurosymbolic framework for automated proof optimization in Lean 4.<n>ImProver 2 combines a data-efficient expert-iteration pipeline with a scaffold that exposes formal structure alongside informal abstractions.<n>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.
• Score: 19.226502853809734
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Beyond Foundation Models: Dimension-Aware Neural Architecture Search with Small-Data Representation Models for Cryocooler Lifetime Prediction [3.40327344752292]
  We propose the FSD-RM (Family of Small-Data Representation Models) paradigm as a practical alternative for limited, domain-specific telemetry.<n>We focus on capacity-controlled representation learning using established encoder architectures.<n> Experiments on cryocooler telemetry show that the proposed approach achieves competitive predictive performance.
  arXiv  Detail & Related papers  (2026-08-07T09:11:45Z)
• Dual-Phase LLM Reasoning: Self-Evolved Mathematical Frameworks [48.105258051884384]
  This paper proposes a new two-stage training framework that enhances models' self-correction capabilities.<n>During the first stage, a multi-turn dialogue strategy guides the model to generate long chain-of-thought (CoT) data.<n>The second stage employs a difficulty-aware rejection sampling mechanism to dynamically optimize data distribution.
  arXiv  Detail & Related papers  (2026-01-09T08:19:11Z)
• How to Set the Learning Rate for Large-Scale Pre-training? [73.03133634525635]
  We formalize this investigation into two distinct research paradigms: Fitting and Transfer.<n>Within the Fitting Paradigm, we introduce a Scaling Law for search factor, effectively reducing the search complexity from O(n3) to O(n*C_D*C_) via predictive modeling.<n>We extend the principles of $$Transfer to the Mixture of Experts (MoE) architecture, broadening its applicability to encompass model depth, weight decay, and token horizons.
  arXiv  Detail & Related papers  (2026-01-08T15:55:13Z)
• Motif-2-12.7B-Reasoning: A Practitioner's Guide to RL Training Recipes [7.998815625852598]
  We introduce a 12.7B parameter language model designed to bridge the gap between open-weight systems and proprietary frontier models in complex reasoning and long-context understanding.<n>Our approach combines memory-efficient infrastructure for 64K-token contexts using hybrid parallelism and kernel-level optimizations.<n>We detail a robust Reinforcement Learning Fine-Tuning pipeline that stabilizes training via difficulty-aware data filtering and mixed-policy trajectory reuse.
  arXiv  Detail & Related papers  (2025-12-11T00:51:18Z)
• Sycophancy Mitigation Through Reinforcement Learning with Uncertainty-Aware Adaptive Reasoning Trajectories [58.988535279557546]
  We introduce textbf sycophancy Mitigation through Adaptive Reasoning Trajectories.<n>We show that SMART significantly reduces sycophantic behavior while preserving strong performance on out-of-distribution inputs.
  arXiv  Detail & Related papers  (2025-09-20T17:09:14Z)
• LimiX: Unleashing Structured-Data Modeling Capability for Generalist Intelligence [61.46575527504109]
  LimiX-16M and LimiX-2M treat structured data as a joint distribution over variables and missingness.<n>We evaluate LimiX models across 11 large structured-data benchmarks with broad regimes of sample size, feature dimensionality, class number, categorical-to-numerical feature ratio, missingness, and sample-to-feature ratios.
  arXiv  Detail & Related papers  (2025-09-03T17:39:08Z)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Prover orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment.<n>bftextDelta Prover achieves a state-of-the-art 95.9% success rate on the miniF2F-test benchmark.
  arXiv  Detail & Related papers  (2025-07-21T03:56:35Z)
• High-Fidelity Scientific Simulation Surrogates via Adaptive Implicit Neural Representations [51.90920900332569]
  Implicit neural representations (INRs) offer a compact and continuous framework for modeling spatially structured data.<n>Recent approaches address this by introducing additional features along rigid geometric structures.<n>We propose a simple yet effective alternative: Feature-Adaptive INR (FA-INR)
  arXiv  Detail & Related papers  (2025-06-07T16:45:17Z)
• Ultra-Resolution Adaptation with Ease [62.56434979517156]
  We propose a set of key guidelines for ultra-resolution adaptation termed emphURAE.<n>We show that tuning minor components of the weight matrices outperforms widely-used low-rank adapters when synthetic data are unavailable.<n>Experiments validate that URAE achieves comparable 2K-generation performance to state-of-the-art closed-source models like FLUX1.1 [Pro] Ultra with only 3K samples and 2K iterations.
  arXiv  Detail & Related papers  (2025-03-20T16:44:43Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.