Formal theorem proving with large language models (LLMs) often loses valuable information because verifier feedback—syntax errors, type mismatches, partial goal progress—is collapsed into a simple pass/fail signal. A new framework called VERITAS aims to change that by feeding every verifier signal back into the proof search process, achieving significant gains on established benchmarks.
The Problem: Lost Verifier Signals
According to the paper published on arXiv, LLM-based formal provers typically reduce the rich output of a verifier to a binary result. This discards information that could guide the search for a correct proof, such as which part of a statement is syntactically invalid or where a type mismatch occurs. The authors argue that this simplification limits the ability of zero-shot methods to solve complex theorems, especially when correct lemma names must be recovered iteratively.
How VERITAS Works
VERITAS (Verifier-Guided Proof Search) is a zero-shot framework that introduces a two-phase protocol. In Phase 1, it performs Best-of-N sampling—generating multiple proof candidates and selecting those that pass a verifier. In Phase 2, a critic-guided Monte Carlo Tree Search (MCTS) pass ingests the failures from Phase 1 as explicit negative examples. The protocol preserves every theorem solved by Phase 1, so additional solves in Phase 2 are directly attributable to feedback-driven exploration. The authors note that this design ensures that performance improvements come from leveraging verifier signals, not from increasing sampling effort.
Benchmark Results
The researchers evaluated VERITAS on two benchmarks. On the miniF2F benchmark, a standard test for formal theorem proving, VERITAS achieved 40.6%. This compares favourably with an independently run Best-of-5 baseline at 36.9% and a Portfolio method at 26.2%. The portfolio approach tries multiple strategies without guidance, while Best-of-5 simply samples five candidates.
On a new benchmark introduced in the paper—VERITAS-CombiBench, consisting of 55 combinatorics theorems—the advantages of verifier-guided search become even clearer. VERITAS scored 7.3%, whereas Best-of-5 fell to 1.8% and Portfolio reached 3.6%. The authors explain that unguided sampling hurts when the proof requires recovering correct lemma names through iterative verifier feedback. The table below summarises the results.
| Benchmark | VERITAS | Best-of-5 | Portfolio |
|---|---|---|---|
| miniF2F | 40.6% | 36.9% | 26.2% |
| VERITAS-CombiBench | 7.3% | 1.8% | 3.6% |
The gains on VERITAS-CombiBench are particularly notable because the benchmark was designed to expose the weakness of methods that ignore verifier feedback. The authors released the benchmark alongside the framework to facilitate further research.
Implications for AI-Driven Proof Search
VERITAS demonstrates that preserving and routing verifier signals can substantially improve zero-shot theorem proving without requiring additional training data or fine-tuning. The framework is method-agnostic and can be applied to different underlying LLMs or verifiers. The authors have made the code and artifacts available on GitHub, enabling other researchers to reproduce and extend the work.
For enterprise technology leaders, the approach underscores a broader lesson: in AI systems that rely on external validation—whether for code generation, compliance checking, or formal verification—using all available feedback signals rather than a simplified summary can unlock significant performance gains. While VERITAS is aimed at mathematical theorem proving, its two-phase protocol could inspire similar architectures in other domains where verifiers produce rich diagnostic information.
