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

arXiv: https://arxiv.org/abs/2606.19399 · HTML: https://mlsanity.com/paper/2606.19399/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 33 references that are in the map.
- First posted on arXiv 17 Jun 2026.

## Builds on (most cited first, 21 of 21)

- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation](https://mlsanity.com/paper/2308.08155/) (2023)
- [MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework](https://mlsanity.com/paper/2308.00352/) (2023)
- [CAMEL: Communicative Agents for "Mind" Exploration of Large Language Model Society](https://mlsanity.com/paper/2303.17760/) (2023)
- [Solving math word problems with process- and outcome-based feedback](https://mlsanity.com/paper/2211.14275/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Reinforcement Learning via Self-Distillation](https://mlsanity.com/paper/2601.20802/) (2026)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement](https://mlsanity.com/paper/2508.10059/) (2025)
- [SPIRAL: Symbolic LLM Planning via Grounded and Reflective Search](https://mlsanity.com/paper/2512.23167/) (2025)
- [DPO-F+: Aligning Code Repair Feedback with Developers' Preferences](https://mlsanity.com/paper/2511.01043/) (2025)
- [SynthFix: Adaptive Neuro-Symbolic Code Vulnerability Repair](https://mlsanity.com/paper/2604.17184/) (2026)

## Built on by (most cited first, 2 of 2)

- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)
- [Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify](https://mlsanity.com/paper/2610.13632/) (2026)

## Abstract (arXiv)

LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot framework that routes every verifier signal back into proof search through a two-phase protocol: Best-of-N sampling first, then a critic-guided MCTS pass that ingests Phase 1 failures as explicit negative examples. The protocol preserves every theorem solved by its own Phase 1 sweep, so Phase 2's additional solves are attributable to feedback-driven exploration. VERITAS reaches 40.6% on miniF2F (vs. an independently run Best-of-5 at 36.9%, Portfolio 26.2%) and 7.3% on VERITAS-CombiBench, a 55-theorem combinatorics benchmark we release on which Best-of-5 (1.8%) falls below Portfolio (3.6%), exposing that unguided sampling hurts when correct lemma names must be recovered iteratively from verifier feedback. Artifacts are available on GitHub.