Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
arXiv:2604.18587v1 Announce Type: new
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 …