DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

1. Probleemstelling

Geautomatiseerd stellingbewijzen (ATP) heeft aanzienlijke vooruitgang geboekt met Large Language Models (LLM's) en formele bewijshulpmiddelen zoals Lean. Echter, de huidige state-of-the-art systemen staan voor twee kritieke beperkingen:

• Gebrek aan Generalisatie: De meeste benaderingen behandelen elke stelling geïsoleerd. Hoewel ze problemen kunnen ontleden in tussenstappen, zijn deze stappen vaak zeer specifiek voor het individuele probleem en generaliseren ze niet over verschillende stellingen heen.
• Inefficiëntie: Bestaande methoden vertrouwen ofwel op vaste, statische lemma-bibliotheken (wat de aanpasbaarheid beperkt) of synthetiseren nieuwe tussen-lemmas voor elke afzonderlijke probleeminstantie. Dit leidt tot redundante berekening, langere bewijzen en hoger tokenverbruik, aangezien het systeem er niet in slaagt om "vaardigheden" (lemmas) die uit eerdere bewijzen zijn geleerd, te accumuleren en opnieuw te gebruiken.

Het artikel betoogt dat huidige systemen falen in het nabootsen van menselijke wiskundige praktijk, waar wiskundigen systematisch een kernset van overdraagbare lemmas accumuleren, abstracteren en hergebruiken om nieuwe problemen efficiënt op te lossen.

2. Methodologie: Het DreamProver Framework

DreamProver is een agentisch framework dat is ontworpen om een herbruikbare bibliotheek van lemmas te leren en te laten evolueren via een iteratief "Wake-Sleep" paradigma, geïnspireerd door cognitieve leerteorieën en het DreamCoder-algoritme. Het systeem werkt in afwisselende cycli:

A. De Wake-fase (Stellingontdekking & Ontleding)

In deze fase probeert de agent stellingen uit een trainingsset te bewijzen met behulp van de huidige lemma-bibliotheek.

• Identificatie van Leerbare Stellingen: Het systeem probeert stellingen direct te bewijzen met de bibliotheek. Als dit lukt, wordt de stelling gemarkeerd als "leerbaar", wat impliceert dat de bibliotheek voldoende is voor dat domein.
• Ontdekking van Tussenstellingen: Als een stelling niet direct bewezen kan worden, ontleedt het systeem deze recursief in eenvoudigere sub-problemen (sub-stellingen).
  • Het genereert een formeel bewijsschets.
  • Het extraheert onbewezen tussen-doelen (gemarkeerd met sorry) als zelfstandige stellingen.
  • Het valideert deze geëxtraheerde stellingen door te proberen het volledige bewijs opnieuw samen te stellen met behulp van de schets en de nieuwe kandidaten.
• Resultaat: Het systeem accumuleert een set "leerbare stellingen" (tussenresultaten) afgeleid van de trainingsdata.

B. De Sleep-fase (Lemma-abstractie & Bibliotheekoptimalisatie)

In deze fase verwerkt het systeem de opgehoopte ervaringen om de lemma-bibliotheek te laten evolueren.

• Semantische Clustering: Het systeem annoteert de verzamelde tussenstellingen met beschrijvingen in natuurlijke taal (sub-domein, moeilijkheidsgraad, relevante concepten). Vervolgens worden deze beschrijvingen ingebed en geclusterd met K-Means op basis van semantische gelijkenis.
• Lemma-abstractie: Voor elke cluster wordt een LLM geprompted om een kandidaat-lemma te genereren dat de specifieke stellingen in die cluster generaliseert.
• Structurele Validatie: Om ervoor te zorgen dat de geabstracteerde lemmas toepasbaar zijn, berekent het systeem de structurele gelijkenis (met behulp van tree edit distance op bomen van eerste-orde logische expressies) tussen de kandidaat-lemma en de stellingen in de cluster. Lemmas die een gelijkenisdrempel overschrijden, worden behouden.
• Bibliotheekupdate (Vergeten & Deduplicatie):
  • Deduplicatie: Nieuwe lemmas worden vergeleken met de bestaande bibliotheek met behulp van tree edit distance; sterk vergelijkbare (dubbele) lemmas worden verworpen.
  • Vergeten: Om een compacte bibliotheek te behouden, hanteert het systeem een "Least Recently Used" (LRU) strategie. Lemmas die in recente wake-fases niet vaak zijn gebruikt, worden geschrapt zodra de bibliotheek zijn capaciteit bereikt.
  • Verificatie: Overgebleven kandidaat-lemmas worden formeel geverifieerd om ervoor te zorgen dat ze bewijsbaar zijn.

C. Inference

Tijdens inferentie op ongezette testproblemen maakt DreamProver gebruik van de geëvolueerde bibliotheek. Het probeert eerst directe bewijsgeneratie. Als dat faalt, hanteert het een "Sketch-and-Prove"-workflow, waarbij de bibliotheek wordt gebruikt om de generatie van bewijsschetsen en het oplossen van sub-doelen te sturen.

3. Belangrijkste Bijdragen

1. Wake-Sleep Paradigma voor ATP: De eerste toepassing van een continue, iteratieve wake-sleep cyclus specifiek voor het laten evolueren van overdraagbare lemma-bibliotheken in formeel stellingbewijzen.
2. Leren van Overdraagbare Lemmas: In tegenstelling tot eerdere werken (zoals LEGO-Prover) die moeite hadden om effectief hergebruik aan te tonen, cluster en abstract DreamProver tussenresultaten expliciet tot algemene lemmas, waardoor een persistente, hoogwaardige kennisbank ontstaat.
3. Efficiëntiemechanismen: De introductie van een "vergeten"-mechanisme (LRU-schrapping) en structurele deduplicatie zorgt ervoor dat de bibliotheek compact blijft (<100 lemmas), wat contextvenster-overloop voorkomt en hoge ophaalrelevantie handhaaft.
4. Domeingeneralisatie: Het framework is ontworpen om te werken over diverse wiskundige domeinen heen, waaronder die welke ondervertegenwoordigd zijn in LLM-trainingsdata.

4. Experimentele Resultaten

De auteurs evalueerden DreamProver over vijf wiskundige domeinen: Ongelijkheden, Getaltheorie, Combinatoriek, Vlakke Meetkunde en Machine Learning Theorie.

• Prestatiewinst:

  • DreamProver verbeterde de bewijssuccespercentages met gemiddeld 61% ten opzichte van eerdere state-of-the-art (SOTA) systemen zoals Hilbert en Goedel-Prover-V2.
  • In specifieke domeinen waren de verbeteringen drastisch: 114% in Getaltheorie en 50% in Combinatoriek.
  • In ondervertegenwoordigde domeinen (Vlakke Meetkunde, ML Theorie) loste DreamProver aanzienlijk meer instanties op dan propriëtaire LLM's (bijvoorbeeld het oplossen van 14-16 meetkundige problemen op Olympiade-niveau waar baseline LLM's 0-3 oplostten).

• Efficiëntie en Kwaliteit:

  • Tokenreductie: DreamProver verlaagde het output tokenverbruik met gemiddeld 48% ten opzichte van SOTA agentische systemen.
  • Bewijsconcisie: Genereren bewijzen waren gemiddeld 50% korter, wat wijst op hogere kwaliteit en betere structuur.
  • Lemma-hergebruik: Analyse toonde aan dat 58% van de lemmas gegenereerd tijdens het trainen werd hergebruikt in testsets, wat bijdroeg aan 71% van alle succesvol bewezen stellingen.

• Ablatiestudies:

  • Het verwijderen van de iteratieve wake-sleep verfijning (evolutie in één doorgang) liet de succespercentages significant dalen (van 104 naar 76 opgeloste problemen).
  • Het verwijderen van semantische clustering resulteerde in een te grote, onbeheersbare bibliotheek, wat de prestaties zelfs onder een baseline zonder bibliotheek bracht.

5. Betekenis

DreamProver vertegenwoordigt een verschuiving van "one-shot" of "statische-bibliotheek" stellingbewijzen naar continue, zelfverbeterende leerprocessen.

• Overbrugging van de Kloof: Het overbrugt effectief de kloof tussen de ruwe redeneerkracht van LLM's en de gestructureerde, herbruikbare kennis die nodig is voor complexe wiskundige redenering.
• Schaalbaarheid: Door een compacte, overdraagbare bibliotheek te leren, verlaagt het systeem de rekenkosten voor het bewijzen van nieuwe stellingen, waardoor hoogwaardige formele verificatie toegankelijker wordt.
• Mensachtig Leren: Het framework nabootst menselijke cognitieve processen (ervaring opdoen, principes abstracteren en irrelevante details vergeten), wat wijst op een levensvatbaar pad naar robuustere en generaliseerbaardere AI-redeneersystemen.

Concluderend toont DreamProver aan dat het expliciet leren en verfijnen van een bibliotheek van herbruikbare lemmas een kritieke factor is in het bereiken van state-of-the-art prestaties in geautomatiseerd stellingbewijzen, met name in complexe en datagebrekkige wiskundige domeinen.