Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

1. Problem Statement

Formal theorem proving using Large Language Models (LLMs) has shown promise but faces a critical scalability bottleneck. State-of-the-art performance often requires prohibitive test-time compute, achieved through massive roll-outs (generating thousands of attempts) or extended context windows (accumulating long histories of failed attempts).

Existing approaches typically treat compiler feedback (error messages) as binary success/failure indicators or simple text strings. This approach ignores the rich structural information embedded in compiler outputs, forcing models to rely on cumulative, multi-round self-correction. Consequently, models become tethered to long interaction histories, causing context windows to expand rapidly and severely limiting the depth of exploration within fixed computational budgets.

2. Core Insight: The Compiler as a Dimension Compressor

The authors identify a fundamental structural property of formal verification: The Lean compiler acts as an effective dimension compressor.

• Observation: While the space of possible Lean programs (proof attempts) is combinatorially vast and diverse, the space of compiler error messages is surprisingly compact and structured.
• Mechanism: Many syntactically distinct incorrect proofs induce identical or invariant error signatures (e.g., "unsolved goals," "unknown identifier," "tactic failed").
• Implication: Compiler feedback filters out syntactic noise to expose underlying semantic defects. This allows the learning objective to shift from "blind generation" to "targeted correction" based on failure modes rather than specific program syntax.

3. Methodology: Learning-to-Refine Framework

The paper proposes a Learning-to-Refine framework that leverages this compression to perform efficient learning and proof exploration.

A. Theoretical Foundation: Chain of Distributions (CoD)

• Markovian Refinement: Unlike traditional methods that condition on the entire history of attempts, the proposed method treats refinement as a Markovian process. The next step depends only on the current failed attempt, the problem, and the compiler error message.
• Distributional Shift: Direct generation samples from a fixed distribution $D_{direct}$. Refinement, however, induces a Chain of Distributions (CoD). As the model iteratively corrects errors based on feedback, it transitions through a sequence of conditional distributions, effectively navigating the program space toward regions containing correct solutions that were initially out-of-distribution (OOD) for the base model.

B. Training Pipeline

1. Cold-Start Data Synthesis:
   • The authors synthesize training data by sampling incorrect and correct solutions for a given problem.
   • They use a strong LLM (Claude-3.7-Sonnet) to generate a "thought" trace that analyzes the compiler error and plans the correction, bridging the gap between the failed code and the correct solution.
   • This creates a supervised dataset for Supervised Fine-Tuning (SFT) where the model learns to repair its own failures.
2. Expert Iteration:
   • To adapt to the shifting distribution of errors as the model improves, the authors employ Expert Iteration.
   • The model attempts to solve problems, and successful refinement trajectories are converted into new supervision data. This creates an on-policy training loop where the model learns repair strategies for failure modes that emerge only after earlier refinements.

C. Test-Time Search Strategy

The framework models proof generation as a tree search problem, balancing two strategies:

• Breadth-First Search (BFS): Generating new proofs from scratch (Direct Generation).
• Depth-First Search (DFS): Refining a previously failed attempt.
• Value-Guided Tree Search: To optimize the allocation of the computational budget, the authors train a neural value function. This function estimates the potential of a specific node (state) to lead to a verified proof.
  • The value function is trained via preference learning, comparing states along successful trajectories against failed ones.
  • During inference, the search policy expands nodes based on a softmax distribution of these predicted values, prioritizing branches with higher refinement potential.

4. Key Contributions

1. Compiler as a Compressor: Theoretical and empirical demonstration that compiler error messages form a low-dimensional, structured partition of the proof space, enabling efficient learning.
2. Learning-to-Refine Framework: A novel architecture that internalizes error-correction trajectories via SFT and Expert Iteration, allowing models to generalize repair strategies across different problems sharing similar failure modes.
3. Chain of Distributions (CoD): A formalization of how iterative self-correction dynamically reshapes the sampling distribution, allowing models to escape local modes and find OOD solutions.
4. Value-Guided Search: A scalable search strategy that adaptively balances direct generation and refinement based on learned value estimates, significantly improving sample efficiency.

5. Experimental Results

The framework was evaluated on Kimina-Prover-Distill-8B and Goedel-Prover-V2-32B across four benchmarks: MiniF2F, ProofNet, MathOlympiadBench, and PutnamBench.

• Performance Gains:
  • The refined provers consistently outperformed their base counterparts.
  • Goedel-32B achieved over 50% relative improvement on ProofNet, MathOlympiadBench, and PutnamBench.
  • Kimina-8B showed significant gains, particularly on harder problems where direct generation saturates.
• State-of-the-Art (SOTA):
  • On PutnamBench, the Goedel-32B model solved 110 problems (out of 660), ranking first among all publicly reported ~32B parameter models under comparable test-time budgets.
  • The Kimina-8B model solved 25 problems, ranking first among ~8B parameter models.
• Efficiency: The method achieves these results with significantly lower computational budgets compared to systems relying on massive roll-outs or long context windows.
• Ablation Studies:
  • Refinement vs. Direct: Models trained only on direct synthesis (without refinement) showed marginal improvements, proving that the gains come from the refinement mechanism, not just additional data.
  • Search Strategy: Value-guided search consistently outperformed random tree search and pure BFS/DFS, demonstrating the value of adaptive exploration.

6. Significance and Future Work

• Scalability: The approach offers a scalable paradigm for next-generation verifier-guided reasoning, decoupling performance from context window size and massive roll-outs.
• Generalizability: The framework is model-agnostic and scales consistently with model size.
• Limitations & Future Directions:
  • Refinement is most effective for recurring, structurally regular errors (e.g., type mismatches). Deep semantic failures or global proof structure errors remain difficult to correct.
  • Future work includes applying this to larger Lean systems and investigating the transferability of this "compiler compression" concept to settings with weaker or noisier verification signals (e.g., non-formal reasoning).

In summary, "Compile to Compress" redefines how LLMs interact with formal verifiers. Instead of treating compiler errors as mere noise to be ignored or simple binary signals, it treats them as a compressed, high-value abstraction of the proof search space, enabling efficient, targeted, and scalable theorem proving.