Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

arXiv:2604.18587v1 Announce Type: cross Abstract: 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...