🤖 machine learning

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

The paper introduces VERITAS, a zero-shot framework that enhances formal theorem proving by routing rich verifier signals back into the search process via a two-phase Best-of-N and critic-guided MCTS protocol, achieving state-of-the-art performance on benchmarks like miniF2F and a new combinatorics dataset.

Original authors: Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

Published 2026-06-19

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a very difficult puzzle, like a complex math problem, but you are doing it with a team of AI assistants. Usually, when these AI assistants try to solve a problem, they guess a solution, check if it works, and if it fails, they just get a simple "No, try again" signal. They throw away all the details about why it failed.

VERITAS is a new system that changes the game. Instead of just saying "No," it listens to the specific reasons the proof failed and uses those reasons to guide the next guess. Think of it as a detective who doesn't just say "The suspect is innocent," but says, "The suspect is innocent because they were at the store at 5 PM, so let's look for someone else who was at the store."

Here is how VERITAS works, broken down into simple parts:

1. The Team of Four Specialists

VERITAS doesn't rely on just one AI brain. It uses a team of four specialized "agents" that talk to each other:

The Strategist: Before trying to solve the problem, this agent decides on a high-level plan (e.g., "Let's try to break this down by cases" or "Let's try to prove it by contradiction"). It narrows the search so the team doesn't waste time on bad ideas.
The Retriever: This agent is like a librarian. It quickly finds the right reference books (math rules and lemmas) that might help solve the current step.
The Tactician: This is the main worker. It tries to write the actual steps of the proof. Crucially, it looks at a list of failed attempts from earlier. If a previous attempt failed because it used the wrong name for a rule, the Tactician is told, "Don't use that name again; here is the error message."
The Critic: This agent acts like a coach. It watches the progress and says, "You're getting closer," or "You're going down a dead end," based on the specific feedback from the computer checking the math.

2. The Two-Phase Game Plan

The system plays the game in two distinct rounds to be efficient:

Phase 1: The "Quick Sweep" (Best-of-N)
The team makes 5 quick, independent guesses at the solution. If one of them works, great! They stop immediately. This is fast and handles the "easy" problems.
Phase 2: The "Deep Dive" (Critic-Guided Search)
If the quick sweep fails, the system switches to a more careful mode. It takes all the mistakes from Phase 1 and feeds them back into the Tactician as "negative examples."
- Analogy: Imagine you are trying to open a locked door. In Phase 1, you try 5 different keys quickly. None work. In Phase 2, instead of just trying random keys, you look at the 5 keys that jammed the lock, note exactly how they jammed, and use that information to craft a new key that fits the specific shape of the lock.

3. Why This Matters: The "Combinatorics" Problem

The paper tested this on two types of math problems.

Standard Math Problems: VERITAS solved more of these than previous methods (40.6% vs 36.9%).
Combinatorics (Counting Problems): This is where VERITAS really shined. In these problems, you often need to use very specific, exact names for math rules.
- The Problem: Standard AI guessing often "hallucinates" (makes up) names for rules that don't exist. If an AI guesses a fake rule name, a standard system just says "Fail" and moves on.
- The VERITAS Fix: Because VERITAS reads the specific error message ("Unknown constant 'X'"), it learns in real-time that "X" doesn't exist. It iteratively corrects the name until it finds the real one.
- Result: On these hard counting problems, standard guessing actually got worse the more it tried (because it kept making up fake names). VERITAS got better because it learned from its mistakes.

4. The "Monotonicity" Guarantee

The authors made sure that VERITAS never loses a solution it already found.

The Guarantee: If the "Quick Sweep" (Phase 1) solves a problem, VERITAS keeps that solution and doesn't touch it. The "Deep Dive" (Phase 2) only works on the problems the first phase couldn't solve.
Why it matters: This proves that any extra success VERITAS achieves comes specifically from the smart, feedback-driven search, not just from trying more random guesses.

5. The "Batch" Trick

One of the clever engineering tricks in the paper is how they check the answers.

Old Way: Check one guess, wait for the computer to say "No," check the next guess, wait, check the next... This is slow.
VERITAS Way: They pack 6 guesses into a single file and ask the computer to check them all at once. This makes the system about 10 to 20 times faster, saving a lot of time and money.

Summary

VERITAS is a system that treats the computer's error messages not as a "stop sign," but as a map. By reading the specific reasons why a proof failed (syntax errors, wrong types, missing steps) and feeding that information back into the AI's next attempt, it can solve difficult math problems that other systems give up on. It combines a fast "try-and-see" approach with a smart "learn-from-failure" approach to get the best results.

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

Problem Statement

Current Large Language Model (LLM)-based formal theorem provers typically collapse rich, structured signals from formal verifiers (such as Lean 4) into a binary pass/fail outcome. Verifiers provide granular feedback including syntax errors, type mismatches, partial goal progress, and proof completion status. However, standard pipelines discard these intermediate artifacts, summarizing them into scalar rewards or discarding them entirely. This forces the search algorithm to "relearn" information the verifier has already explicitly provided, a limitation that becomes particularly costly in proofs requiring chains of dependent tactics where the correctness of each step hinges on the previous step's effect on the goal.

Methodology: The VERITAS Framework

VERITAS is a zero-shot framework designed to route every verifier signal back into the proof generation process. It employs a four-agent architecture coordinated by a shared proof state and a two-phase search protocol.

1. Four Specialized Agents

All agents operate on a shared ProofState containing the theorem, current goal, hypotheses, tactic history, and four structured signals from Lean:

Strategist: Maps the proof state to one of six high-level strategies (direct, induction, contradiction, cases, rewrite, apply_lemma) and estimates depth, restricting the search to a relevant subspace.
Retriever: Surfaces relevant Mathlib premises by scoring keyword overlap against goal tokens, lemma names, and signatures.
Critic: A lightweight model that scores partial proof states, suggesting next tactics and pruning recommendations. It replaces random rollouts in MCTS with a value estimate integrating Lean's four-way feedback.
Tactician: Generates $K$ tactic candidates conditioned on the strategy, retrieved premises, Critic guidance, and crucially, a list of previously failed tactics with their specific Lean error messages injected as negative examples.

2. Two-Phase Protocol with Monotonicity Guarantee

The framework utilizes a conservative two-phase protocol to ensure that gains are attributable to the feedback-driven search:

Phase 1 (Best-of-N): A standard Best-of-N sweep (e.g., $N=5$ ) generates tactics in a single batch. If any succeed, the theorem is solved immediately.
Phase 2 (Critic-Guided MCTS): Activated only if Phase 1 fails. The set of failures from Phase 1 (tactics and their errors) is injected into the Tactician's system prompt as negative examples. The Critic guides a Monte Carlo Tree Search (MCTS) where:
- Selection: Uses an extended UCB formula incorporating the Critic's value and strategy alignment.
- Expansion: Agents run sequentially; candidates are validated via a Batched Lean Validation trick.
- Simulation: Replaces random rollouts with the Critic's value augmented by structured signals ( $\sigma_A$ syntax, $\sigma_B$ type, $\sigma_C$ progress, $\sigma_D$ completion).
- Backpropagation: Carries the structured signals upward rather than collapsing to binary win/loss, preserving credit for partial progress.

Batched Lean Validation: Instead of invoking Lean $K$ times per expansion, candidates are compiled into a single .lean file as private theorems and validated in one call. This reduces verification cost from $O(K)$ to $O(1)$ , yielding a $\sim10\times$ speedup.

Monotonicity: The protocol guarantees that the final set of solved theorems is a superset of those solved by Phase 1 alone ( $S \supseteq S_1$ ). This isolates the contribution of Phase 2, ensuring that any additional solves are strictly due to the verifier-guided MCTS.

Key Contributions

Zero-Shot Four-Agent Framework: A system that routes structured Lean feedback (syntax, type, progress, completion) into every generation decision without trace fine-tuning.
Two-Phase Protocol: A Best-of-N $\to$ Critic-MCTS design with an internal monotonicity guarantee that allows for clean attribution of search contributions.
Efficiency Optimization: A batched Lean validation trick that reduces verification overhead by approximately $10\times$ .
VERITAS-CombiBench: A new benchmark of 55 author-verified, hard combinatorics theorems in Lean 4, released to expose limitations in unguided sampling.
Attribution Analysis: Empirical evidence showing that 11 miniF2F theorems were uniquely solvable by the MCTS phase, which flat sampling could not reach.

Experimental Results

Experiments were conducted on miniF2F (244 theorems) and VERITAS-CombiBench (55 theorems).

miniF2F Performance: VERITAS achieved a 40.6% solve rate (99/244), outperforming an independent Best-of-5 baseline (36.9%) and a handcrafted Portfolio (26.2%).
- Phase 2 contributed 11 unique solves that flat sampling could not achieve, primarily on problems requiring 2–4 dependent tactics.
- On "hard" non-sorry problems, VERITAS reached 28.9% vs. 25.9% for Best-of-5.
VERITAS-CombiBench Performance: This benchmark highlighted the failure of unguided sampling. Best-of-5 achieved only 1.8%, falling below the Portfolio (3.6%) because LLMs hallucinated incorrect Mathlib lemma names. VERITAS reached 7.3% by iteratively correcting these names using Lean's error feedback.
Efficiency: VERITAS dominates the Pareto frontier for inference-only methods, achieving 40.6% solve rate with ~27 Lean calls per theorem at an API cost of ~$150 per sweep.
Failure Modes: Analysis showed that 32% of failures were syntax-level (hallucinated names), 17% were type-correct but wrong, and 10% were "near-misses" (partial goal progress) where the Critic could provide high-value guidance.

Significance and Claims

The paper posits a general design principle: when a deterministic verifier emits structured intermediate signals, folding them back into generation amplifies the LLM substantially more than additional sampling does.

VERITAS demonstrates that:

Verifier Signals as State: Deterministic verifier signals can serve as inference-time state, not just final checks.
Synergy of Components: Tightly coupling the verifier with generation is more effective than scaling either the LLM or the search component in isolation.
Iterative Correction: For domains requiring precise lemma retrieval (like combinatorics), iterative correction from verifier errors is superior to flat sampling, which tends to hallucinate lexically incorrect names.

The authors conclude that while VERITAS is not a cure for IMO-level creativity or interactive latency, its primary contribution is routing: efficiently collecting easy proofs in Phase 1 and spending computational budget in Phase 2 only where verifier failures can guide the next tactic. Future work is identified as improving retrieval, creating cheaper critics, and distilling Phase 2 traces to scale this principle to the remaining hard tail of problems.