# Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

arXiv: https://arxiv.org/abs/2604.18587 · HTML: https://mlsanity.com/paper/2604.18587/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 18 of its 37 references that are in the map.
- First posted on arXiv 13 Mar 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 18 of 18)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Deep reinforcement learning from human preferences](https://mlsanity.com/paper/1706.03741/) (2017)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification](https://mlsanity.com/paper/2504.21230/) (2025)

## Abstract (arXiv)

Large language models (LLMs) have demonstrated significant potential in formal theorem proving, yet state-of-the-art performance often necessitates prohibitive test-time compute via massive roll-outs or extended context windows. In this work, we address this scalability bottleneck by exploiting an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts to a compact set of structured failure modes. We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration. We perform tree search that corrects errors locally conditioned on explicit verifier feedback, thereby circumventing the costs associated with accumulating a long history of proof attempts. Extensive evaluations show that our method consistently amplifies the reasoning capabilities of base provers across varying scales. Notably, our approach achieves state-of-the-art performance on PutnamBench among publicly reported ~8B and ~32B parameter models under comparable test-time budgets, offering a scalable paradigm for next-generation verifier-guided reasoning.