Technische Samenvatting: Geometrische Metingen van de Keuze-axioma in Neurale Bewijs-embeddings

Probleemstelling

De keuze-axioma (axiom of choice, AC) heeft historisch gezien de wiskundige fundamenten verdeeld in klassieke en constructieve kampen, een onderscheid dat grotendeels filosofisch en methodologisch blijft. Terwijl klassieke bewijzen gebruikmaken van niet-constructieve afkortingen die door AC worden toegestaan, en constructieve bewijzen expliciete getuigen (witnesses) vereisen, is het onduidelijk of deze twee paradigma's structureel verschillen op manieren die detecteerbaar zijn buiten eenvoudige axioma-afhankelijkheid. Dit artikel onderzoekt of de keuze-axioma een meetbare "geometrische signatuur" achterlaat binnen de ruimte van formele bewijzen, specifiek binnen de Lean 4 Mathlib-bibliotheek, en of deze signatuur operationele consequenties heeft voor neurale stellingbewijzers.

Methodologie

Datapartitiering en Afhankelijkheidsregistratie

De auteurs maken gebruik van de kernel-niveau tracking van axioma-afhankelijkheid in Lean 4 om de Mathlib-bibliotheek te partitioneren, die 471.260 machine-gecertificeerde verklaringen bevat. Door een breedte-eerst zoekopdracht (breadth-first search) uit te voeren op de afhankelijkheidsgraaf, classificeren zij de verklaringen in twee sets:

1. Klassieke Bewijzen: Die transitief afhankelijk zijn van Classical.choice.
2. Constructieve Bewijzen: Die dat niet zijn.

De "afstand" van een klassiek bewijs wordt gedefinieerd als de lengte van de kortste afhankelijkheidsketen van dat bewijs naar Classical.choice. Dit creëert een gestratificeerde dataset waarbij bewijzen worden gegroepeerd op basis van hun diepte vanaf het axioma. De studie richt zich op een gefilterde populatie van 42.355 stellingen (31.144 klassiek, 11.211 constructief) met tactische sporen (tactic traces) tussen 2 en 200 stappen.

Label-vrije Representatieleer

Om de geometrische eigenschappen van deze bewijzen te meten zonder bias, trainen de auteurs een zelf-gesuperviseerde denoising autoencoder uitsluitend op constructieve bewijzen.

• Input: Bewijzen worden gerepresenteerd als sequenties van tactische koppen (bijv. intro, rw, simp), waarbij specifieke argumenten worden weggelaten om de focus op bewijscompositie te leggen.
• Architectuur: Een 4-laagse Transformer-encoder gekoppeld aan een 2-laagse decoder. Het model is getraind om gemaskeerde tactische tokens (20% corruptie) te reconstrueren vanuit de inputsequentie.
• Embedding: De bewijs-embedding is het gemiddelde van de verborgen toestanden (hidden states) van de encoder (exclusief padding), genormaliseerd tot de eenheidsbol.
• Label-vrije Beperking: De encoder ziet tijdens de training nooit klassieke bewijzen, noch bij de constructie van de vocabulaire of de hyperparameterselectie. Klassieke bewijzen dienen strikt als een apart gehouden populatie voor meting.

Geometrische Metingen

Drie complementaire metrieken worden gebruikt om de divergentie van klassieke bewijzen van de constructieve trainingsdistributie te meten als functie van hun afhankelijkheidsdiepte:

1. Anomalie-score (k-NN): De Euclidische afstand tot de $k$-dichtstbijzijnde constructieve buren.
2. Reconstructieverlies: Het cross-entropy verlies dat optreedt wanneer het op constructieve bewijzen getrainde model probeert gemaskeerde tokens in een klassiek bewijs te voorspellen.
3. Dichtheids-superlevel Insluiting: Het fractie van klassieke bewijzen die buiten de hoog-densiteitsregio (superlevel set) vallen die door de constructieve trainingsdistributie wordt gedefinieerd.

Operationele Evaluatie

De studie evalueert de impact van deze geometrische bevindingen op de prestaties van stellingbewijzers met behulp van twee systemen:

1. aesop: Een symbolische best-first search bewijzer.
2. Hybride (ReProver + aesop): Een neuraal-gestuurde aanpak waarbij een neurale tactiek-generator de eerste zet voorstelt, gevolgd door aesop.

Belangrijkste Resultaten

De Dieptewet (The Depth Law)

De primaire bevinding is het bestaan van een "dieptewet": het geometrische onderscheid tussen klassieke en constructieve bewijzen neemt voorspelbaar af met de afstand van Classical.choice.

• Scherpe Separatie bij Ondiepheden: Bij diepte 2 (bewijzen die direct klassieke lemma's aanroepen), is de separatie sterk. De k-NN anomalie-score bereikt een AUC van 0,847, het reconstructieverlies is 34,5% hoger dan de constructieve baseline, en 43% van de klassieke bewijzen valt buiten de constructieve 90% dichtheidsregio.
• Verval naar Ononderscheidbaarheid: Naarmate de diepte toeneemt, convergeren de metrieken naar de constructieve baseline. Bij diepte 9+ benaderen alle drie de metrieken het niveau van toeval (AUC $\approx$ 0,5, verlies $\approx$ baseline, containment $\approx$ 90%), waardoor diepe klassieke bewijzen geometrisch ononderscheidbaar zijn van constructieve bewijzen.
• Eén-parameter Mengwet: De auteurs modelleren dit gradiënt als een mengeling van twee distributies: een constructieve distributie $P$ en een direct-klassieke distributie $R$. De diepte-$d$ distributie $Q_d$ wordt gemodelleerd als $Q_d = (1 - \lambda_d)P + \lambda_d R$, waarbij $\lambda_d$ een menggewicht is dat afneemt met de diepte. De drie verschillende metingen vallen samen op één curve wanneer ze genormaliseerd worden, wat de een-parameter wet ondersteunt.

Robuustheidscontroles

Het signaal is robuust tegen verschillende mogelijke verstorende factoren (confounds):

• Keywords: Het verwijderen van expliciete klassieke tactische markers (bijv. classical, by contra) vermindert de diepte-2 AUC slechts licht (van 0,847 naar 0,754), wat aangeeft dat het signaal structureel is en niet louter lexicaal.
• Lengte: Het residualiseren van embeddings voor bewijslengte elimineert het gradiënt niet.
• Auteur/Bestand/Onderwerp: Mixed-effects modellen die controleren voor auteur, bestand en wiskundig subdomein bevestigen dat het signaal standhoudt binnen specifieke contexten.
• Stelling vs. Bewijs: Stelling-verklaringen (statements) vertonen een veel zwakker dieptegradiënt (geaggregeerde AUC 0,604) vergeleken met bewijzen (geaggregeerde AUC 0,675), wat bevestigt dat het signaal primair compositioneel is (bewijsstructuur) en niet topisch (inhoud van de stelling).
• Axioma-specificiteit: Hoewel propext en Quot.sound ook dieptegradiënten vertonen, produceert Classical.choice het steilste gradiënt, wat suggereert dat het een unieke operationele koppeling heeft met klassieke redenering.

Operationele Consequenties

De geometrische signatuur correleert met de prestaties van de bewijzer:

• aesop Falen: aesop lost 20,0% van de constructieve stellingen op maar slechts 1,5% van de klassieke (een factor 13 verschil). In tegenstelling tot het geometrische signaal, vlakt deze operationele kloof niet af met de diepte; klassieke bewijzen blijven moeilijk voor aesop, ongeacht hun afstand tot het axioma.
• Neurale Sturing: Het toevoegen van een neurale tactiek-generator (ReProver) verkleint de kloof tot ongeveer factor 5 (22,0% vs. 4,5%), maar sluit deze niet.
• Voorspellende Kracht: De geometrische anomalie-score voorspelt het falen van aesop aanzienlijk beter dan bewijslengte alleen (de AUC stijgt van 0,766 naar 0,841 wanneer de anomalie-score wordt toegevoegd).

Betekenis en Claims

Het artikel claimt het eerste empirische bewijs te leveren dat de keuze-axioma een meetbare geometrische correlatie heeft in de bewijsruimte. De auteurs stellen dat:

1. Structureel Onderscheid: Het klassieke/constructieve onderscheid is niet alleen een filosofische houding, maar een structurele eigenschap van bewijscompositie die zichtbaar is in neurale embeddings.
2. Operationele Relevantie: Deze geometrische signatuur is niet louter een abstract curiosum; het voorspelt de prestaties van automatische stellingbewijzers. De "dieptewet" suggereert dat naarmate bewijzen verder van het axioma af komen te staan, ze structureel meer lijken op constructieve bewijzen, terwijl de operationele barrière voor symbolische bewijzers zoals aesop specifiek blijft voor de aanwezigheid van Classical.choice.
3. Methodologische Bijdrage: Het werk demonstreert dat label-vrije, zelf-gesuperviseerde leer op een enkele klasse (constructieve bewijzen) de structurele grenzen van een apart gehouden klasse (klassieke bewijzen) kan onthullen die gedefinieerd zijn door logische afhankelijkheid, wat een nieuw instrument biedt voor meta-mathematische analyse.

De auteurs blijven bescheiden over causale mechanismen, waarbij zij opmerken dat hoewel de geometrische signatuur en de operationele kloof sterk geassocieerd zijn, de specifieke oorzaak van de moeilijkheid voor de bewijzer (structurele barrière vs. configuratie van de regelset) verder onderzoek vereist. Het werk wordt gepresenteerd als een uitnodiging aan de gemeenschap om soortgelijke structurele assen in formele bibliotheken te identificeren.