💬 NLP

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

Cet article présente une formalisation en Lean 4 de bornes d'erreur de généralisation basées sur la complexité de Rademacher et l'intégrale d'entropie de Dudley, mettant en œuvre un pipeline mécaniquement vérifié allant des fondements de la théorie de la mesure aux bornes de déviation uniforme à haute probabilité et à leur application aux prédicteurs linéaires.

Auteurs originaux : Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda

Publié 2026-05-26

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un chef qui vient d'inventer une nouvelle recette. Vous l'avez cuisinée 100 fois dans votre cuisine (les données d'entraînement) et elle était parfaite à chaque fois. Mais vous voulez savoir : si vous cuisinez cette même recette pour un million d'inconnus dans un restaurant (les données de test), sera-t-elle toujours aussi bonne ?

Dans le monde de l'apprentissage automatique, c'est ce qu'on appelle le problème de généralisation. L'article dont vous parlez est une preuve rigoureuse, vérifiée par ordinateur, qui nous aide à répondre à cette question avec certitude mathématique.

Voici l'histoire de l'article, décomposée en concepts et analogies simples.

1. Le Problème : Le fossé « Cuisine vs Restaurant »

Lorsqu'un ordinateur apprend, il tente de trouver une règle (une hypothèse) qui correspond aux données qu'il observe.

Erreur d'entraînement : Dans quelle mesure la règle correspond aux données qu'il a déjà vues (vos 100 essais en cuisine).
Erreur de test : Dans quelle mesure la règle fonctionne sur de nouvelles données qu'il n'a pas encore vues (les clients du restaurant).

Le danger est le surapprentissage (overfitting). C'est comme un chef qui mémorise le goût exact de ses 100 essais mais ne comprend pas les principes de la cuisine. S'il rencontre un ingrédient légèrement différent au restaurant, le plat échoue. Nous avons besoin d'un moyen de garantir que le « succès en cuisine » se traduit par un « succès au restaurant ».

2. L'Outil : La Complexité de Rademacher (Le « Test de pile ou face »)

Pour mesurer la probabilité qu'une recette surapprenne, les mathématiciens utilisent un outil appelé Complexité de Rademacher.

Imaginez que vous avez un sac de pièces de monnaie. Vous les lancez, et elles tombent sur Face (+1) ou Pile (-1) complètement au hasard.

Le Test : Vous demandez à votre recette (l'algorithme d'apprentissage) : « Pouvez-vous prédire ces lancers de pièces aléatoires ? »
La Logique : Si votre recette est une règle simple et robuste, elle ne devrait pas pouvoir prédire un bruit aléatoire. Elle devrait avoir raison environ 50 % du temps, simplement par hasard.
Le Drapeau Rouge : Si votre recette est trop complexe (comme un chef qui a mémorisé chaque détail), elle pourrait accidentellement « trouver un motif » dans les lancers de pièces aléatoires et les prédire mieux que le hasard.

La Complexité de Rademacher mesure exactement à quel point un modèle peut « tricher » en s'adaptant à un bruit aléatoire. Plus ce nombre est bas, plus il est probable que le modèle généralise bien à de nouvelles données.

3. La Réalisation : Le « Double-Vérification Numérique »

Les auteurs de cet article n'ont pas seulement écrit ces preuves mathématiques sur papier ; ils les ont construites à l'intérieur d'un programme informatique appelé Lean 4.

Pensez à Lean 4 comme à un éditeur ultra-sévère, impitoyable.

L'Ancienne Méthode : Un mathématicien écrit une preuve sur papier. Un réviseur humain la lit. Si l'humain manque une petite faille logique, la preuve peut être acceptée même si elle est légèrement erronée.
La Nouvelle Méthode (Cet Article) : Les auteurs ont soumis l'intégralité de leur preuve à Lean. L'ordinateur a vérifié chaque étape, chaque définition et chaque hypothèse. S'il y avait même un tout petit lien manquant (comme « Cette fonction est-elle mesurable ?»), l'ordinateur la rejetait.

L'article prétend avoir construit un pipeline vérifié mécaniquement. Il commence par les définitions de base, passe par un tour de passe-passe de « symétrisation » (un remaniement mathématique astucieux), et se termine par une garantie de haute confiance que l'erreur de test ne sera pas beaucoup pire que l'erreur d'entraînement.

4. Le Grand Obstacle : Le Problème de la « Bibliothèque Infinie »

Dans le monde réel, les modèles d'apprentissage automatique ont souvent des possibilités infinies (comme une plage continue de nombres pour les poids).

Le Problème : En mathématiques, il est facile de vérifier une liste finie d'éléments (comme 100 recettes). Il est beaucoup plus difficile de vérifier une liste infinie. En termes informatiques, vérifier le « maximum » d'une liste infinie peut parfois enfreindre les règles de la logique (problèmes de mesurabilité).
La Solution de l'Article : Les auteurs ont créé un « pont » astucieux. Ils ont d'abord prouvé les mathématiques pour un ensemble dénombrable (fini ou énumérable) d'hypothèses. Ensuite, ils ont montré que pour de nombreux modèles réels (qui sont des espaces topologiques « séparables »), on peut approximer l'ensemble infini en utilisant un sous-ensemble dense dénombrable (comme utiliser une grille très fine pour approximer une courbe lisse).
L'Analogie : Imaginez essayer de mesurer la taille de chaque personne possible dans le monde. Il est impossible de mesurer tout le monde. Mais si vous mesurez chaque personne dont la taille diffère exactement de 1 cm, vous pouvez prouver mathématiquement que votre mesure couvre tout le monde avec une grande précision. L'article a formalisé ce tour de passe-passe de la « grille » afin que l'ordinateur l'accepte.

5. Les Résultats : Qu'ont-ils prouvé ?

Une fois le « moteur » construit, ils l'ont fait passer à travers trois scénarios spécifiques pour montrer qu'il fonctionne :

Prédicteurs linéaires avec régularisation $\ell_2$ : C'est comme un modèle forcé à garder ses « ingrédients » (poids) petits et équilibrés. L'article a prouvé la borne mathématique standard pour cela.
Prédicteurs linéaires avec régularisation $\ell_1$ : Cela force le modèle à être « épars » (n'utilisant que quelques ingrédients). Ils ont prouvé la borne pour cela, ce qui implique un calcul légèrement différent (impliquant la racine carrée du nombre de caractéristiques).
Intégrale d'entropie de Dudley : C'est un outil plus avancé et général. Imaginez que vous avez une forme très désordonnée et complexe. Au lieu de mesurer l'ensemble, vous la recouvrez de formes plus petites et plus simples (comme recouvrir un rocher bosselé de galets lisses). L'article a formalisé comment calculer la complexité en fonction du nombre de « galets » nécessaires pour recouvrir la forme.

Résumé

Cet article est une réalisation d'ingénierie fondamentale.

Ce qu'ils ont fait : Ils ont pris des théories complexes de manuels sur la façon dont les modèles d'apprentissage automatique généralisent (complexité de Rademacher) et les ont traduites dans un langage qu'un ordinateur peut vérifier avec 100 % de certitude.
Pourquoi c'est important : Cela élimine l'« erreur humaine » des garanties de sécurité les plus critiques de l'IA. Cela prouve que si vous suivez ces règles mathématiques spécifiques, votre modèle ne se contentera pas de mémoriser le passé ; il apprendra réellement pour le futur.
La Métaphore : Ils n'ont pas seulement écrit une recette pour un gâteau sûr ; ils ont construit un robot qui vérifie chaque ingrédient et chaque étape de la recette pour garantir que le gâteau ne s'effondrera jamais, peu importe qui le mange.

Résumé technique : Formalisation en Lean de la borne d'erreur de généralisation par la complexité de Rademacher et l'intégrale d'entropie de Dudley

Énoncé du problème

Le défi central abordé est la vérification formelle des performances de généralisation en apprentissage automatique. Plus précisément, les auteurs visent à dériver des estimations théoriques de l'erreur de test (risque populationnel) à partir de l'erreur d'entraînement (risque empirique) en utilisant un cadre théorique de la mesure. Alors que les approches classiques reposent sur la dimension de Vapnik–Chervonenkis (VC), celles-ci sont souvent indépendantes des données et adaptées à la classification binaire. La théorie de l'apprentissage moderne utilise de plus en plus la complexité de Rademacher, qui fournit des bornes précises, dépendantes des données, applicables aux pertes à valeurs réelles et à des classes de fonctions diverses (par exemple, l'apprentissage profond, les méthodes à noyaux). Cependant, la formalisation de ces arguments dans des assistants de preuve est difficile en raison de la nécessité de traiter rigoureusement la mesurabilité (en particulier pour les supremums sur des classes d'hypothèses non dénombrables), les mesures produits et les inégalités de concentration.

Méthodologie

Les auteurs formalisent la borne d'erreur de généralisation en Lean 4, en tirant parti de l'infrastructure probabiliste théorique de la mesure étendue de la bibliothèque Mathlib. Le développement suit le pipeline standard « symétrisation + différences bornées » trouvé dans les manuels (par exemple, Mohri et al., Wainwright), mais l'adapte aux contraintes de la vérification formelle :

Cadre théorique de la mesure : Le cadre modélise la génération de données via un espace probabilisé $(\Omega, m_\Omega, \mu)$ et une variable aléatoire $X: \Omega \to \mathcal{X}$ . Les échantillons sont modélisés comme des fonctions $\omega: \text{Fin } n \to \Omega$ , poussées vers l'avant pour obtenir $S = X \circ \omega$ .
Définitions fondamentales :
- Complexité de Rademacher : Définie à la fois pour les cas empirique (sur un échantillon fixe $S$ ) et espéré (sur la mesure produit $\mu^n$ ). La version empirique moyenne sur tous les vecteurs de signes $\sigma \in \{-1, 1\}^n$ .
- Déviation uniforme : Définie comme le supremum de la différence absolue entre les moyennes empirique et populationnelle sur une classe d'hypothèses $F = \{f_i\}_{i \in \iota}$ .
Symétrisation : Un théorème formel (abs_symmetrization_equation) remplace le supremum des différences entre deux échantillons indépendants par une moyenne sur des sommes à signes inversés, reliant la déviation uniforme à la complexité de Rademacher.
Concentration : Les auteurs prouvent une inégalité de McDiarmid à partir de zéro dans Lean. Ils établissent que le fonctionnel de déviation uniforme satisfait la propriété de différences bornées (changer un point d'échantillon modifie la valeur d'au plus $2b/n$ ), permettant la dérivation de bornes de queue à haute probabilité.
Gestion des ensembles d'indices non dénombrables : Un obstacle technique critique est la mesurabilité des supremums sur des ensembles d'indices non dénombrables $\iota$ $ι$ . Mathlib fournit la mesurabilité pour des indices dénombrables, mais pas automatiquement pour des indices non dénombrables. Les auteurs résolvent cela en :
- Prouvant d'abord des théorèmes pour des ensembles d'indices dénombrables.
- Étendant les résultats à des ensembles d'indices topologiques séparables via une réduction dénombrable dense. Cela implique de prouver que pour des fonctions continues, le supremum sur un espace séparable est égal au supremum sur un sous-ensemble dénombrable dense, à condition que la continuité soit préservée sous intégration (assurée par une domination uniforme).

Contributions clés

L'article présente la première formalisation systématique de l'analyse de généralisation via la complexité de Rademacher. Les contributions spécifiques incluent :

Infrastructure formelle réutilisable : Un pipeline vérifié mécaniquement couvrant la complexité de Rademacher empirique/espérée, la symétrisation, l'analyse des différences bornées et l'inégalité de McDiarmid.
Résolution de la mesurabilité : Un mécanisme réutilisable pour relever les résultats des classes d'hypothèses dénombrables vers des espaces de paramètres topologiques séparables. Cela regroupe explicitement les conditions suffisantes (séparabilité, premier axiome de dénombrabilité, domination uniforme et continuité sous intégration) requises pour rendre les supremums non dénombrables mesurables, une étape souvent implicite dans les preuves informelles.
Outils de concentration formalisés : Une preuve complète de l'inégalité de McDiarmid et des lemmes de soutien pour les inégalités maximales, le lemme de Massart et les nombres de couverture.
Applications détaillées :
- Prédicteurs linéaires : Formalisation des bornes standards $O(1/\sqrt{n})$ pour les prédicteurs régularisés en $\ell_2$ et des bornes $O(\sqrt{\log(d)/n})$ pour les prédicteurs régularisés en $\ell_1$ .
- Intégrale d'entropie de Dudley : Une formalisation de la borne de type Dudley reliant la complexité de Rademacher aux nombres de couverture via une construction de chaînage. Cela a nécessité la définition de pseudo-métriques empiriques et la gestion de la transition des sommes de chaînage discrètes vers les bornes intégrales.

Résultats

La formalisation produit des versions vérifiées mécaniquement des bornes standard de la théorie de l'apprentissage :

Borne espérée : $E[\text{UD}_n(F)] \leq 2 R_n(F)$ , où $R_n(F)$ est la complexité de Rademacher.
Borne à haute probabilité : Pour tout $\delta \in (0, 1)$ , avec une probabilité d'au moins $1-\delta$ :
$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$
Bornes spécifiques : Le dépôt fournit des preuves concrètes de la complexité de Rademacher empirique des prédicteurs linéaires sous contraintes $\ell_2$ et $\ell_1$ , ainsi que de la borne de l'intégrale d'entropie de Dudley.

Importance et affirmations

Les auteurs positionnent ce travail comme une étape fondamentale vers une théorie de l'apprentissage automatique fiable et certifiée.

Pont entre théorie et vérification : Le travail démontre que la théorie de l'apprentissage moderne, théorique de la mesure (qui repose sur les mesures produits, l'intégrabilité des enveloppes et la concentration), peut être formalisée dans un assistant de preuve sans recourir à des proxies discrets excessivement simplifiés.
Clarification des hypothèses implicites : Une contribution majeure est l'identification explicite des conditions requises pour gérer les classes d'hypothèses non dénombrables. La formalisation isole la « réduction dénombrable dense » et les hypothèses spécifiques de continuité/intégrabilité nécessaires, qui sont souvent passées sous silence dans les manuels standards.
Modularité : Le développement est conçu de manière à ce que le pipeline abstrait de Rademacher puisse être réutilisé. Les bornes concrètes deviennent des « corollaires exécutables » obtenus en instanciant la classe de fonctions et en acquittant des estimations analytiques spécifiques (par exemple, contraintes de norme).
Comparaison avec les travaux antérieurs : Contrairement aux formalisations précédentes limitées à des classes d'hypothèses finies (par exemple, Bagnall & Stewart) ou à des cas algorithmiques spécifiques (par exemple, les决策 stumps), ce travail gère des classes de fonctions générales, potentiellement non dénombrables, avec des pertes à valeurs réelles.

L'article conclut que, bien que les bornes mathématiques elles-mêmes soient classiques, la formalisation clarifie la structure logique précise et les conditions secondaires nécessaires à leur validité dans un cadre rigoureux, fournissant une base pour de futures extensions telles que les inégalités de contraction de Lipschitz et les liens avec la complexité gaussienne.