Technisch overzicht: Zelfgestuurde ontdekking van stellingen in een formeel axiomatisch systeem

Probleemstelling

Hoewel recente AI-systemen, met name Large Language Models (LLM's), aanzienlijke vooruitgang hebben getoond in wiskundig redeneren, vertrouwen zij grotendeels op door mensen verstrekte priors zoals wiskundige teksten, code en bestaande stellingbibliotheken. Een cruciale openstaande vraag blijft: Kan een agent autonoom nuttige stellingen ontdekken uitsluitend vanaf de primitieve regels van een formeel axiomatisch systeem, zonder toegang tot menselijke voorkennis, bestaande stellingbibliotheken of trainingsprobleemsets?

Huidige methoden zijn vaak afhankelijk van door mensen geconstrueerde kennis om redeneren te bootstrappen. Zelfverbeterende agenten in axiomatische domeinen vertrouwen ook vaak op externe beoordelaars om de bruikbaarheid van ontdekte stellingen te evalueren. Dit artikel onderzoekt of een agent niet alleen stellingen kan ontdekken, maar ook in staat is om "nuttige" stellingen te identificeren en te benutten om zijn eigen bewijszoektocht en de prestaties van externe redeneersystemen te verbeteren, waarbij uitsluitend wordt vertrouwd op axioma's en inferentieregels.

Methodologie

1. Formele setting: Hilbert-systeem als stackmachine

De auteurs instantiëren het probleem binnen een Hilbert-axioma systeem voor propositielogica. Het systeem is doelbewust minimaal en bestaat uit:

• Drie Axioma's:
  • $Ax1: A \to (B \to A)$ (Verzwakking)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distributie)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Contrapositie)
• Eén Inferentieregel: Modus Ponens (MP), waarbij $Y$ wordt afgeleid uit $X$ en $X \to Y$.

Om leren te faciliteren, formuleren de auteurs bewijsvoering als een deterministisch, doelgeconditioneerd stackmachine-beslissingsproces $(S, A, s_0, P)$:

• Toestand ($S$): Een eindige stack van formules.
• Acties ($A$): Het pushen van instanties van $Ax1, Ax2, Ax3$ op de stack, of het toepassen van Modus Ponens (MP).
• Mechanisme: De MP-actie gebruikt Hindley–Milner unificatie. Als het bovenste element van de stack unificeert met $X \to Y$ en het element eronder unificeert met $X$, worden beide gepopt en wordt $Y$ gepusht.
• Succes: Een bewijs is succesvol als de stack een enkele formule bevat die overeenkomt met het doel (target goal).

2. Algoritme voor zelfgestuurde ontdekking van stellingen

De kernbijdrage is een algoritme dat afwisselend tussen bewijszoektocht en extractie van nuttige stellingen werkt, waarbij een bibliotheek van stellingen wordt opgebouwd die dienen als lemma's voor toekomstige zoektochten.

A. Doelgeconditioneerd beleidsleren (Policy Learning)

De agent leert een beleid $\pi_\theta(A|S, g)$ om de volgende actie te voorspellen gegeven de huidige stack $S$ en een doel $g$.

• Hindsight Learning: Tijdens een zoekepisode wordt elke toestand waarin de stack een enkele formule $f_t$ bevat, behandeld als een "bereikte stelling", ongeacht of dit de oorspronkelijke doelstelling was.
• Trainingssignaal: Het actieprefix dat tot $f_t$ leidt, wordt behandeld als een bewijs van $f_t$. Deze prefixes worden toegevoegd aan een trainingsset $D_{train}$ om het beleid bij te werken via cross-entropy loss.
• Doelbuffer ($G$): Een buffer houdt ontdekte stellingen bij. De agent sampleert doelen uniform uit $G$ voor daaropvolgende zoekepisodes, wat effectief zijn eigen curriculum bootstrapt.

B. Extractie van nuttige stellingen

Om te voorkomen dat de bibliotheek overvol raakt met triviale of redundante stellingen, filtert het algoritme ontdekte stellingen op basis van twee criteria:

1. Generaliteit: Stellingen worden gefilterd om diegene te verwijderen die louter specialisaties zijn van andere kandidaten. Het systeem behoudt alleen de "minimale" elementen onder een partiële orde gedefinieerd door formule-substitutie (d.w.z. het behouden van de meest algemene vormen).
2. Herbewijsbaarheid: Het systeem schat de waarschijnlijkheid in dat de huidige policy een stelling opnieuw kan bewijzen. Met behulp van een Bayesiaanse posterieure gemiddelde (Beta(1,1) prior), geeft het prioriteit aan stellingen die weliswaar ontdekt zijn, maar moeilijk te herbewijzen zijn. Deze "moeilijk te herbewijzen" stellingen zijn waardevol omdat het toevoegen van hen als lemma's de moeilijke bewijsroutes comprimeert.

C. Multi-generatie bibliotheekexpansie

Het proces werkt in generaties:

1. Beleidsleren: Train de policy op de huidige actieruimte (aanvankelijk alleen axioma's en MP).
2. Extractie: Identificeer nuttige stellingen uit de doelbuffer $G$ op basis van generaliteit en herbewijsbaarheid.
3. Expansie van de actieruimte: Voeg de geëxtraheerde stellingen toe als nieuwe bibliotheekacties (bijv. $Thm_1, Thm_2$). Wanneer deze worden geselecteerd, worden de corresponderende stelling op de stack gepusht, wat fungeert als een vooraf geverifieerd lemma.
4. Iteratie: Herhaal het proces, waardoor de agent de eerder ontdekte stellingen kan gebruiken om nieuwe, complexere stellingen te vinden.

Belangrijkste Bijdragen

1. Formulering: Bewijsvoering in propositielogica wordt geformuleerd als een stackmachine-beslissingsproces direct gebaseerd op Hilbert-axioma's en inferentieregels, zonder afhankelijkheid van externe bewijs corpora.
2. Algoritme: Er wordt een zelfgestuurd algoritme voor de ontdekking van stellingen voorgesteld dat een bibliotheek van stellingen laat groeien vanuit primitieve regels alleen. Het hergebruikt geëxtraheerde stellingen als lemma's voor daaropvolgende bewijszoektochten.
3. Autonome Ontdekking: De agent ontdekt tienduizenden stellingen en vindt bewijzen voor door mensen geschreven benchmarkproblemen zonder menselijke priors te gebruiken voor training.
4. Transfereerbaarheid: De geëxtraheerde stellingen dienen als effectieve externe kennis, wat de prestaties van externe LLM's bij bewijsvoering verbetert wanneer zij als prompt-lemma's worden verstrekt.

Experimentele Resultaten

1. Ontdekking en Dekking van Stellingen

• Groei: Het aantal ontdekte stellingen neemt toe over zes generaties, wat de bekwaamheid van de agent aantoont om zijn kennisbasis autonoom uit te breiden.
• Benchmark Prestaties: De agent vindt succesvol Hilbert-systeem bewijzen voor 30% van een door mensen geschreven benchmarkset (afgeleid van Kleene's tekstboek).
• Vergelijking: Terwijl GPT-5-high (de sterkste baseline) slechts ~23% nauwkeurigheid bereikt op deze benchmarks zonder assistentie, suggereert het vermogen van de agent om bewijzen te vinden voor 30%, dat de agent niet-triviale bewijzen ontdekt die vanuit een menselijk wiskundig perspectief betekenisvol zijn.

2. Impact op LLM Redeneren

• Prompt Lemma's: Wanneer de geëxtraheerde stellingen als prompt-lemma's aan GPT-4o en GPT-5 varianten worden verstrekt, verbeteren hun succespercentages op de benchmarkproblemen aanzienlijk.
• Kwalitatieve Analyse:
  • Sommige ontdekte stellingen komen overeen met bekende principes (bijv. het principe van explosie, $\neg A \to (A \to B)$), die gemakkelijk interpreteerbaar zijn.
  • Andere (bijv. complexe implicatie-lifting) zijn niet direct voor de mens voor de hand liggend, maar functioneren effectief als ondersteunende kennis in LLM-bewijzen.
  • Dit geeft aan dat de agent nuttige lemma's kan naar voren brengen die mensen niet expliciet hebben verstrekt, en dat deze lemma's transfereerbaar zijn naar andere redeneerarchitecturen (van de agent naar LLM's).

Betekenis en Claims

Het artikel beweert bewijs te leveren dat nuttige stellingen kunnen ontstaan uit bewijszoektocht zonder afhankelijk te zijn van door mensen verstrekte stellingbibliotheken.

• Zelf-evoluerende AI: Het werk suggereert een pad naar zelf-evoluerende AI-systemen voor wiskunde die autonoom hun formele kennis kunnen uitbreiden via bewijszoektocht, terwijl ze garanderen dat elke ontdekking formeel verifieerbaar blijft.
• Formele Verifieerbaarheid: In tegen tegenover LLM's die plausibele maar onjuiste stellingen kunnen hallucineren, zijn de ontdekkingen van de agent strikt gegrond in de axioma's en inferentieregels van het Hilbert-systeem.
• Bescheidenheid: De auteurs beweren niet dat zij de state-of-the-art LLM's in algemeen redeneren hebben overtroffen. In plaats daarvan demonstreren zij dat in een beperkte, formele setting, een agent kan leren om zijn eigen kennis te ontdekken en te benutten om problemen op te lossen die zelfs voor geavanceerde LLM's moeilijk zijn, en dat deze zelf ontdekte kennis externe systemen kan versterken.

De studie is beperkt tot één enkel axioma-systeem (Hilbert propositielogica), maar de auteurs stellen dat het framework generaliseerbaar is naar rijkere systemen zoals eerste-orde logica of verzamelingenleer, wat een richting blijft voor toekomstig werk.