Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Dit artikel introduceert de Conjecturing-Proving Loop (CPL), een pijplijn die gebruikmaakt van in-context learning door een LLM iteratief zijn eigen formeel geverifieerde stellingen en bewijzen in Lean 4 aan te reiken om de ontdekkingskans en het succes van nieuwe, moeilijk te bewijzen wiskundige conjecturen aanzienlijk te verbeteren.

De kern

Stel je voor dat je probeert een zeer slimme, maar licht vergeetachtige robot te leren hoe complexe wiskundepuzzels op te lossen. De robot is een Large Language Model (LLM) en de puzzels zijn formele wiskundige bewijzen geschreven in een strikte computertaal genaamd Lean.

Het artikel introduceert een nieuwe manier om deze robot te leren, genaamd de Conjecturing-Proving Loop (CPL). Hieronder wordt uitgelegd hoe dit werkt, met behulp van eenvoudige analogieën:

Het Probleem: De "Gok-en-Controle" Valstrik

Meestal vragen mensen aan AI om wiskunde te doen door het te vragen om een puzzel te raden en deze in één keer op te lossen.

• De Analogie: Stel je voor dat je een student vraagt: "Schrijf een wiskundevraag op en los deze direct op."
• Het Probleem: De student wordt lui. Ze schrijven makkelijke vragen (zoals "2 + 2 = 4") omdat die makkelijk op te lossen zijn. Ze vermijden moeilijke problemen omdat ze weten dat ze misschien falen. De AI eindigt met het genereren van duizenden makkelijke, saaie bewijzen en mist de moeilijke, interessante.

De Oplossing: De "Tweestapsdans" (CPL)

De auteurs splitsen het proces op in twee distincte rollen: een Conjecturer (de Idee-Generator) en een Prover (de Oplosser).

1. De Conjecturer (De Architect): Dit deel van de AI kijkt naar een bibliotheek met bestaande wiskunderegels en bedenkt nieuwe ideeën (conjecturen). Het probeert ze nog niet op te lossen; het schrijft ze gewoon op.
2. De Prover (De Bouwer): Dit deel neemt de ideeën en probeert een bewijs daarvoor te bouwen. Als het faalt, probeert het het opnieuw. Het blijft proberen totdat het ofwel slaagt ofwel zijn pogingen opgebruikt heeft.
3. De Bibliotheek (Het Geheugen): Elke keer dat de Prover succesvol een bewijs bouwt, wordt dat bewijs toegevoegd aan de bibliotheek.

Het Magische Ingrediënt: In-Context Learning
Hier komt het slimme deel: De Prover kijkt niet alleen naar de originele wiskunderegels. Het kijkt naar de bibliotheek met bewijzen die het tijdens de huidige sessie al succesvol heeft gebouwd.

• De Analogie: Stel je voor dat een student een toets maakt. Op de oude manier moest het zich alleen baseren op wat het voor de toets begon had gememoriseerd. Op deze nieuwe manier mag de student, elke keer dat het een probleem correct oplost, zijn eigen oplossing lezen voordat het het volgende probleem aanpakt. Het leert de "trucs" en "strategieën" van zijn eigen recente successen.

Wat Ze Vonden

De onderzoekers testten dit op wat lastige topologieconcepten (een tak van wiskunde die zich bezighoudt met vormen en ruimten) die de AI nog niet goed kende.

• Kwantiteit versus Kwaliteit: De oude methode (gokken en in één keer oplossen) genereerde meer totale stellingen, maar deze waren voornamelijk kort en makkelijk. De nieuwe methode (CPL) genereerde minder totale stellingen, maar ze waren veel moeilijker en langer.
• De Grote Winst: De nieuwe methode slaagde erin een specifieke, moeilijke stelling over "alpha-open sets" te ontdekken die de oude methode nooit vond, zelfs niet na 20 pogingen.
• Leren van Succes: Wanneer de AI de bibliotheek van zijn eigen eerdere bewijzen kreeg als "spiekbriefje" (context), kon het moeilijke stellingen bewijzen die het zonder die context niet kon oplossen. Zelfs wanneer de AI de stelling niet in gewoon Engels kon bewijzen, kon het het bewijzen in Lean-code zodra het vergelijkbare succesvolle bewijzen had gezien.

De Conclusie

Het artikel beweert dat door het "idee-genereren" te scheiden van het "bewijs-oplossen" en de AI in real-time te laten leren van zijn eigen geverifieerde successen, we het kunnen laten moeilijkere, complexere wiskundige waarheden ontdekken die het anders zou missen. Het is alsof je de AI een voorsprong geeft door het zijn eigen huiswerk te laten bestuderen voordat het het eindexamen maakt.

Opmerking: Het artikel richt zich strikt op deze methode voor het genereren en verifiëren van wiskundige stellingen. Het beweert niet dat deze methode werkt voor medische diagnose, financiële voorspelling of andere toepassingen in de echte wereld buiten de formele wiskunde.

Technische samenvatting

Technische Samenvatting: Het Ontdekken van Nieuwe Stellingen via LLM's met In-Context Bewijsleer in Lean

Probleemstelling
Grote Taalmodellen (LLMs) hebben veelbelovende resultaten laten zien in formeel stellingbewijs, maar staan voor aanzienlijke uitdagingen: ze kunnen hallucineren, en het gelijktijdig genereren van een wiskundige conjectuur en het bijbehorende bewijs leidt vaak tot convergentie naar triviale of eenvoudige stellingen. Bestaande benaderingen vertrouwen doorgaans op Supervised Fine-Tuning (SFT) of Reinforcement Learning met Verifieerde Beloningen (RLVR), wat uitgebreide trainingsdata vereist en moeilijk toepasbaar is op gesloten bronmodellen. Bovendien worstelen huidige methoden vaak om "moeilijk te bewijzen" stellingen te ontdekken, omdat de waarschijnlijkheid van het genereren van een stelling zwaar wordt gewogen door de directe succeskans van het bewijzen ervan, waardoor het zoekproces instort in simpele, korte bewijzen.

Methodologie: De Conjectureren-Bewijzen-lus (CPL)
De auteurs stellen de Conjectureren-Bewijzen-lus (CPL) voor, een pijplijn ontworpen om automatisch wiskundige conjecturen te genereren en deze te verifiëren in Lean 4. Het kader scheidt het genereren van conjecturen van het genereren van bewijzen, waarbij een bibliotheek van eerder geverifieerde stellingen als context wordt gebruikt voor beide fasen.

De pijplijn werkt via vier hoofdcomponenten: een Conjecturer (LLM-agent), een Bewijzer (LLM-agent), een Lean Server en een Bibliotheek (Lean-code data).

1. Conjectuur-fase: De Conjecturer genereert nieuwe wiskundige uitspraken in Lean 4-formaat op basis van de huidige bibliotheek. Hij vraagt de Lean Server om syntactische geldigheid en originaliteit te verifiëren (controleer of de uitspraak niet al bewijsbaar is door bestaande stellingen in Mathlib4 of de huidige bibliotheek).
2. Bewijs-fase: Voor elke geldige conjectuur probeert de Bewijzer een formeel bewijs te construeren. Cruciaal is dat de Bewijzer de bibliotheek (bevattende eerder geverifieerde stellingen en bewijzen) als context krijgt. Dit stelt de LLM in staat om bewijsstrategieën te leren via in-context learning zonder modelhertraining. De Bewijzer iteratieert tot een maximum aantal pogingen (in experimenten ingesteld op 16), waarbij foutberichten van de Lean Server worden gebruikt om zijn pogingen te verfijnen.
3. Iteratie: Geverifieerde paren van conjecturen en bewijzen worden toegevoegd aan de bibliotheek, die vervolgens als context dient voor daaropvolgende iteraties.

Deze scheiding stelt het systeem in staat om zoekresources toe te wijzen op basis van bewijsmoeilijkheid. In tegenstelling tot een eenvoudige lus (SL) waarbij een uitspraak en bewijs gelijktijdig worden gegenereerd, probeert CPL meerdere bewijzen voor een enkele uitspraak voordat deze wordt verworpen. Dit verschuift de verdeling van gegenereerde stellingen naar die welke bewijsbaar maar moeilijk zijn, in plaats van die welke slechts makkelijk te bewijzen zijn.

Belangrijkste Bijdragen

1. Pijplijnvoorstel: De introductie van CPL, een kader dat het genereren van conjecturen ontkoppelt van het genereren van bewijzen, waardoor de ontdekking van langere, complexere bewijzen mogelijk wordt.
2. In-Context Learning voor Gesloten Bronmodellen: Het aantonen dat gesloten bron-LLMs (specifiek ChatGPT-o3) hun bewijsvaardigheden kunnen verbeteren door in-context learning van hun eigen eerder geverifieerde output, waardoor updates van parameters of fine-tuning overbodig worden.
3. Theoretische en Empirische Validatie: Het paper biedt een theoretisch model dat aantoont dat CPL de kans vergroot op het genereren van moeilijk te bewijzen stellingen in vergelijking met kaders voor gelijktijdige generatie. Experimenteel wordt bevestigd dat CPL succesvol een specifiek onderzoeksstadium-stelling herontdekte die het basiskader niet vond.

Experimentele Resultaten
De auteurs evalueerden CPL tegen een Simple Loop (SL) baseline met topologische noties (semi-openheid, $\alpha$-openheid en preopenheid) die binnen Mathlib zijn gedefinieerd maar nog niet in de bibliotheek zijn opgenomen. Het doel was de stelling dat de doorsnede van twee $\alpha$-open verzamelingen $\alpha$-open is.

• Ontdekkingspercentage: In 20 experimentele runs ontdekte CPL de doelstelling 5 keer. Daarentegen slaagde het SL-kader, dat gemiddeld aanzienlijk meer stellingen genereerde (328 versus 106), er niet in om de doelstelling ook maar één keer te genereren. De exacte toets van Fisher bevestigde dat dit verschil statistisch significant was ($p = 0,024$).
• Bewijslengte: CPL genereerde stellingen met aanzienlijk langere bewijzen (in aantal tekens) in vergelijking met SL, wat de theoretische claim ondersteunt dat het kader de focus verschuift naar moeilijkere bewijzen.
• Effectiviteit van Context:
  • Opnieuw Bewijzen: Bij het opnieuw bewijzen van gegenereerde stellingen verhoogde het verstrekken van de bibliotheek als context het succespercentage van 91% naar 99% ($p = 4 \times 10^{-35}$).
  • Doelstelling: Bij het proberen om de doelstelling over de doorsnede van $\alpha$-open verzamelingen opnieuw te bewijzen, slaagde de bewijzer 7 keer in 80 pogingen wanneer de gegenereerde bibliotheek als context werd verstrekt. Zonder de bibliotheek faalde hij 100% van de tijd.
  • Natuurtaalbasis: Toen werd gevraagd om de stelling in natuurlijke taal te bewijzen, oordeelde ChatGPT-4o de stelling vaak als onwaar of leverde het onjuiste bewijzen, en ChatGPT-o3 oordeelde consequent dat het onwaar was, wat aangeeft dat de stelling buiten de vooraf getrainde kennis van de modellen viel. Het succes in Lean 4 werd toegeschreven aan in-context learning van bewijsstrategieën uit de gegenereerde bibliotheek.

Betekenis en Claims
Het paper claimt dat CPL effectief de beperking van LLM's in het ontdekken van niet-triviale stellingen aanpakt door in-context learning van zelfgegenereerde geverifieerde bewijzen te benutten. De auteurs benadrukken dat deze benadering toelaat tot automatische uitbreiding van formele wiskundige bibliotheken (zoals Mathlib) door proposities te genereren over gegeven noties die mogelijk niet expliciet bekend zijn bij de LLM. Het werk suggereert dat het scheiden van de conjectureren- en bewijzenfasen, gecombineerd met iteratieve contextverrijking, een levensvatbare strategie is voor neurale stellingbewijzen, met name voor gesloten bronmodellen waar traditionele trainingsmethoden niet van toepassing zijn. De auteurs houden een bescheiden standpunt aan, noteren dat hoewel het kader een bekende onderzoeksstadium-stelling succesvol herontdekte, toekomstig werk nodig is om het generatieproces te verfijnen voor diepere en inzichtelijker wiskundige uitspraken.