🤖 machine learning

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

OptProver introduces a continual training pipeline that enables an Olympiad-level theorem prover to successfully transfer its reasoning capabilities to the undergraduate optimization domain through expert-curated data and a specialized preference learning objective.

Original authors: Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

Published 2026-04-28

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Tale of the Math Prodigy and the Specialist: How "OptProver" Learned a New Language

Imagine you have a brilliant student named Olympiad-Bot. This student is a superstar at solving high-school math competitions—the kind of problems that involve clever tricks, geometry puzzles, and intense logic. If you give Olympiad-Bot a math contest problem, it shines.

However, there is a problem. Olympiad-Bot has never stepped foot in a university. It knows how to solve "riddles," but it doesn't know how to do Optimization.

Optimization is the math of "finding the best way." It’s what GPS uses to find the fastest route, what Netflix uses to suggest movies, and what engineers use to build stable bridges. It’s not just about clever tricks; it’s about a very specific, heavy-duty language involving complex rules like convexity (the math of "bowl-shaped" curves) and convergence (the math of "getting closer to the goal").

When researchers tried to teach Olympiad-Bot this new subject, something went wrong. It was like trying to teach a Shakespearean actor how to write computer code. The actor might learn a few technical words, but they’d lose their poetic soul, and their "code" would be full of weird, useless flourishes that don't actually run the program.

This paper introduces OptProver—the solution to this "identity crisis."

The Three Big Problems

The researchers identified three reasons why teaching math to AI is harder than it looks:

The "Identity Crisis" (Catastrophic Forgetting): When you force a model to learn a new, specialized subject, it often "forgets" how to do the general math it was originally good at. It becomes a specialist that has lost its common sense.
The "Dead-End" Trap (Stagnant Tactics): In formal math (using a tool called Lean), every step must be perfect. The AI often suggests steps that are "technically legal" but totally useless. Imagine trying to get to the top of a mountain, and instead of climbing, you decide to walk in a perfect, beautiful circle. You aren't breaking any laws of physics, but you aren't getting any higher either.
The "Language Gap" (Distribution Shift): The way math is written in textbooks is very different from the way it’s written in competition puzzles. The AI gets confused by the change in "vibe."

How OptProver Fixed It: The Three-Step Training Plan

To turn the "Olympiad Prodigy" into an "Optimization Expert," the team used three clever strategies:

1. The "Self-Study" Phase (Expert Iteration)

Instead of just handing the AI a textbook and saying "Read this," they let the AI practice. They gave it thousands of mathematical statements and told it, "Try to prove these. If you succeed, study your own successful path. If you fail, try a different way." This is like a musician practicing scales until the movements become second nature.

2. The "No More Circles" Rule (Utility-Aware Preference)

To stop the AI from walking in "mathematical circles," the researchers introduced a special way of grading it.

Grade A: A step that actually moves you closer to the answer.
Grade B: A step that is technically correct but leads to a dead end (the "stagnant" step).
Grade F: A step that is just plain wrong.

By teaching the AI to prefer Grade A over Grade B, they trained it to be efficient, not just "correct." It learned to stop wasting time on beautiful but useless logic.

3. The "Steady Hand" Method (Perplexity-Weighted DPO)

When learning something new, AI can sometimes get "overwhelmed" by extremely difficult or weirdly phrased sentences, causing its brain to glitch (numerical instability). The researchers added a "weighting" system. It’s like a teacher saying, "Focus on the core concepts first; don't get distracted by the weirdly worded footnotes until you've mastered the basics." This kept the training stable and prevented the AI from losing its original skills.

The Result: A True Specialist

The researchers built a new test called OptBench to see if it worked. The results were impressive:

It’s a Specialist: OptProver crushed the old models in optimization math, solving over 55% of the complex problems.
It Kept Its Brain: Unlike previous attempts, OptProver didn't forget its old skills. It stayed just as good (or even better!) at general math.
It’s Efficient: It doesn't just find the answer; it finds the smartest path to the answer.

In short: OptProver isn't just a student who memorized a textbook; it's a student who actually learned how to think like an optimizer.

Technical Summary: OptProver

OptProver is a specialized formal theorem-proving model designed to bridge the gap between Olympiad-level mathematical reasoning and undergraduate-level optimization theory. The paper addresses the challenge of transferring knowledge from general mathematical domains to highly specialized ones in the context of interactive formal verification.

1. The Problem: Interactive Distribution Shift

While current Large Language Model (LLM)-based provers excel at Olympiad mathematics (e.g., MiniF2F), they struggle with optimization, a cornerstone of machine learning and scientific computing. The authors identify two primary barriers to domain adaptation:

The Rigor of the Verifier: Unlike natural language adaptation, formal proving requires absolute syntactic correctness. A single incorrect tactic invalidates the entire proof.
Interactive Distribution Shift: Naive continual training (SFT) on new domains often leads to catastrophic forgetting of general reasoning skills and the introduction of "stagnant tactics." These are tactics that are syntactically valid and follow the new domain's style but are strategically aimless, leading the search process into "dead ends" that consume computational budget without progressing toward a solution.
Decoupling of Perplexity and Utility: The authors demonstrate that minimizing perplexity on new corpora does not guarantee improved proving ability; in fact, it can degrade performance by teaching the model "distractor" patterns.

2. Methodology: A Robust Continual Training Pipeline

To mitigate these issues, the authors propose a multi-stage framework that moves beyond simple supervised fine-tuning:

Large-Scale Self-Distillation (Expert Iteration): Instead of training only on static textbooks, the model uses Expert Iteration (EI). It treats Mathlib (a massive formal library) as a seed, performing model-guided searches to discover new, successful proof trajectories. This "self-play" ensures the model learns tactics that are not just syntactically correct but are actually discoverable and verifiable by the model itself.
Utility-Aware Preference Optimization (UAPO): To solve the "stagnant tactic" problem, the authors introduce a preference learning mechanism. They categorize tactics into three utility levels:
1. Proven ( $u=2$ ): Leads to a successful proof.
2. Stagnant ( $u=1$ ): Syntactically valid but leads to a dead end (exhausts search budget).
3. Invalid ( $u=0$ ): Results in compilation/runtime errors.
  By using a preference-based objective, the model is explicitly trained to prefer $u=2$ over $u=1$ , effectively penalizing "distractor" tactics that look correct but provide no progress.
Perplexity-Weighted DPO (PW-DPO): To stabilize training and prevent the model from overfitting to high-variance, out-of-distribution tokens (which cause numerical instability in Direct Preference Optimization), the authors implement a token-level weighting mechanism. This down-weights tokens with high perplexity relative to the reference model, ensuring the gradient updates are grounded in reliable distributions.

3. Key Contributions

OptBench: A novel, rigorous benchmark of 400 undergraduate-level optimization problems (categorized into Basics, Convexity, and Algorithmic Analysis) implemented in Lean 4.
Novel Training Paradigm: The integration of PW-UAPO (Perplexity-Weighted Utility-Aware Preference Optimization), which combines strategic utility guidance with statistical stability.
Empirical Framework: A demonstration of how to handle the "valid-but-unhelpful" tactic problem in step-level formal proving.

4. Results and Evaluation

State-of-the-Art Performance: On the OptBench benchmark, OptProver achieves a Pass@32 of 55.25%, significantly outperforming comparable 7B-scale models (e.g., DeepSeek-Prover-V2 and Goedel-Prover-V2), which struggle to reach 20% in many categories.
Robustness (No Catastrophic Forgetting): Unlike naive fine-tuning, OptProver maintains (and in some cases improves) its performance on general benchmarks like MiniF2F and ProofNet. This proves that the proposed pipeline successfully transfers domain knowledge without sacrificing foundational reasoning.
Efficiency: The model demonstrates an "unfold-then-reason" capability, effectively using tactics to expand specialized definitions (like KKT conditions or proximal operators) into manageable algebraic steps.

5. Significance

This work is significant because it provides a blueprint for domain-specific adaptation in formal verification. It moves the field away from the assumption that "more data = better model" and toward a more nuanced understanding of data utility. By explicitly modeling the strategic value of a proof step rather than just its syntactic correctness, OptProver demonstrates how to build specialized AI agents capable of tackling complex, professional-level mathematical domains.