ProofCompass: Enhancing Specialized Provers with LLM Guidance
Nicolas Wischermann, Claudio Mayrink Verdun, Gabriel Poesia, Francesco Noseda

TL;DR
ProofCompass introduces a hybrid approach that leverages large language models to guide specialized theorem provers, significantly improving efficiency and success rates without additional training.
Contribution
It presents a novel method combining LLM guidance with existing provers, reducing computational resources while enhancing proof success.
Findings
Outperforms DSP-v1.5 on miniF2F benchmark
Uses 25x fewer attempts for proof success
Achieves better resource efficiency and accuracy
Abstract
Language models have become increasingly powerful tools for formal mathematical reasoning. However, most existing approaches rely exclusively on either large general-purpose models or smaller specialized models, each with distinct limitations, while training specialized large models still requires significant computational resources. This paper introduces ProofCompass, a novel hybrid methodology that achieves remarkable computational efficiency by strategically guiding existing specialized prover methods, such as DeepSeek-Prover-v1.5-RL (DSP-v1.5) with a Large Language Model (LLM) without requiring additional model training. The LLM provides natural language proof strategies and analyzes failed attempts to select intermediate lemmas, enabling effective problem decomposition. On the miniF2F benchmark, ProofCompass demonstrates substantial resource efficiency: it outperforms DSP-v1.5…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
