Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

The paper presents a novel approach to boosting formal theorem provers by leveraging compiler outputs. The authors observe that compilers map a vast space of diverse proof attempts to a compact set of structured failure modes, and introduce a learning-to-refine framework that exploits this compression to perform efficient learning and proof exploration. The framework performs tree search that corrects errors locally conditioned on explicit verifier feedback, thereby circumventing the costs associated with accumulating a long history of proof attempts. The authors evaluate their method extensively, showing that it consistently amplifies the reasoning capabilities of base provers across varying scales. Notably, their approach achieves state-of-the-art performance on PutnamBench among publicly reported models under comparable test-time budgets, offering a scalable paradigm for next-generation verifier-guided reasoning.

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