Technische Samenvatting: Pseudo-formalisatie voor Automatische Bewijsverificatie

Probleemstelling

Betrouwbare automatische verificatie van wiskundige bewijzen blijft een kritieke knelpunt voor het trainen en evalueren van AI-systemen op complex wiskundig redeneren. Hoewel volledig formele bewijzen (bijvoorbeeld in Lean of Isabelle) eenvoudig te verifiëren zijn vanwege hun semantische precisie en modulariteit, missen de meeste bewijzen – met name die gegenereerd door AI of geschreven door mensen in natuurlijke taal – deze eigenschappen. Het vertalen van bewijzen in natuurlijke taal naar volledig formele talen is vaak onuitvoerbaar voor grenswiskunde vanwege onvolledige formele bibliotheken en de enorme hoeveelheid expertinspanning die vereist is. Bijgevolg worstelen huidige verificatiemethoden, zoals "LLM-as-judge" (directe evaluatie van bewijzen in natuurlijke taal), met precisie en recall, en slagen ze er vaak niet in specifieke fouten in lange, complexe argumenten te identificeren.

Methodologie: Pseudo-formalisatie en Blokverificatie

De auteurs stellen Pseudo-formalisatie (PF) gecombineerd met Blokverificatie (BV) voor als een raamwerk om de kloof te overbruggen tussen de flexibiliteit van natuurlijke taal en de verifieerbaarheid van formele bewijzen.

1. Pseudo-formeel Bewijsformaat

Een Pseudo-formeel bewijs decomposeert een argument in natuurlijke taal in een reeks zelfstandige modules (lemma's, proposities, claims). Elke module is een tuple $(P, c, \pi)$ die vertegenwoordigt:

• Premises ($P$): Expliciet gestelde aannames en overgeërfd context.
• Conclusie ($c$): De specifieke claim die bewezen wordt.
• Bewijs ($\pi$): Het argument in natuurlijke taal dat $c$ uit $P$ afleidt.

De structuur wordt beheerst door twee grafen:

• Afhankelijkheidsgraaf ($G$): Een gerichte acyclische graaf (DAG) waarbij een rand bestaat als een module de conclusie van een andere module oproept. Dit voorkomt circulaire redenering.
• Scope-erfgoedbos ($T$): Een bosstructuur die modules hiërarchisch organiseert (bijvoorbeeld lemma's binnen een propositie), waardoor context (definities, aannames) kan worden overgeërfd zonder herhaling.

De auteurs definiëren "Goede Pseudo-formele Bewijzen" als die welke voldoen aan twee desiderata: concisie (korte bewijzen die weinig andere knoppen oproepen) en beperkte scope-diepte (ondiepe erfgoedbomen). Theoretisch maakt het verifiëren van dergelijke bewijzen het mogelijk dat de contextlengte die voor elke verificatiestap vereist is, onafhankelijk blijft van de totale bewijsgrootte, wat "contextrot" (de degradatie van LLM-prestaties bij toenemende invoerlengte) mitigeert.

2. Het Verificatieproces (PF+BV)

Het verificatieproces omvat vier stappen, waarbij allemaal kant-en-klare LLM's worden gebruikt zonder fine-tuning:

1. Vertaling: Een LLM vertaalt het originele bewijs in natuurlijke taal $\Pi$ naar een Pseudo-formeel bewijs $\hat{\Pi}$. Een optionele zelfherstellende lus controleert $\hat{\Pi}$ op $\Pi$ om trouw te waarborgen.
2. Blokverificatie: Een verifieer-LLM controleert elke module van $\hat{\Pi}$ onafhankelijk. Het ontvangt de volledige premises van de module (inclusief overgeërfd context), conclusie, bewijs, en de geverifieerde conclusies van eventuele opgeroepen kindmodules. Het geeft een accept-verdict of een specifieke foutbeschrijving uit.
3. Kalibratie: Een kalibratie-LLM aggregateert per-module foutrapporten tot een eindverdict. Het kan configureerbare strengheidsdrempels toepassen en blok-niveau fouten terugkoppelen naar de structuur van het originele bewijs (bijvoorbeeld het identificeren van specifieke stappen of lemma's).
4. Parallelle Schaling: Het gehele proces wordt $k$ keer onafhankelijk uitgevoerd. Een bewijs wordt alleen geaccepteerd als alle $k$ runs het accepteren (pessimistische aggregatie). Dit maakt het mogelijk om af te wisselen tussen precisie en recall door $k$ te variëren.

Belangrijkste Bijdragen

1. Pseudo-formalisatie (PF): Een nieuw bewijsformaat dat de flexibiliteit van natuurlijke taal behoudt terwijl het de modulariteit en de expliciete premise-conclusiestructuur afdwingt die nodig zijn voor betrouwbare verificatie.
2. Blokverificatie (BV): Een algoritme dat bewijzen verifieert door ze te decomponeren in onafhankelijke blokken, wat theoretisch de contextvereisten vermindert en empirisch de foutdetectie verbetert.
3. ArxivMathGradingBench: Een nieuwe benchmark bestaande uit 35 wiskundige papers op onderzoeksniveau van arXiv die bekende, door auteurs gecorrigeerde fouten bevatten. Deze dataset vult een gat in bestaande benchmarks door verificatie te testen op echte onderzoekspublicaties in plaats van op problemen op competitieniveau.
4. Theoretische Rechtvaardiging: De auteurs leveren een stelling (Stelling 1) die aantoont dat voor "Goede" Pseudo-formele bewijzen, bloksgewijze verificatie kan worden gesimuleerd door een Transformer met vaste grootte met een contextlengte die onafhankelijk is van de bewijsgrootte, in tegenstelling tot de lineaire contextgroei die vereist is voor gehele-bewijsverificatie.

Experimentele Resultaten

De methode werd geëvalueerd op twee benchmarks: Hard2Verify (problemen op Olympiade/Putnam-niveau) en ArxivMathGradingBench (papers op onderzoeksniveau).

• Prestaties versus Baselines: Op beide benchmarks pareto-dominant PF+BV de "LLM-as-judge"-baseline. Dit betekent dat voor elk gegeven niveau van recall (het vermogen om fouten te vinden), PF+BV een hogere precisie bereikt (minder valse alarmen), en vice versa.
• Hard2Verify: PF+BV kwam overeen met de baseline in recall (~90%), maar verlaagde het aantal per bewijs gemarkeerde valse fouten aanzienlijk (meer dan 40% minder vals-positieven bij $k=8$).
• ArxivMathGradingBench: De benchmark bleek uitdagend, waarbij beide methoden bij $k=8$ ongeveer 50% van de geannoteerde fouten onopgemerkt lieten. PF+BV presteerde echter consequent beter dan de baseline in recall, vals-positiefpercentages en het aandeel papers waarbij alle geannoteerde fouten werden opgepikt.
• Kwalitatieve Analyse: Casestudies (bijvoorbeeld IMO 2024 P6) illustreren dat PF+BV slaagt door logische sprongen te isoleren in lokale blokken. Dit stelt de verifieerder in staat te detecteren wanneer een bewijs een premisse onterecht versterkt (bijvoorbeeld "zelfde teken" afleiden uit "geen $d$ en $-d$") zonder het gehele globale argument opnieuw te hoeven evalueren.

Betekenis en Claims

Het paper claimt dat Pseudo-formalisatie een praktisch alternatief biedt voor autoformalisatie (vertaling naar Lean/Isabelle) voor het verifiëren van modern wiskundig onderzoek. Hoewel autoformalisatie sterkere correctheidsgaranties biedt, is het vaak onuitvoerbaar voor huidig onderzoek vanwege onvolledigheid van bibliotheken. PF+BV offert de absolute zekerheid van formele verificatie op in ruil voor toepasbaarheid op een breder scala aan wiskundige domeinen, waarbij het gebruikmaakt van de rijke woordenschat en standaardtechnieken van natuurlijke taal terwijl het een structuur oplegt die fouten makkelijker lokaal maakt.

De auteurs positioneren dit werk als een stap naar schaalbaar toezicht op AI-redenering, waarbij een mechanisme wordt geboden om betrouwbare beloningssignalen te genereren voor het trainen van LLM's op moeilijke wiskunde en menselijke wiskundigen te helpen bij het beoordelen van bewijzen. Ze erkennen beperkingen, met name dat het produceren van een trouwe Pseudo-formele herschrijving niet triviaal is, en dat toekomstig werk het trainen van modellen om bewijzen direct in dit formaat te genereren, zou kunnen omvatten.