OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

TL;DR

OptProver is a new model that effectively transfers Olympiad-level theorem proving skills to undergraduate optimization problems by addressing distribution shifts with specialized training and evaluation benchmarks.

Contribution

The paper introduces OptProver, a model that bridges Olympiad and optimization theorem proving through novel training techniques and a new Lean 4 benchmark.

Findings

OptProver achieves state-of-the-art Pass@1 and Pass@32 on the optimization benchmark.

The model maintains competitive performance on general theorem-proving tasks.

Specialized preference learning improves domain transfer effectiveness.

Abstract

Recent advances in formal theorem proving have focused on Olympiad-level mathematics, leaving undergraduate domains largely unexplored. Optimization, fundamental to machine learning, operations research, and scientific computing, remains underserved by existing provers. Its reliance on domain-specific formalisms (convexity, optimality conditions, and algorithmic analysis) creates significant distribution shift, making naive domain transfer ineffective. We present OptProver, a trained model that achieves robust transfer from Olympiad to undergraduate optimization. Starting from a strong Olympiad-level prover, our pipeline mitigates distribution shift through two key innovations. First, we employ large-scale optimization-focused data curation via expert iteration. Second, we introduce a specialized preference learning objective that integrates perplexity-weighted optimization with a mechanism to penalize valid but non-progressing proof steps. This not only addresses distribution shifts but also guides the search toward efficient trajectories. To enable rigorous evaluation, we construct a novel benchmark in Lean 4 focused on optimization. On this benchmark, OptProver achieves state-of-the-art Pass@1 and Pass@32 among comparably sized models while maintaining competitive performance on general theorem-proving tasks, demonstrating effective domain transfer without catastrophic forgetting.