VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

VERITAS is a zero-shot formal theorem proving framework that enhances LLM-based provers by integrating verifier signals into proof search via a two-phase protocol: Best-of-N sampling followed by a critic-guided Monte Carlo Tree Search (MCTS). This approach allows the system to utilize Phase 1 failures as negative examples, resulting in a performance of 40.6% on the miniF2F benchmark, surpassing the Best-of-5 method at 36.9% and Portfolio at 26.2%. The introduction of VERITAS-CombiBench, a 55-theorem combinatorics benchmark, further highlights the limitations of unguided sampling, demonstrating the importance of structured feedback in improving theorem proving efficacy for AI practitioners.