Technische Samenvatting: VERITAS: Verifier-Guided Proof Search voor Zero-Shot Formeel Theorem Proving

Probleemstelling

Huidige op Large Language Models (LLM's) gebaseerde formele theorem provers laten rijke, gestructureerde signalen van formele verifiers (zoals Lean 4) meestal instorten tot een binaire pass/fail uitkomst. Verifiers bieden granulair feedback, inclus\u00zafend syntactische fouten, type-mismatches, gedeeltige doelprogressie en bewijsvoltooiingsstatus. Echter, standaard pipelines verwerpen deze tussenliggende artefacten door ze te sommeren tot scalaire beloningen of ze geheel te negeren. Dit dwingt het zoekalgoritme om informatie opnieuw te "leren" die de verifier al expliciet heeft verstrekt, een beperking die bijzonder kostbaar wordt bij bewijzen die een keten van afhankelijke tactieken vereisen, waarbij de correctheid van elke stap afhangt van het effect van de vorige stap op het doel.

Methodologie: Het VERITAS-framework

VERITAS is een zero-shot framework ontworpen om elk verifier-signaal terug te leiden naar het bewijsproces. Het maakt gebruik van een vier-agent architectuur die wordt gecoördineerd door een gedeelde proof state en een twee-fasen zoekprotocol.

1. Vier Gespecialiseerde Agenten

Alle agenten opereren op een gedeelde ProofState die de stelling, het huidige doel, hypothesen, tactiekgeschiedenis en vier gestructureerde signalen van Lean bevat:

• Strategist: Brengt de proof state in kaart naar een van zes hoogwaardige strategieën (direct, inductie, contradictie, gevallen, herschrijven, apply_lemma) en schat de diepte in, waardoor de zoekruimte wordt beperkt tot een relevant subsysteem.
• Retriever: Haalt relevante Mathlib-premissen op door keyword overlap te scoren tegen doel-tokens, lemma-namen en signaturen.
• Critic: Een lichtgewicht model dat gedeeltelijke proof states scoort, volgende tactieken suggereert en pruning-aanbevelingen geeft. Het vervangt willekeurige rollouts in MCTS met een waarde-inschatting die de vierweg-feedback van Lean integreert.
• Tactician: Genereert $K$ tactiek-kandidaten geconditioneerd op de strategie, opgehaalde premissen, Critic-begeleiding en cruciaal: een lijst met eerder gefaalde tactieken met hun specifieke Lean-foutmeldingen geïnjecteerd als negatieve voorbeelden.

2. Twee-fasen Protocol met Monotoniciteitsgarantie

Het framework maakt gebruik van een conservatief twee-fasen protocol om ervoor te zorgen dat winsten toe te schrijven zijn aan de feedback-gestuurde zoektocht:

• Fase 1 (Best-of-N): Een standaard Best-of-N sweep (bijv. $N=5$) genereert tactieken in een enkele batch. Als er één slaagt, wordt de stelling direct opgelost.
• Fase 2 (Critic-Guided MCTS): Geactiveerd alleen als Fase 1 faalt. De verzameling mislukkingen uit Fase 1 (tactieken en hun fouten) wordt in de system prompt van de Tactician geïnjecteerd als negatieve voorbeelden. De Critic begeleidt een Monte Carlo Tree Search (MCTS) waarbij:
  • Selectie: Gebruikt een uitgebreide UCB-formule die de waarde van de Critic en strategie-alignement incorporeert.
  • Expansie: Agenten draaien sequentieel; kandidaten worden gevalideerd via een Batched Lean Validation truc.
  • Simulatie: Vervangt willekeurige rollouts door de waarde van de Critic, aangevuld met gestructureerde signalen ($\sigma_A$ syntaxis, $\sigma_B$ type, $\sigma_C$ progressie, $\sigma_D$ voltooiing).
  • Backpropagation: Draagt de gestructureerde signalen omhoog in plaats van ze te reduceren tot een binaire win/verlies, waardoor krediet behouden blijft voor gedeeltelijke progressie.

Batched Lean Validation: In plaats van Lean $K$ keer aan te roepen per expansie, worden kandidaten samengevoegd in één enkel .lean bestand als private theorems en gevalideerd in één enkele call. Dit vermindert de verificatiekosten van $O(K)$ naar $O(1)$, wat een snelheidswinst van ongeveer $\sim10\times$ oplevert.

Monotoniciteit: Het protocol garandeert dat de uiteindelijke verzameling opgeloste stellingen een bovendekking is van de stellingen die door Fase 1 alleen zijn opgelost ($S \supseteq S_1$). Dit isoleert de bijdrage van Fase 2, waardoor wordt gegarandeerd dat eventuele extra oplossingen strikt te danken zijn aan de verifier-gestuurde MCTS.

Belangrijkste Bijdragen

1. Zero-Shot Vier-Agent Framework: Een systeem dat gestructureerde Lean-feedback (syntaxis, type, progressie, voltooiing) naar elke generatiebeslissing routeert zonder trace fine-tuning.
2. Twee-fasen Protocol: Een Best-of-N $\to$ Critic-MCTS ontwerp met een interne monotoniciteitsgarantie die een zuivere attributie van zoekbijdragen mogelijk maakt.
3. Efficiëntie Optimalisatie: Een batched Lean validatie-truc die de verificatie-overhead met ongeveer $10\times$ vermindert.
4. VERITAS-CombiBench: Een nieuwe benchmark van 55 door auteurs geverifieerde, moeilijke combinatorische stellingen in Lean 4, uitgebracht om de beperkingen van ongeleide sampling bloot te leggen.
5. Attributie Analyse: Empirisch bewijs dat 11 miniF2F stellingen uniek oplosbaar waren door de MCTS-fase, wat platte sampling niet kon bereiken.

Experimentele Resultaten

Experimenten werden uitgevoerd op miniF2F (244 stellingen) en VERITAS-CombiBench (55 stellingen).

• miniF2F Prestaties: VERITAS bereikte een oplossingspercentage van 40,6% (99/244), waarmee het een onafhankelijke Best-of-5 baseline (36,9%) en een handmatig Portfolio (26,2%) verslaat.
  • Fase 2 droeg 11 unieke oplossingen bij die platte sampling niet kon bereiken, voornamelijk bij problemen die 2 tot 4 afhankelijke tactieken vereisen.
  • Op "harde" non-sorry problemen bereikte VERITAS 28,9% versus 25,9% voor Best-of-5.
• VERITAS-CombiBench Prestaties: Deze benchmark benadrukte het falen van ongeleide sampling. Best-of-5 bereikte slechts 1,8%, wat lager was dan de Portfolio (3,6%), omdat LLM's incorrecte Mathlib lemma-namen hallucineerden. VERITAS bereikte 7,3% door deze namen iteratief te corrigeren met behulp van de Lean-foutfeedback.
• Efficiëntie: VERITAS domineert de Pareto-front voor inference-only methoden, waarbij het een 40,6% oplossingspercentage bereikt met ongeveer 27 Lean calls per stelling tegen een API-kosten van ~$150 per sweep.
• Foutmodi: Analyse toonde aan dat 32% van de fouten op syntaxisniveau lag (gehallucineerde namen), 17% type-correct maar onjuist was, en 10% "near-misses" (gedeeltelijke doelprogressie) waren waar de Critic hoogwaardige begeleiding kon bieden.

Betekenis en Claims

Het paper stelt een algemeen ontwerpprincipe voor: wanneer een deterministische verifier gestructureerde tussenliggende signalen uitzendt, versterkt het terugvoeren hiervan in de generatie de LLM aanzienlijk meer dan aanvullende sampling doet.

VERITAS demonstreert dat:

1. Verifier Signalen als Toestand: Deterministische verifier-signalen kunnen dienen als inference-time toestand, niet alleen als eindcontroles.
2. Synergie van Componenten: Het nauw koppelen van de verifier met de generatie is effectiever dan het isoleren schalen van de LLM of de zoekcomponent.
3. Iteratieve Correctie: Voor domeinen die precieze lemma-retrieval vereisen (zoals combinatoriek), is iteratieve correctie vanuit verifier-fouten superieur aan platte sampling, dat de neiging heeft om lexicaal incorrecte namen te hallucineren.

De auteurs concluderen dat hoewel VERITAS geen genezing is voor IMO-niveau creativiteit of interactieve latentie, de primaire bijdrage routing is: het efficiënt verzamelen van eenvoudige bewijzen in Fase 1 en het besteden van de computationele budget in Fase 2 alleen daar waar verifier-fouten de volgende tactiek kunnen sturen. Toekomstig werk wordt geïdentificeerd als het verbeteren van retrieval, het creëren van goedkopere critics, en het distilleren van Fase 2 traces om dit principe te schalen naar de resterende harde staart van problemen.