💬 NLP

AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory

Dit artikel presenteert de eerste uitgebreide Lean 4-formalisering van statistische leertheorie gebaseerd op empirische processen, ontwikkeld via een mens-AI-collaboratieve workflow om een herbruikbare formele basis te vestigen die impliciete aannames in standaard tekstboeken oplost en toekomstige ontwikkelingen in de machine learning-theorie mogelijk maakt.

Oorspronkelijke auteurs: Yuanhe Zhang, Jason D. Lee, Fanghui Liu

Gepubliceerd 2026-06-11

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Yuanhe Zhang, Jason D. Lee, Fanghui Liu

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een computer probeert te leren van data, zoals een student die studeert voor een wiskundetoets. Statistical Learning Theory (SLT) is het regelboek dat ons vertelt waarom deze student waarschijnlijk de toets zal halen en hoe goed hij zal presteren. Het is de "natuurkunde" achter machine learning.

Echter, dit regelboek is geschreven in een zeer complexe, hoogwaardige taal (geavanceerde wiskunde). Decennialang hebben mensen dit gelezen, het grote plaatje begrepen en zijn verder gegaan. Maar omdat de bewijzen zo lang zijn en steunen op subtiele, verborgen aannames, is het gemakkelijk om een klein logisch gat te missen. Het is alsof je een recept leest waarin staat "meng tot het glad is" zonder te definiëren wat "glad" eigenlijk betekent. Als je dan probeert een robotkok te bouwen op basis van dat vage recept, kan het misgaan.

Dit artikel, AI4SLT, gaat over het bouwen van een perfecte, onbreekbare digitale versie van dat regelboek met behulp van een tool genaamd Lean 4. Denk aan Lean 4 als een superstrikte corrector die weigert één enkel vaag woord te accepteren. Als een stap in de logica niet expliciet is gedefinieerd, stopt Lean 4 en zegt: "Dat kan ik niet doen."

Hier is wat de auteurs hebben gedaan, uitgelegd via eenvoudige analogieën:

1. Het Mens-AI Team: De Architect en de Metselaar

De auteurs vroegen niet simpelweg een AI om "de code te schrijven". Ze gebruikten een collaboratieve workflow:

De Mensen (Architecten): Zij bekeken de complexe wiskundige tekstboeken en ontwierpen de strategie. Ze zeiden: "We moeten eerst dit specifieke deel bewijzen, en dit is het plan."
De AI (De Metselaar): De AI (specifiek Claude Code) nam dat plan en deed het zware werk van het schrijven van de eigenlijke code, waarbij de kleine, tijdrovende logische stappen werden ingevuld.
Het Resultaat: Ze bouwden een enorme bibliotheek van ongeveer 30.000 regels code. Dit is als het bouwen van een wolkenkrabber vanaf de grond af aan, steen voor steen, waarbij elke enkele steen is geïnspecteerd door een robot om te garanderen dat deze perfect past.

2. Het Fundament Bouwen: De "Gaussian Toolbox"

Om te bewijzen dat machine learning werkt, moet je begrijpen hoe willekeurige ruis zich gedraagt. Het artikel bouwde een complete gereedschapskist voor dit doel, wat nog nooit op een computer-verifieerbare manier was gedaan.

De Analogie: Stel je voor dat je het weer probeert te voorspellen. Je moet begrijpen hoe wind, regen en temperatuur met elkaar interageren. De auteurs bouwden de "wind", "regen" en "temperatuur" sensoren vanaf nul binnen de computer.
Wat ze bouwden: Ze formaliseerden complexe wiskundige instrumenten zoals Gaussian Lipschitz concentration en Dudley's entropy integral.
- Eenvoudige vertaling: Deze instrumenten helpen ons te berekenen wat het "worst-case scenario" is voor hoeveel een leeralgoritme kan falen door willekeurig geluk. Het artikel bewees dat het algoritme, zelfs in het slechtste geval, binnen een voorspelbare, veilige grens blijft.

3. De "Chaining" Truc: Een Berg Beklimmen

Een van de moeilijkste delen van de wiskunde wordt Dudley's Entropy Integral genoemd.

De Analogie: Stel je voor dat je een zeer hoge, mistige berg moet beklimmen (het "empirische proces"). Je kunt de top niet zien.
De Oude Manier: Tekstboeken zeggen vaak: "Ga er maar vanuit dat je de top kunt zien."
De Manier van dit Artikel: Ze bouwden een ladder van platforms (genoemd "chaining"). Je springt niet direct naar de top; je springt van een klein platform naar een iets hoger platform, en dan naar een volgend platform, helemaal naar boven toe.
De Prestatie: De auteurs formaliseerden dit volledige laddersysteem in Lean 4. Ze bewezen dat als je deze kleine, veilige sprongen maakt, je wiskundig kunt garanderen dat je niet van de berg af valt. Dit stelt hen in staat om precies te voorspellen hoeveel data je nodig hebt om een specifieke taak te leren.

4. De Motor Testen: De Least Squares Test

Zodra de gereedschapskist gebouwd was, testten ze deze op een reëel probleem: Least Squares Regression (een veelvoorkomende manier om een lijn door een reeks punten te trekken).

Het Resultaat: Ze gebruikten hun nieuwe, superstrikte digitale regelboek om te bewijzen dat deze methode werkt, en ze berekenden de exacte snelheid waarmee het leert.
Waarom het ertoe doet: Ze zeiden niet alleen "het werkt". Ze bewezen hoe snel het werkt, tot in het kleinste detail, en toonden aan dat hun methode de best mogelijke snelheid (minimax rate) bereikt voor dit soort problemen.

5. Het Verborgen Voordeel: Het Ontdekken van de "Ghost" Aannames

Het meest verrassende deel van het artikel is wat er gebeurde tijdens het proces.

De Analogie: Wanneer je een huis probeert te bouwen met een robot die perfecte instructies eist, besef je dat je oorspronkelijke blauwdrukken zaken missen zoals "de deur heeft een scharnier nodig" of "de vloer moet waterpas zijn".
De Ontdekking: De auteurs ontdekten dat standaard wiskundige tekstboeken vaak kleine, cruciale details weglaten (zoals of een functie "meetbaar" of "continu" is). De AI kon niet verder gaan totdat deze waren gecorrigeerd.
De Uitkomst: Door de computer te dwingen elke regel te controleren, hebben ze de theorie opgeschoond, waardoor deze rigoureuzer werd en verborgen aannames blootlegden waar mensen jarenlang overheen hadden gekeken.

Samenvatting

Dit artikel is de eerste keer dat iemand de complexe, abstracte "regelboek" van de machine learning theorie heeft genomen en deze volledig heeft herbouwd binnen een computersysteem dat elke enkele logische stap controleert. Ze gebruikten een team van mensen om het plan te ontwerpen en AI om de structuur te bouwen. Het resultaat is een geverifieerde, foutloze fundering die bewijst dat machine learning algoritmen werken, uitlegt exact hoe snel ze leren, en de gaten in de oorspronkelijke wiskundige theorieën dicht.

Technische Samenvatting: AI4SLT: Empirische Processen in Lean 4 voor Formele Statistische Leertheorie

Probleemstelling

De Statistische Leertheorie (SLT) stuurt de vooruitgang van machine learning al decennia lang succesvol aan door fundamentele concepten zoals de bias-variantie afruil en regularisatie te bieden. Echter, naarmate modellen evolueren naar complexe architecturen (bijv. diepe neurale netwerken, grote taalmodellen), zijn hedendaagse theoretische analyses steeds complexer geworden, waarbij ze vertrouwen op geavanceerde wiskundige instrumenten uit de functionele analyse en statistische fysica. Deze complexiteit zet de menselijke verificatie onder druk, waardoor het moeilijk wordt om logische afhankelijkheden te volgen en tussenliggende lemma's op schaal te verifiëren.

Bovendien missen kerntechnieken in SLT, zoals concentratie-ongelijkheden en covering-argumenten, een gestructureerde, machine-leesbare bibliotheek, wat de herbruikbaarheid beperkt. Hoewel interactieve stellingbewijzers zoals Lean 4 een pad bieden naar machine-controleerbare correctheid, zijn bestaande formalisaties in machine learning beperkt tot specifieke gebieden (bijv. reinforcement learning, optimalisatie) of vereenvoudigde instellingen (bijv. generalisatiebounds via Rademacher-complexiteit over volledige functieklassen). Een uitgebreide formalisering van het gelokaliseerde empirische procesframework—dat essentieel is voor het afleiden van scherpe minimax-snelheden in hoogdimensionele en niet-parametrische settings—ontbreekt nog. Dit framework vereft een rigoureuze behandeling van meetbaarheid, integreerbaarheid en topologische aannames die in standaard tekstboeken vaak impliciet worden gelaten.

Methodologie

De auteurs presenteren AI4SLT, de eerste uitgebreide formalisering van SLT gebaseerd op empirische procesleer binnen Lean 4. Het project werd uitgevoerd met behulp van een mens-AI collaboratieve workflow:

Rol van de Mens: Wiskundigen ontwierpen bewijsstrategieën, analyseerden de bestaande Mathlib-infrastructuur, deconstrueerden complexe stellingen in beheersbare lemma's en verifieerden de consistentie van beweringen.
Rol van de AI: AI-agenten (specifiek Claude Code met Opus-4.5) voerden tactische bewijskonstructie uit, waarbij zij details invulden op basis van gestructureerde specificaties.

De workflow maakte gebruik van een gestructureerd specificatieprotocol (TASK.md) bevattende doelstellingen, infrastructuur-pointers, formaliseringsgerichte bewijsplannen en harde grenzen. Het proces legde de nadruk op iteratieve verfijning, waarbij AI-fouten werden gebruikt om impliciete aannames geïdentificeerd te hebben die door mensen waren weggelaten, wat leidde tot convergente in plaats van open eindeloze samenwerking. Het gehele project besloeg ongeveer 500 uur van gesuperviseerde ontwikkeling, resulterend in ~30.000 regels Lean 4-code gecompileerd zonder sorry (onbewezen doelen) of aangepaste axioma's.

Kernbijdragen

1. Gaussian Lipschitz Concentratie Toolbox

De auteurs hebben een volledige formele ontwikkeling geconstrueerd van de Gaussian Lipschitz concentratie, een fundamenteel instrument in de hoogdimensionele waarschijnlijkheidsleer. Dit vereiste het vanaf nul opbouwen van een substantiële infrastructuur, inclusief:

Efron-Stein Ongelijkheid: Formaliseerd met een universele transfer-lemma om coördinaat-gewijze updates met verschillende distributies af te handelen.
Gaussian Poincaré Ongelijkheid: Afgeleid met behulp van de Efron-Stein infrastructuur en Taylor-expansie-bounds.
Dichtheidsargumenten: Formalisering van de extensie van ongelijkheden van gladde, compact ondersteunde functies ( $C^\infty_c$ ) naar algemene Lipschitz en $C^1$ klassen via Gaussian Sobolev ruimtes ( $W^{1,2}$ ) en mollificatie-technieken.
Gaussian Logaritmische Sobolev Ongelijkheid (LSI): Formalisering van de tensorisatie van de 1D LSI naar de $n$ -dimensionale casus met behulp van entropie subadditiviteit.
Gaussian Lipschitz Concentratie: Afgeleide van de uiteindelijke concentratiebound met behulp van het Herbst-argument en de Chernoff-bound.

Naar weten van de auteurs vormt dit de eerste formalisering van de volledige Gaussian analyse-instrumenten in enige theorem prover.

2. Dudley's Entropie-integraal voor Sub-Gaussian Processen

Het artikel biedt de eerste formalisering van de Dudley's entropie-integraal stelling voor sub-Gaussian processen in Lean 4. Dit resultaat begrenst de verwachte supremum van een stochastisch proces door een integraal die betrokken is bij metrische entropie.

Formaliseringsuitdagingen: De auteurs adresseerden de noodzaak voor rigoureuze chaining-argumenten, waarbij het proces wordt gedecomposeerd in een telescopische som over dyadische benaderingen. Zij formaliseerden covering en packing getallen in metrieke ruimtes en hanteerden de integratie van uitgebreide niet-negatieve reële getallen ( $\mathbb{R}_{\ge 0}^\infty$ ) versus reële functies, om er zeker van te zijn dat de bound toepasbaar is op algemene sub-Gaussian processen.

3. Toepassing: Least-Squares Framework via Gelokaliseerde Empirische Processen

De auteurs toonden het praktische nut van hun infrastructuur aan door een verenigd framework voor least-squares regressie te ontwikkelen op basis van het gelokaliseerde empirische proces.

Master Error Bound: Zij formaliseerden de cruciale ongelijkheid die de voorspellingsfout koppelt aan de kritische radius $\delta^*$ , afgeleid van de gelokaliseerde Gaussian complexiteit.
Scherpe Rates: Het framework werd toegepast op lineaire regressie en $\ell_1$ -geconstrangeerde regressie (Lasso). Door covering getallen te begrenzen (met behulp van Euclidische reductie en Maurey's empirische methode voor $\ell_1$ -convexe hulls), verkregen de auteurs scherpe rates tot op het minimax niveau, waarbij resultaten zoals $O(\sigma^2 r/n)$ voor lineaire regressie en $O(R\sqrt{\log d/n})$ voor hoogdimensionele sparse regressie werden gereproduceerd.

4. Mens-AI Collaboratieve Formaliseringsparadigma

Het artikel beschrijft een methodologie voor grootschalige formalisering:

Gestructureerde Specificaties: Het reduceren van de eerste poging faalratio's van ~70% naar ~15% door expliciete infrastructuur-pointers en tactische bewijsplannen te verstrekken.
Iteratieve Evolutie: Het gebruik van AI-fouten om impliciete menselijke aannames (bijv. meetbaarheid, integreerbaarheid, domeinrestricties) aan het licht te brengen en specificaties iteratief te verfijnen.
Kwantitatieve Uitsplitsing: Ongeveer 40% van de declaraties werd bewezen onder volledige natuurlijke taal bewijsplannen, 30% was sketch-gestuurd, 15% was autonoom, en 15% vereiste kritische menselijke interventie (bijv. het corrigeren van gebrekkige wiskundige strategieën of het verifiëren van de consistentie van stellingen).

Resultaten

Codebase: Een bibliotheek van ~30.000 regels Lean 4-code met meer dan 1.000 stellingen en lemma's.
Volledigheid: Alle formalisaties compileren zonder sorry of axioma's, wat machine-verifieerbare correctheid garandeert.
Gap Resolutie: De formalisering legde impliciete aannames in standaard SLT tekstboeken bloot en loste deze op, zoals meetbaarheidscondities voor supremum random variabelen, integreerbaarheid van entropie functionalen, en de niet-leegheid van empirische sferen.
Prestaties: Het framework heeft succesvol scherpe minimax rates afgeleid voor zowel parametrische (lineaire) als niet-parametrische (sparse) regressie settings, wat het nut van de gelokaliseerde empirische procesbenadering valideert.

Betekenis

De auteurs claimen dat dit werk een herbruikbare formele fundering voor de statistische leertheorie vestigt. Door verder te gaan dan mechanische vertaling naar een granulaire, regel-voor-regel begrip van de theorie, dwingt dit project een rigoureuze standaard af die logische afhankelijkheden en verborgen aannames verheldert.

De betekenis is tweeledig:

Theoretische Rigor: Het biedt een machine-gecontroleerde bibliotheek voor SLT, wat schaalbare, geautomatiseerde theoretische analyse van machine learning systemen mogelijk maakt en dient als een principiële trainingsgrond voor studenten om de volledige technische stack van SLT onder de knie te krijgen.
Methodologische Vooruitgang: Het demonstreert dat grootschalige formaliseringsprojecten aanzienlijk versneld kunnen worden door goed ontworpen mens-AI samenwerking, wat een blauwdruk biedt voor toekomstige ontwikkelingen in de machine learning theorie en andere complexe wiskundige domeinen.

De auteurs benadrukken dat dit werk niet louter een oefening in rigor is, maar een noodzakelijke stap om de toenemende complexiteit van moderne machine learning theorie te hanteren, wat de deur opent voor toekomstige formele ontwikkelingen in het veld.