💬 NLP

Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

Dieser Artikel präsentiert eine Formalisierung in Lean 4 von Generalisierungsfehlergrenzen, die auf Rademacher-Komplexität und Dudley-Entropieintegral basieren, und zwar mit einem mechanisch verifizierten Ablauf von maßtheoretischen Grundlagen bis zu hochwahrscheinlichen gleichmäßigen Abweichungsgrenzen und deren Anwendung auf lineare Prädiktoren.

Ursprüngliche Autoren: Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda

Veröffentlicht 2026-05-26

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie sind ein Koch, der gerade ein neues Rezept erfunden hat. Sie haben es 100 Mal in Ihrer Küche (den Trainingsdaten) zubereitet, und es schmeckte jedes Mal perfekt. Aber Sie möchten wissen: Wenn Sie dieses gleiche Rezept für eine Million Fremde in einem Restaurant (den Testdaten) kochen, wird es dann immer noch gut schmecken?

In der Welt des maschinellen Lernens nennt man dies das Generalisierungsproblem. Das Papier, nach dem Sie fragen, ist ein strenger, computerverifizierter Beweis, der uns hilft, diese Frage mit mathematischer Gewissheit zu beantworten.

Hier ist die Geschichte des Papiers, aufgeschlüsselt in einfache Konzepte und Analogien.

1. Das Problem: Die Kluft zwischen „Küche und Restaurant"

Wenn ein Computer lernt, versucht er, eine Regel (eine Hypothese) zu finden, die zu den Daten passt, die er sieht.

Trainingsfehler: Wie gut die Regel zu den Daten passt, die sie bereits gesehen hat (Ihre 100 Küchenversuche).
Testfehler: Wie gut die Regel auf neue Daten funktioniert, die sie noch nicht gesehen hat (die Restaurantgäste).

Die Gefahr ist das Overfitting. Das ist wie ein Koch, der den exakten Geschmack seiner 100 Versuche auswendig gelernt hat, aber die Prinzipien des Kochens nicht versteht. Wenn er im Restaurant auf eine leicht andere Zutat trifft, misslingt das Gericht. Wir brauchen eine Möglichkeit, zu garantieren, dass der „Kuchenerfolg" in einen „Restauranterfolg" übersetzt wird.

2. Das Werkzeug: Rademacher-Komplexität (der „Münzwurf-Test")

Um zu messen, wie wahrscheinlich es ist, dass ein Rezept overfittet, verwenden Mathematiker ein Werkzeug namens Rademacher-Komplexität.

Stellen Sie sich einen Beutel mit Münzen vor. Sie werfen sie, und sie landen völlig zufällig auf Kopf (+1) oder Zahl (-1).

Der Test: Sie fragen Ihr Rezept (den Lernalgorithmus): „Können Sie diese zufälligen Münzwürfe vorhersagen?"
Die Logik: Wenn Ihr Rezept eine einfache, robuste Regel ist, sollte es nicht in der Lage sein, zufälliges Rauschen vorherzusagen. Es sollte rein zufällig etwa 50 % richtig liegen.
Die rote Flagge: Wenn Ihr Rezept zu komplex ist (wie ein Koch, der jedes einzelne Detail auswendig gelernt hat), könnte es versehentlich ein „Muster" in den zufälligen Münzwürfen finden und sie besser als zufällig vorhersagen.

Die Rademacher-Komplexität misst genau, wie gut ein Modell durch das Anpassen an zufälliges Rauschen „schummeln" kann. Je niedriger diese Zahl ist, desto wahrscheinlicher wird das Modell auf neue Daten gut generalisieren.

3. Die Leistung: Der „digitale Doppelcheck"

Die Autoren dieses Papiers haben diese mathematischen Beweise nicht nur auf Papier geschrieben; sie haben sie in einem Computerprogramm namens Lean 4 implementiert.

Stellen Sie sich Lean 4 als einen überstrengen, unblinzelnden Redakteur vor.

Der alte Weg: Ein Mathematiker schreibt einen Beweis auf Papier. Ein menschlicher Prüfer liest ihn. Wenn der Mensch eine winzige logische Lücke übersieht, könnte der Beweis akzeptiert werden, selbst wenn er leicht falsch ist.
Der neue Weg (dieses Papier): Die Autoren fütterten ihren gesamten Beweis in Lean ein. Der Computer überprüfte jeden einzelnen Schritt, jede Definition und jede Annahme. Wenn es auch nur eine winzige fehlende Verbindung gab (wie „Ist diese Funktion messbar?"), hätte der Computer ihn abgelehnt.

Das Papier behauptet, eine mechanisch verifizierte Pipeline aufgebaut zu haben. Sie beginnt mit den grundlegenden Definitionen, durchläuft einen „Symmetrisierungs"-Trick (ein cleveres mathematisches Umsortieren) und endet mit einer Garantie hoher Sicherheit, dass der Testfehler nicht viel schlechter sein wird als der Trainingsfehler.

4. Die große Hürde: Das Problem der „unendlichen Bibliothek"

In der realen Welt haben maschinelle Lernmodelle oft unendliche Möglichkeiten (wie einen kontinuierlichen Bereich von Zahlen für Gewichte).

Das Problem: In der Mathematik ist es einfach, eine endliche Liste von Elementen zu überprüfen (wie 100 Rezepte). Es ist viel schwieriger, eine unendliche Liste zu überprüfen. In computertechnischen Begriffen kann das Überprüfen des „Maximums" einer unendlichen Liste manchmal die Regeln der Logik brechen (Messbarkeitsprobleme).
Die Lösung des Papiers: Die Autoren schufen eine clevere „Brücke". Sie bewiesen die Mathematik zuerst für eine abzählbare (endliche oder auflistbare) Menge von Hypothesen. Dann zeigten sie, dass für viele reale Modelle (die „separierbare" topologische Räume sind) die unendliche Menge durch eine abzählbare dichte Teilmenge angenähert werden kann (wie die Verwendung eines sehr feinen Gitters zur Annäherung an eine glatte Kurve).
Die Analogie: Stellen Sie sich vor, Sie versuchen, die Größe jedes möglichen Menschen auf der Welt zu messen. Es ist unmöglich, jeden zu messen. Aber wenn Sie jeden Menschen messen, der genau 1 cm in der Größe voneinander entfernt ist, können Sie mathematisch beweisen, dass Ihre Messung alle anderen mit hoher Präzision abdeckt. Das Papier formalisierte diesen „Gitter"-Trick, damit der Computer ihn akzeptiert.

5. Die Ergebnisse: Was haben sie bewiesen?

Sobald der „Motor" gebaut war, fuhren sie ihn durch drei spezifische Szenarien, um zu zeigen, dass er funktioniert:

Lineare Prädiktoren mit $\ell_2$ -Regularisierung: Dies ist wie ein Modell, das gezwungen wird, seine „Zutaten" (Gewichte) klein und ausgewogen zu halten. Das Papier bewies die Standardmathematikgrenze dafür.
Lineare Prädiktoren mit $\ell_1$ -Regularisierung: Dies zwingt das Modell, „spärlich" zu sein (nur wenige Zutaten zu verwenden). Sie bewiesen die Grenze dafür, was eine leicht andere Berechnung beinhaltet (die die Quadratwurzel der Anzahl der Merkmale einbezieht).
Dudleys Entropie-Integral: Dies ist ein fortgeschritteneres, allgemeines Werkzeug. Stellen Sie sich vor, Sie haben eine sehr unordentliche, komplexe Form. Anstatt das Ganze zu messen, bedecken Sie es mit kleineren, einfacheren Formen (wie einen buckligen Felsen mit glatten Kieselsteinen bedecken). Das Papier formalisierte, wie man die Komplexität basierend auf der Anzahl der „Kieselsteine" berechnet, die benötigt werden, um die Form zu bedecken.

Zusammenfassung

Dieses Papier ist ein fundamentales Ingenieurskunstwerk.

Was sie taten: Sie nahmen komplexe, lehrbuchartige Theorien darüber, wie maschinelle Lernmodelle generalisieren (Rademacher-Komplexität), und übersetzten sie in eine Sprache, die ein Computer mit 100-prozentiger Sicherheit verifizieren kann.
Warum es wichtig ist: Es entfernt den „menschlichen Fehler" aus den kritischsten Sicherheitsgarantien der KI. Es beweist, dass wenn Sie diesen spezifischen mathematischen Regeln folgen, Ihr Modell nicht nur die Vergangenheit auswendig lernt; es wird tatsächlich für die Zukunft lernen.
Die Metapher: Sie haben nicht nur ein Rezept für einen sicheren Kuchen geschrieben; sie haben einen Roboter gebaut, der jede einzelne Zutat und jeden Schritt des Rezepts überprüft, um sicherzustellen, dass der Kuchen niemals zusammenbricht, egal wer ihn isst.

Technische Zusammenfassung: Lean-Formalisierung einer Generalisierungsfehler-Schranke mittels Rademacher-Komplexität und Dudley-Entropieintegral

Problemstellung

Die zentrale Herausforderung besteht in der formalen Verifikation der Generalisierungsleistung im maschinellen Lernen. Konkret zielen die Autoren darauf ab, theoretische Schätzungen des Testfehlers (Populationsrisiko) aus dem Trainingsfehler (empirisches Risiko) unter Verwendung eines maßtheoretischen Rahmens abzuleiten. Während klassische Ansätze auf der Vapnik–Chervonenkis (VC)-Dimension beruhen, sind diese häufig datenunabhängig und auf binäre Klassifikation zugeschnitten. Die moderne Lerntheorie nutzt zunehmend die Rademacher-Komplexität, die scharfe, datenabhängige Schranken liefert, die auf reellwertige Verluste und diverse Funktionsklassen (z. B. Deep Learning, Kernel-Methoden) anwendbar sind. Die Formalisierung dieser Argumente in Beweisassistenten ist jedoch aufgrund der Notwendigkeit einer rigorosen Behandlung von Messbarkeit (insbesondere für Supremata über überabzählbare Hypothesenklassen), Produktmaßen und Konzentrationsungleichungen schwierig.

Methodik

Die Autoren formalisieren die Generalisierungsfehler-Schranke in Lean 4 und nutzen die umfangreiche maßtheoretische Infrastruktur der Wahrscheinlichkeitstheorie der Bibliothek Mathlib. Die Entwicklung folgt der in Lehrbüchern (z. B. Mohri et al., Wainwright) üblichen Standard-Pipeline „Symmetrisierung + beschränkte Differenzen", passt sie jedoch an die Einschränkungen der formalen Verifikation an:

Maßtheoretischer Aufbau: Der Rahmen modelliert die Datengenerierung über einen Wahrscheinlichkeitsraum $(\Omega, m_\Omega, \mu)$ und eine Zufallsvariable $X: \Omega \to \mathcal{X}$ . Stichproben werden als Funktionen $\omega: \text{Fin } n \to \Omega$ modelliert und durch Bildmaße in $S = X \circ \omega$ überführt.
Kerndefinitionen:
- Rademacher-Komplexität: Definiert sowohl für den empirischen Fall (über eine feste Stichprobe $S$ ) als auch für den erwarteten Fall (über das Produktmaß $\mu^n$ ). Die empirische Version mittelt über alle Vorzeichenvektoren $\sigma \in \{-1, 1\}^n$ .
- Uniforme Abweichung: Definiert als das Supremum des Betrags der Differenz zwischen empirischem und Populationsmittel über eine Hypothesenklasse $F = \{f_i\}_{i \in \iota}$ .
Symmetrisierung: Ein formaler Satz (abs_symmetrization_equation) ersetzt das Supremum der Differenzen zwischen zwei unabhängigen Stichproben durch einen Durchschnitt über vorzeicheninvertierte Summen und verknüpft so die uniforme Abweichung mit der Rademacher-Komplexität.
Konzentration: Die Autoren beweisen eine McDiarmid-Ungleichung von Grund auf innerhalb von Lean. Sie zeigen, dass das Funktional der uniformen Abweichung die Eigenschaft der beschränkten Differenzen erfüllt (die Änderung eines Stichprobenpunkts verändert den Wert um höchstens $2b/n$ ), was die Herleitung von Tail-Schranken mit hoher Wahrscheinlichkeit ermöglicht.
Umgang mit überabzählbaren Indexmengen: Eine kritische technische Hürde ist die Messbarkeit von Supremata über überabzählbare Indexmengen $\iota$ $ι$ . Mathlib liefert Messbarkeit für abzählbare Indizes, aber nicht automatisch für überabzählbare. Die Autoren lösen dies durch:
- Zuerst den Beweis von Sätzen für abzählbare Indexmengen.
- Die Erweiterung der Ergebnisse auf separable topologische Indexmengen mittels einer abzählbar-dichten Reduktion. Dies beinhaltet den Nachweis, dass für stetige Funktionen das Supremum über einen separablen Raum gleich dem Supremum über eine abzählbare dichte Teilmenge ist, sofern die Stetigkeit unter Integration erhalten bleibt (gewährleistet durch uniforme Dominanz).

Hauptbeiträge

Der Artikel präsentiert die erste systematische Formalisierung der Generalisierungsanalyse mittels Rademacher-Komplexität. Die spezifischen Beiträge umfassen:

Wiederverwendbare formale Infrastruktur: Eine mechanisch überprüfte Pipeline, die empirische/erwartete Rademacher-Komplexität, Symmetrisierung, Analyse beschränkter Differenzen und die McDiarmid-Ungleichung abdeckt.
Lösung des Messbarkeitsproblems: Ein wiederverwendbarer Mechanismus zum Heben von Ergebnissen von abzählbaren Hypothesenklassen auf separable topologische Parameterräume. Dies verpackt explizit die hinreichenden Bedingungen (Separabilität, erste Abzählbarkeit, uniforme Dominanz und Stetigkeit unter Integration), die erforderlich sind, um überabzählbare Supremata messbar zu machen – ein Schritt, der in informellen Beweisen oft implizit bleibt.
Formalisierte Konzentrationswerkzeuge: Ein vollständiger Beweis der McDiarmid-Ungleichung sowie unterstützende Lemmata für maximale Ungleichungen, Massarts Lemma und Überdeckungszahlen.
Durchgerechnete Anwendungen:
- Lineare Prädiktoren: Formalisierung der Standard-Schranken $O(1/\sqrt{n})$ für $\ell_2$ -regularisierte Prädiktoren und $O(\sqrt{\log(d)/n})$ für $\ell_1$ -regularisierte Prädiktoren.
- Dudley-Entropieintegral: Eine Formalisierung der Dudley-artigen Schranke, die die Rademacher-Komplexität über eine Kettenkonstruktion (chaining) mit Überdeckungszahlen verknüpft. Dies erforderte die Definition empirischer Pseudometriken und die Handhabung des Übergangs von diskreten Ketten-Summen zu Integral-Schranken.

Ergebnisse

Die Formalisierung liefert mechanisch verifizierte Versionen standardmäßiger lerntheoretischer Schranken:

Erwartete Schranke: $E[\text{UD}_n(F)] \leq 2 R_n(F)$ , wobei $R_n(F)$ die Rademacher-Komplexität ist.
Schranke mit hoher Wahrscheinlichkeit: Für jedes $\delta \in (0, 1)$ gilt mit einer Wahrscheinlichkeit von mindestens $1-\delta$ :
$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$
Spezifische Schranken: Das Repository liefert konkrete Beweise für die empirische Rademacher-Komplexität linearer Prädiktoren unter $\ell_2$ - und $\ell_1$ -Beschränkungen sowie für die Dudley-Entropieintegral-Schranke.

Bedeutung und Behauptungen

Die Autoren positionieren diese Arbeit als grundlegenden Schritt hin zu vertrauenswürdiger, zertifizierter Lerntheorie.

Brücke zwischen Theorie und Verifikation: Die Arbeit zeigt, dass moderne, maßtheoretische Lerntheorie (die auf Produktmaßen, Integrierbarkeit von Hüllen und Konzentration beruht) in einem Beweisassistenten formalisiert werden kann, ohne auf übermäßig vereinfachte diskrete Proxy-Modelle zurückzugreifen.
Klärung impliziter Annahmen: Ein Hauptbeitrag ist die explizite Identifizierung der Bedingungen, die für den Umgang mit überabzählbaren Hypothesenklassen erforderlich sind. Die Formalisierung isoliert die „abzählbar-dichte Reduktion" und die spezifischen Stetigkeits-/Integrierbarkeits-Hypothesen, die in Standard-Lehrbüchern oft übersehen werden.
Modularität: Die Entwicklung ist so konzipiert, dass die abstrakte Rademacher-Pipeline wiederverwendet werden kann. Konkrete Schranken werden zu „ausführbaren Korollaren", die durch Instantiierung der Funktionsklasse und Entlastung spezifischer analytischer Abschätzungen (z. B. Normbeschränkungen) erhalten werden.
Vergleich mit vorheriger Arbeit: Im Gegensatz zu früheren Formalisierungen, die auf endliche Hypothesenklassen (z. B. Bagnall & Stewart) oder spezifische algorithmische Fälle (z. B. Entscheidungsstümpfe) beschränkt waren, behandelt diese Arbeit allgemeine, potenziell überabzählbare Funktionsklassen mit reellwertigen Verlusten.

Der Artikel kommt zu dem Schluss, dass, obwohl die mathematischen Schranken selbst klassisch sind, die Formalisierung die präzise logische Struktur und die Nebenbedingungen verdeutlicht, die für ihre Gültigkeit in einem rigorosen Rahmen notwendig sind, und damit eine Grundlage für zukünftige Erweiterungen wie Lipschitz-Kontraktionsungleichungen und Verbindungen zur Gaußschen Komplexität bietet.