Technische Samenvatting: Risicogestuurde Lean-as-Judge voor Natuurlijke-Taal Wiskundig Redeneren

1. Probleemstelling

Het artikel adresseert de uitdaging om formele bewijsassistenten (specifiek Lean) te gebruiken als beoordelaars voor in natuurlijke taal gegenereerde wiskundige redeneringen van Large Language Models (LLM's). Hoewel een succesvol Lean-bewijs sterke positieve bewijzen biedt voor een formele stelling, is de afwezigheid van een bewijs een dubbelzinnig signaal. Een mislukt bewijs kan wijzen op een wiskundig onjuist antwoord, maar kan evenzeer het gevolg zijn van een slecht getypeerde formalisering, ontbrekende bibliotheekfeiten of time-outs tijdens het zoeken naar een bewijs.

Huidige benaderingen behandelen bewijsmislukking vaak als een negatief signaal voor juistheid, wat het risico met zich meebrengt dat wiskundige onjuistheid wordt verward met een gebrek aan formele dekking. De auteurs identificeren een "dekking-afgrond": de betrouwbaarheid van formele selectie is scherp afhankelijk van het aandeel kandidaatantwoorden dat succesvol kan worden geformaliseerd en bewezen. Wanneer de dekking hoog is, is formele selectie zeer accuraat; wanneer de dekking laag is, wordt het signaal onbetrouwbaar.

Het kernprobleem is het bepalen wanneer een downstream-systeem een formeel Lean-signaal moet vertrouwen en wanneer het het signaal moet behandelen als buiten-de-dekking (d.w.z. onopgelost) in plaats van onjuist, terwijl een risico-garantie voor geaccepteerde antwoorden op basis van een eindige steekproef wordt geboden.

2. Methodologie: COVCAL

De auteurs stellen COVCAL (Coverage-Calibrated Lean) voor, een risicogestuurde selectieve wrapper die op basis van dekking-diagnostiek besluit of een formeel antwoord wordt geaccepteerd of wordt afgezien.

2.1 Framework voor Gedeeltelijke Observatie

Het systeem behandelt de formele pijplijn als een mechanisme voor gedeeltelijke observatie. Het observeert niet de waarheid van elk kandidaatantwoord, maar observeert slechts:

1. Welke genormaliseerde antwoordklassen een welgevormde Lean-stelling bereiken (Getypeerde Dekking).
2. Welke van die klassen succesvol worden bewezen (Bewezen Dekking).
3. Het gewicht van de klasse met het hoogste gewicht die is bewezen, versus het gewicht van de onopgeloste rivaal met het hoogste gewicht (Formele Marge).

Een antwoordklasse wordt gedefinieerd als een groep kandidaatstrings die hetzelfde eindantwoord aanduiden (bijv. $1/2$, $0.5$, $2/4$). Klassen die niet worden geformaliseerd of niet worden bewezen, worden beschouwd als onopgelost, niet automatisch fout.

2.2 Dekking-Diagnostiek

COVCAL berekent vier sleutelmetrieken voor een gegeven probleem $x$:

• Getypeerde Dekking ($C_{typ}$): Het totale gewicht van kandidaatklassen die een welgevormde Lean-stelling hebben bereikt (status: proved, typechecked, of timeout).
• Bewezen Dekking ($C_{prf}$): Het totale gewicht van kandidaatklassen die een door de kernel gecontroleerd bewijs hebben ontvangen.
• Massa van Onopgeloste Rivalen ($R_{unres}$): Het gewicht van de antwoordklasse met het hoogste gewicht die niet is bewezen.
• Formele Marge ($M$): Het verschil tussen het gewicht van de klasse met het hoogste gewicht die is bewezen en de massa van de onopgeloste rivaal.

2.3 Selectie en Certificering

COVCAL accepteert de klasse met het hoogste gewicht die is bewezen, alleen als een vooraf aangekondigde regel op basis van drempelwaarden $(\tau_{typ}, \tau_{prf}, \tau_M)$ wordt voldaan. Als aan de regel niet wordt voldaan, ziet het systeem af (of grijpt het terug naar een niet-formele methode zoals zelf-consistentie).

Om betrouwbaarheid te waarborgen, maakt COVCAL gebruik van certificering van selectief risico op basis van een eindige steekproef. Het garandeert dat, met een waarschijnlijkheid van $1-\delta$, het selectieve risico (foutenpercentage) van geaccepteerde antwoorden ten hoogste $\epsilon$ is. Twee certificeringsregimes worden voorgesteld:

1. Bonferroni-regime: Zoekt over een rooster van drempelwaarden op een kalibratiesplit en past een unie-begrens-correctie toe ($\delta/|T|$) om rekening te houden met de meervoudige vergelijkingen. Dit is conservatief en vereist een hoge signaaldichtheid om haalbaar te zijn.
2. Dev-then-Cal-regime: Selecteert de drempelwaarde op een onafhankelijke ontwikkelingsplit en certificeert deze eenmaal op de kalibratiesplit met behulp van een enkele Clopper-Pearson-begrens ($\delta$). Dit is efficiënter qua steekproefgrootte, maar vereist een strikte scheiding tussen ontwikkelings- en kalibratiegegevens.

2.4 Theoretische Grenzen

Het artikel bewijst dat zonder dekking-diagnostiek (d.w.z. uitsluitend vertrouwend op het bestaan van een bewijs) geen niet-vacuüm punt-voor-punt juistheidscertificaat kan worden afgeleid als er een onopgeloste, niet-equivalente rivaliserende klasse bestaat. Ontbrekend formeel bewijs is geen bewijs van wiskundige onwaarheid; het is bewijs van een onopgeloste status.

3. Belangrijkste Bijdragen

1. Karakterisering van de Dekking-Afgrond: Op de MATH-500-dataset tonen de auteurs aan dat het "bewijs-winnende" antwoord 96% van de tijd correct is bij hoge bewezen dekking, maar slechts 20% bij lage dekking. Dit stelt vast dat Lean-bewijzen alleen betrouwbaar zijn wanneer dekking en marge hoog zijn.
2. Signaalsparsiteit en Trouw: Het formele signaal is spaarzaam en imperfect. Een 7B auto-formalisator bewijst een klasse voor slechts 28% van de problemen. Bovendien onthult een handmatige audit dat slechts $\approx 43\%$ van deze bewijzen trouw is aan het oorspronkelijke probleem (de rest zijn triviale identiteiten of waar maar irrelevante stellingen).
3. COVCAL-methode: Een framework voor selectieve voorspelling dat risico certificeert onder gedeeltelijke observatie. Het behandelt expliciet de asymmetrie van bewijsmislukking en biedt garanties voor een eindige steekproef voor geaccepteerde voorspellingen.
4. Afhangbaarheid van Formalisator: Het artikel toont aan dat de haalbaarheid van certificaten wordt bepaald door de dekking van auto-formalisatie. Een 7B-formalisator levert een signaal dat te spaarzaam is voor het conservatieve Bonferroni-regime (het verwerpt alle 20 bootstrap-partities), terwijl een op het bewijzen gespecialiseerde formalisator (Goedel-Prover-V2-8B) die 79% dekking bereikt, de methode haalbaar maakt op 17/20 partities.

4. Experimentele Resultaten

Experimenten werden uitgevoerd op een gefilterde subset van MATH-500 (378 voorbeelden) met Qwen2.5-Math-7B voor generatie en diverse formalisators voor auto-formalisatie.

• Basisprestaties: Zelf-consistentie alleen bereikt 91% nauwkeurigheid zonder afzien.
• COVCAL-prestaties:
  • Onder het Bonferroni-regime met een 7B-formalisator verwerpt de methode alle invoer (0/20 partities) omdat het signaal te spaarzaam is om aan de strikte unie-begrens te voldoen.
  • Onder het dev-then-cal-regime met de 7B-formalisator worden 12/20 partities gecertificeerd. Het geaccepteerde aandeel is $\approx 21\%$, met een geaccepteerde nauwkeurigheid van 0,93.
  • Met de Goedel-Prover-V2-8B (gespecialiseerde formalisator) stijgt de bewezen dekking naar 79%. Bonferroni wordt haalbaar op 17/20 partities, waarbij $\approx 48\%$ van de problemen wordt geaccepteerd met een geaccepteerde nauwkeurigheid van 0,98.
• Audit van Trouw: Een handmatige audit van 45 gestratificeerde voorbeelden toonde aan dat hoewel 73,6% van de bewezen stellingen niet-triviaal en correct was, slechts 43% trouw was aan de probleemstelling. Veel "bewezen" stellingen waren waar zij-facten of triviale identiteiten die de beperkingen van het probleem niet vastlegden.

5. Betekenis en Beweringen

Het artikel beweert dat de primaire bijdrage een precieze uiteenzetting is van wanneer en met welke formalisator een partieel formeel signaal kan worden vertrouwd onder risicobesturing, in plaats van simpelweg de ruwe nauwkeurigheid te verbeteren.

• Risicobesturing boven Ruwe Nauwkeurigheid: Aangezien zelf-consistentie al 91% nauwkeurig is, ligt de waarde van COVCAL in het vermogen om een certificaat te bieden voor het subset van antwoorden dat het accepteert, waarbij wordt onderscheid gemaakt tussen "geverifieerd" en "onopgelost" in plaats van "correct" en "onjuist".
• Omgaan met Gedeeltelijke Observaties: Het werk herformuleert formele verificatie als een probleem van selectieve voorspelling waarbij ontbrekende bewijzen worden behandeld als onopgeloste kandidaten, waardoor het verkeerd labelen van correct redeneren als onjuist als gevolg van formalisatiefouten wordt voorkomen.
• Afhankelijkheid van Specialisatie: De resultaten benadrukken dat ruwe modelgrootte geen vervanging is voor specialisatie. Een op het bewijzen gespecialiseerde formalisator presteert aanzienlijk beter dan een groter generalistisch model in termen van bewijsdekking, wat de bindende beperking is voor certificeerbare risicobesturing.

De auteurs concluderen dat COVCAL dient als een conservatieve interface voor het gebruik van Lean als beoordelaar: het is alleen haalbaar en informatief wanneer de auto-formalisator voldoende antwoordmassa dekt om een risicocertificaat te ondersteunen, maar het garandeert niet dat alle antwoorden worden geverifieerd.