Probabilistic Proof State Compression: Optimizing LLM-Guided Formal Verification

Despite recent successes in LLM-guided formal proof search, scalability remains limited by the large search space. This paper introduces a novel approach that integrates off-the-shelf LLMs with conformal prediction-based compression to optimize proof search. By employing adaptive, probability-based binning informed by conformal prediction intervals, our method compresses the proof state space, reducing computational demands while retaining statistical proof guarantees. Preliminary results on the Lean miniF2F test set show similar success rates with 75% fewer passes, and on average 23% reduced wall clock time.