Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

ArXi:2604.18587v1 Announce Type: cross Large language models (LLMs) have nstrated 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.