Learning to Disprove: Formal Counterexample Generation with Large Language Models

Dit artikel introduceert een methode om grote taalmodellen te trainen in het genereren van formeel geverifieerde tegenvoorbeelden in Lean 4, middels een symbolische mutatiestrategie en een multi-beloning expertiteratiekader dat de prestaties op wiskundige redeneertaken aanzienlijk verbetert.

De kern

Titel: Hoe AI leert om fouten te vinden in plaats van alleen maar antwoorden te geven

Stel je voor dat wiskunde een enorme, ingewikkelde puzzel is. Tot nu toe hebben kunstmatige intelligenties (AI) vooral getraind om de oplossing te vinden. Ze zijn als een supersterke detective die altijd de juiste dader probeert te vinden. Maar wat als de "dader" eigenlijk niet bestaat? Wat als de hele theorie die we proberen op te lossen, gewoon verkeerd is?

Dat is waar dit nieuwe onderzoek over gaat. De onderzoekers hebben een manier bedacht om AI niet alleen te leren bewijzen dat iets waar is, maar ook te leren ontmaskeren waarom iets onwaar is. Ze noemen dit "leren om te weerleggen".

Hier is hoe het werkt, vertaald in alledaagse termen:

1. Het probleem: De AI is te beleefd

Stel je een AI voor als een student die altijd denkt dat de leraar gelijk heeft. Als de leraar zegt: "Alle zwanen zijn wit", zoekt de AI naar zwanen om dit te bewijzen. Maar de AI vergeet vaak om te kijken of er misschien een zwarte zwaan bestaat.

In de echte wereld van wiskunde zijn tegenvoorbeelden (zoals een zwarte zwaan) cruciaal. Als je een theorie wilt testen, is het vinden van één foutje vaak belangrijker dan het vinden van duizend bewijzen. Helaas waren de huidige AI-modellen hier heel slecht in, omdat er te weinig oefenmateriaal voor was.

2. De oplossing: De "Mutatie-methode" (Het koken van een nieuwe soep)

Het grootste probleem was: waar haal je genoeg oefenmateriaal vandaan? Er zijn niet genoeg bestaande wiskundige problemen die al weten dat ze fout zijn.

De onderzoekers bedachten een slimme truc, die ze "symbolische mutatie" noemen.

• De analogie: Stel je hebt een perfect gerecht (een bewezen wiskundestelling) met drie belangrijke ingrediënten: A, B en C. Als je A, B en C gebruikt, wordt het gerecht perfect.
• De truc: De AI pakt nu het recept en doet er expres één ingrediënt uit (bijvoorbeeld B).
• Het resultaat: Nu is het gerecht waarschijnlijk niet meer lekker (de stelling is nu fout). De AI moet nu een tegenvoorbeeld vinden: een situatie waarin A en C wel werken, maar het gerecht toch mislukt omdat B ontbreekt.

Door dit systematisch te doen met duizenden bestaande theorieën, hebben ze 575.000 nieuwe oefenproblemen gegenereerd. Het is alsof ze een fabriek hebben gebouwd die automatisch "valkuilen" creëert om de AI in te laten vallen, zodat de AI leert hoe hij uit die valkuilen kan klimmen.

3. De training: Twee prijzen in plaats van één

Normaal gesproken krijgt een AI alleen een "prikje" (beloning) als hij het hele probleem perfect oplost. Als hij halverwege vastloopt, krijgt hij niets. Dit is als een speler in een videospel die pas punten krijgt als hij de hele game uitgespeeld heeft; als hij in level 1 vastloopt, leert hij niets.

De onderzoekers bedachten een meervoudige beloningssysteem:

• Prijs 1: Heeft de AI een goed voorbeeld gevonden dat laat zien dat de theorie fout is? (Zelfs als de formele bewijsvoering nog niet perfect is).
• Prijs 2: Is het formele bewijs (in de taal van de computer, genaamd Lean 4) correct?

Dit zorgt ervoor dat de AI ook beloning krijgt voor de halve goede stappen. Het is alsof je een kind leert fietsen: je geeft niet alleen een snoepje als het kind de hele weg rijdt, maar ook als het even goed balanceert zonder te vallen. Hierdoor leert de AI veel sneller en efficiënter.

4. Het resultaat: Een AI die beter "niet" kan zeggen

De getrainde AI is nu een stuk slimmer geworden. In tests bleek dat deze nieuwe AI 47% tot 74% beter presteerde dan de beste bestaande modellen.

• Vroeger: De AI probeerde wanhopig een onmogelijke stelling te bewijzen en gaf uiteindelijk op.
• Nu: De AI denkt: "Wacht even, deze stelling klopt niet. Hier is een voorbeeld waar het misgaat, en hier is het bewijs."

Waarom is dit belangrijk?

Dit is niet alleen leuk voor wiskundepuzzels. Het helpt AI om kritischer na te denken. In plaats van blindelings te vertrouwen op patronen, leert de AI om zijn eigen redeneringen te testen en fouten te vinden. Dit is een enorme stap in het maken van AI die betrouwbaarder is, niet alleen in wiskunde, maar ook in het oplossen van complexe problemen in de echte wereld.

Kortom: De onderzoekers hebben een AI getraind die niet alleen een "ja" kan zeggen, maar ook een goed onderbouwd "nee" kan geven, en dat bewijzen. Ze hebben de AI leren denken als een echte kritische wetenschapper.

Technische samenvatting

Titel: Learning to Disprove: Formele Generatie van Tegenvoorbeelden met Grote Taalmodellen

1. Het Probleem

Wiskundig redeneren vereist twee complementaire vaardigheden: het construeren van rigoureuze bewijzen voor ware stellingen en het ontdekken van tegenvoorbeelden (counterexamples) om valse beweringen te weerleggen. Hoewel de huidige AI-ontwikkeling in de wiskunde zich bijna uitsluitend richt op het genereren van formele bewijzen, wordt de even belangrijke taak van het vinden van tegenvoorbeelden genegeerd.

Er zijn twee fundamentele uitdagingen bij het trainen van Large Language Models (LLMs) voor deze taak:

1. Schaarste aan trainingsdata: Er is een gebrek aan grote, gestructureerde datasets voor tegenvoorbeelden. Het enige bestaande dataset (CounterMath) bevat slechts ongeveer 1.200 natuurlijke taalproblemen, wat ontoereikend is voor effectief fine-tuning.
2. Schaarse beloningssignalen (Sparse Rewards): Bij complexe problemen faalt een model vaak om een correct tegenvoorbeeld te vinden. In traditionele reinforcement learning-leeromgevingen verdwijnt het beloningssignaal dan volledig, wat leidt tot een plateau in de prestaties en het model in een lokaal optimum laat steken.

2. Methodologie

De auteurs stellen een geïntegreerd framework voor dat bestaat uit twee hoofdfasen: symboolische mutatie voor datageneratie en multi-beloning geleide training.

A. Symboolische Mutatie voor Datageneratie (Data Synthesis)
Om het data-tekort op te lossen, ontwikkelen de auteurs een strategie om grote hoeveelheden trainingsdata te synthetiseren uit bestaande, bewijsbare stellingen:

• Bron: Ze verzamelen duizenden bewijsbare stellingen uit bibliotheken zoals Mathlib, Leanworkbook, MiniF2F en PutnamBench.
• Mutatie: Voor een universele stelling van de vorm $\forall x, H_1(x) \land H_2(x) \to C(x)$ wordt een noodzakelijke hypothese (bijv. $H_1$) systematisch verwijderd.
• Resultaat: De gereduceerde stelling ($H_2(x) \to C(x)$) is nu onwaar (invalidated), wat betekent dat er een tegenvoorbeeld bestaat ($\exists x, H_2(x) \land \neg C(x)$).
• Validatie: Het Lean 4 theorema-prover wordt gebruikt om te verifiëren dat de originele hypothese inderdaad noodzakelijk was en dat de gegenereerde mutatie grammaticaal correct is.
• Output: Deze methode genereerde 575.000 unieke tegenvoorbeeldproblemen.

B. Multi-Beloning Geleide Training (Expert Iteration)
Om het probleem van schaarste beloning op te lossen, introduceren ze een multi-beloningssysteem binnen een Expert Iteration pipeline:

• Twee taken: Voor een gegenereerd tegenvoorbeeld $x^*$ moet het model twee bewijzen leveren:
  1. Het bewijs dat $x^*$ de gemuteerde stelling weerlegt.
  2. Het bewijs dat $x^*$ de verwijderde hypothese ($\neg H_1(x^*)$) weerlegt.
• Beloningsstructuur: In plaats van alleen te belonen als het einddoel (de gemuteerde stelling) wordt bewezen, wordt er ook beloond voor het bewijzen van de "dropped hypothesis". Omdat het bewijzen van de verwijderde hypothese vaak eenvoudiger is, blijft er een geldig beloningssignaal over, zelfs als het model het moeilijkere doel nog niet volledig heeft bereikt.
• Fine-tuning: De modellen worden getraind met gewogen data, waarbij de gewichten gebaseerd zijn op de succesvolle verificatie van beide bewijzen door de Lean 4 prover.

3. Belangrijkste Bijdragen

1. Formele Definitie: Het formaliseren van het genereren van tegenvoorbeelden als een taak waarbij LLMs niet alleen een kandidaat moeten voorstellen, maar ook een formeel, automatisch verifieerbaar bewijs in Lean 4 moeten leveren.
2. Symboolische Mutatiestrategie: Een nieuwe methode om grote, diverse datasets van tegenvoorbeelden te synthetiseren door systematisch hypothese te verwijderen uit bewijsbare stellingen, wat de schaalbaarheid van trainingsdata mogelijk maakt.
3. Multi-Beloning Framework: Een innovatieve trainingsaanpak die het "sparse reward"-probleem oplost door extra beloningen te geven voor het valideren van de verwijderde hypothese, waardoor het leerproces robuuster wordt.
4. Nieuwe Benchmarks: Het verzamelen en publiceren van drie nieuwe benchmarks voor het evalueren van tegenvoorbeeldgeneratie, verificatie van geautomatiseerde formalisatie en verificatie van redeneerstappen.

4. Resultaten

De auteurs testten hun gefinetuned model op de nieuwe benchmarks en vergeleken het met de beste bestaande modellen (zoals DeepSeek-R1, Goedel-prover, en proprietary modellen zoals GPT-4 en Gemini).

• Prestatieverbetering: Het gefinetuned model vertoonde significante verbeteringen. In vergelijking met de sterkste baseline (DeepSeek-Prover-v2) werd een relatieve verbetering van 47% tot 74% bereikt in de pass@1 succesratio.
• Convergentie: De multi-beloning training convergeerde sneller en bereikte een hogere eindprestatie dan training met een enkele beloning (single-reward).
• Benchmarks: Het model presteerde overtuigend op drie taken:
  1. FOR-COUNTER: Identificatie van tegenvoorbeelden (95 meer correcte antwoorden dan de beste baseline).
  2. VERI-REASON: Verificatie van redeneerstappen.
  3. VERI-FORMALIZE: Verificatie van geautomatiseerde formalisatie.
• Efficiëntie: De mutatiestrategie genereerde gemiddeld 1,65 tot 2,48 nieuwe problemen per bronstelling met een zeer korte uitvoeringstijd (0,3 - 0,71 seconden per stelling).

5. Significantie

Dit werk vult een cruciale lacune in de AI-onderzoek voor wiskundig redeneren. Door zich te richten op het "disproven" (weerleggen) in plaats van alleen het "proven" (bewijzen), biedt het framework modellen de mogelijkheid om hun eigen redenering te verifiëren en te corrigeren.

• Zelfreflectie: Het genereren van tegenvoorbeelden is essentieel voor zelfreflectie; het dwingt het model om na te denken over de grenzen van een bewering en edge cases te onderzoeken.
• Toekomstige Toepassingen: De methode kan dienen als een praktische "copilot" voor wiskundigen om conjectures te valideren en helpt bij het ontwikkelen van robuustere AI-systemen die minder gevoelig zijn voor fouten in hun logische deductie.
• Open Source: De auteurs maken hun code, data en modellen openbaar, wat de gemeenschap in staat stelt om verder te bouwen op dit werk in de richting van zelf-corrigerende wiskundige AI.

Samenvattend biedt dit paper een solide oplossing voor de uitdagingen van data-schaarste en schaarste beloning in het domein van formele wiskundige redenering, en bewijst dat het trainen van LLMs om te "leren weerleggen" een krachtige route is naar betere wiskundige intelligentie.