💬 NLP

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

Cet article présente la première formalisation complète en Lean 4 de la théorie de l'apprentissage statistique fondée sur les processus empiriques, développée via un flux de travail collaboratif humain-IA afin d'établir une fondation formelle réutilisable qui résout les hypothèses implicites des manuels standards et permet de futurs développements de la théorie de l'apprentissage automatique.

Auteurs originaux : Yuanhe Zhang, Jason D. Lee, Fanghui Liu

Publié 2026-06-11

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yuanhe Zhang, Jason D. Lee, Fanghui Liu

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 essayiez d'apprendre à un ordinateur à apprendre à partir de données, comme un élève étudiant pour un examen de mathématiques. La Théorie de l'Apprentissage Statistique (SLT - Statistical Learning Theory) est le livre de règles qui nous dit pourquoi cet élève réussira probablement l'examen et avec quel niveau de performance. C'est la « physique » derrière l'apprentissage automatique.

Cependant, ce livre de règles est écrit dans un langage très complexe et de haut niveau (mathématiques avancées). Pendant des décennies, les humains l'ont lu, en ont compris l'idée générale, puis sont passés à autre chose. Mais parce que les preuves sont longues et reposent sur des hypothèses subtiles et cachées, il est facile de manquer un minuscule écart logique. C'est comme lire une recette qui dit « mélanger jusqu'à ce que ce soit lisse » sans définir ce que signifie réellement « lisse ». Si vous essayez de construire un robot chef basé sur cette recette vague, il risque d'échouer.

Ce document, AI4SLT, consiste à construire une version numérique parfaite et incassable de ce livre de règles en utilisant un outil appelé Lean 4. Considérez Lean 4 comme un correcteur ultra-strict qui refuse d'accepter le moindre mot vague. Si une étape de la logique n'est pas explicitement définie, Lean 4 s'arrête et dit : « Je ne peux pas faire cela. »

Voici ce que les auteurs ont fait, expliqué à travers des analogies simples :

1. L'équipe Humain-IA : L'Architecte et le Maçon

Les auteurs n'ont pas simplement demandé à une IA d'« écrire le code ». Ils ont utilisé un flux de travail collaboratif :

Les Humains (Architectes) : Ils ont examiné les manuels de mathématiques complexes et conçu la stratégie. Ils ont dit : « Nous devons d'abord prouver cette partie spécifique, et voici le plan. »
L'IA (Le Maçon) : L'IA (plus précisément Claude Code) a pris ce plan et a effectué le travail lourd consistant à écrire le code réel, en remplissant les étapes logiques minuscules et fastidieuses.
Le Résultat : Ils ont construit une immense bibliothèque d'environ 30 000 lignes de code. C'est comme construire un gratte-ciel de fond en comble, brique par brique, où chaque brique a été inspectée par un robot pour s'assurer qu'elle s'ajuste parfaitement.

2. Construire les Fondations : La « Boîte à Outils Gaussienne »

Pour prouver que l'apprentissage automatique fonctionne, vous devez comprendre comment le bruit aléatoire se comporte. Le document a construit une boîte à outils complète pour cela, ce qui n'avait jamais été fait de manière vérifiable par ordinateur.

L'Analogie : Imaginez que vous essayiez de prédire la météo. Vous devez comprendre comment le vent, la pluie et la température interagissent. Les auteurs ont construit les capteurs de « vent », de « pluie » et de « température » à partir de zéro à l'intérieur de l'ordinateur.
Ce qu'ils ont construit : Ils ont formalisé des outils mathématiques complexes comme la concentration de Lipschitz gaussienne et l'intégrale d'entropie de Dudley.
- Traduction simple : Ces outils aident à calculer le « pire scénario » de la façon dont un algorithme d'apprentissage pourrait se tromper à cause de la chance ou du hasard. Le document a prouvé que même dans le pire des cas, l'algorithme reste dans une limite prévisible et sûre.

3. L'astuce du « Chaining » : Grimper une Montagne

L'une des parties les plus difficiles des mathématiques est appelée l'intégrale d'entropie de Dudley.

L'Analogie : Imaginez que vous deviez grimper une montagne très haute et brumeuse (le « processus empirique »). Vous ne voyez pas le sommet.
L'Ancienne Méthode : Les manuels disent souvent : « Supposez simplement que vous voyez le sommet. »
La Méthode du Document : Ils ont construit une échelle de plateformes (appelée « chaining » ou chaînage). Vous ne sautez pas directement au sommet ; vous passez d'une petite plateforme à une plateforme légèrement plus haute, puis à une autre plus haute, et ainsi de suite.
L'Accomplissement : Les auteurs ont formalisé tout ce système d'échelle dans Lean 4. Ils ont prouvé que si vous faites ces petits sauts sécurisés, vous pouvez mathématiquement garantir que vous ne tomberez pas de la montagne. Cela permet de prédire exactement la quantité de données dont vous avez besoin pour apprendre une tâche spécifique.

4. Tester le Moteur : Le Test des Moindres Carrés

Une fois la boîte à outils construite, ils l'ont testée sur un problème du monde réel : la Régression des Moindres Carrés (une méthode courante pour tracer une ligne à travers un ensemble de points).

Le Résultat : Ils ont utilisé leur nouveau livre de règles numériques ultra-strict pour prouver que cette méthode fonctionne, et ils ont calculé la vitesse exacte à laquelle elle apprend.
Pourquoi c'est important : Ils n'ont pas seulement dit « ça fonctionne ». Ils ont prouvé à quelle vitesse cela fonctionne, jusqu'au plus petit détail, et ont montré que leur méthode atteint la meilleure vitesse possible (taux minimax) pour ce type de problèmes.

5. Le Bénéfice Caché : Trouver les Hypothèses « Fantômes »

La partie la plus surprenante du document est ce qui s'est passé pendant le processus.

L'Analogie : Lorsque vous essayez de construire une maison avec un robot qui exige des instructions parfaites, vous réalisez que vos plans originaux omettaient des détails cruciaux comme « la porte a besoin d'une charnière » ou « le sol doit être de niveau ».
La Découverte : Les auteurs ont découvert que les manuels de mathématiques standards omettent souvent des détails minuscules mais cruciaux (comme le fait qu'une fonction soit « mesurable » ou « continue »). L'IA ne pouvait pas procéder tant que ces points n'étaient pas corrigés.
Le Résultat : En forçant l'ordinateur à vérifier chaque ligne, ils ont nettoyé la théorie, la rendant plus rigoureuse et exposant les hypothèses cachées que les humains avaient négligées pendant des années.

Résumé

Ce document est la première fois que quelqu'un prend le « livre de règles » complexe et abstrait de la théorie de l'apprentissage automatique pour le reconstruire entièrement à l'intérieur d'un système informatique qui vérifie chaque étape logique. Ils ont utilisé une équipe d'humains pour concevoir le plan et l'IA pour construire la structure. Le résultat est une fondation vérifiée et sans erreur qui prouve que les algorithmes d'apprentissage automatique fonctionnent, explique exactement à quelle vitesse ils apprennent, et corrige les failles cachées dans les théories mathématiques originales.

Résumé Technique : AI4SLT : Processus Empiriques en Lean 4 pour la Théorie Statistique de l'Apprentissage Formelle

Énoncé du Problème

La Théorie Statistique de l'Apprentissage (SLT) guide avec succès le progrès de l'apprentissage automatique depuis des décennies, fournissant des concepts fondamentaux tels que les compromis biais-variance et la régularisation. Cependant, à mesure que les modèles évoluent vers des architectures complexes (par exemple, les réseaux de neurones profonds, les grands modèles de langage), les analyses théoriques contemporaines sont devenues de plus en dé plus complexes, s'appuyant sur des outils mathématiques avancés issus de l'analyse fonctionnelle et de la physique statistique. Cette complexité met à l'épreuve la vérification humaine, rendant difficile le suivi des dépendances logiques et la vérification des lemmes intermédiaires à grande échelle.

De plus, les techniques de base de la SLT, telles que les inégalités de concentration et les arguments de recouvrement, manquent d'une bibliothèque structurée et lisible par machine, ce qui limite leur réutilisabilité. Bien que les prouveurs de théorèmes interactifs comme Lean 4 offrent une voie vers la correction vérifiable par machine, les formalisations existantes en apprentissage automatique sont limitées à des domaines spécifiques (par exemple, l'apprentissage par renforcement, l'optimisation) ou à des contextes simplifiés (par exemple, les bornes de généralisation via la complexité de Rademacher sur des classes de fonctions entières). Une formalisation complète du cadre des processus empiriques localisés — essentiel pour dériver des taux minimax précis dans les contextes de haute dimension et non paramétriques — demeure absente. Ce cadre nécessite une gestion rigoureuse de la mesurabilité, de l'intégrabilité et des hypothèses topologiques qui sont souvent laissées implicites dans les manuels standards.

Méthodologie

Les auteurs présentent AI4SLT, la première formalisation complète de la SLT fondée sur la théorie des processus empiriques dans Lean 4. Le projet a été exécuté en utilisant un flux de travail collaboratif humain-IA :

Rôle Humain : Les mathématiciens ont conçu les stratégies de preuve, analysé l'infrastructure existante de Mathlib, décomposé les théorèmes complexes en lemmes gérables et vérifié la cohérence des énoncés.
Rôle de l'IA : Des agents d'IA (spécifiquement Claude Code avec Opus-4.5) ont exécuté la construction tactique des preuves, comblant les détails basés sur des spécifications structurées.

Le flux de travail impliquait un protocole de spécification structuré (TASK.md) contenant les énoncés cibles, les pointeurs d'infrastructure, les plans de preuve orientés vers la formalisation et les limites strictes. Le processus mettait l'accent sur le raffinement itératif, où les échecs de l'IA servaient à identifier les hypothèses implicites laissées par les humains, menant à une collaboration convergente plutôt qu'ouverte. L'ensemble du projet a couvert environ 500 heures de développement supervisé, aboutissant à environ 30 000 lignes de code Lean 4 compilées sans sorry (buts non prouvés) ou axiomes personnalisés.

Contributions Clés

1. Boîte à Outils de Concentration de Lipschitz Gaussienne

Les auteurs ont construit un développement formel complet de la concentration de Lipschitz gaussienne, un outil fondamental en probabilité de haute dimension. Cela a nécessité la construction d'une infrastructure substantielle à partir de zéro, incluant :

Inégalité d'Efron-Stein : Formalisée avec un lemme de transfert universel pour gérer les mises à jour par coordonnée avec des distributions distinctes.
Inégalité de Poincaré Gaussienne : Dérivée en utilisant l'infrastructure d'Efron-Stein et des bornes d'expansion de Taylor.
Arguments de Densité : Formalisation de l'extension des inégalités des fonctions lisses à support compact ( $C^\infty_c$ ) vers les classes générales de Lipschitz et $C^1$ via les espaces de Sobolev gausiens ( $W^{1,2}$ ) et les techniques de mollification.
Inégalité de Log-Sobolev Gaussienne (LSI) : Formalisation de la tensorisation de la LSI 1D vers le cas $n$ -dimensionnel en utilisant la sous-additivité de l'entropie.
Concentration de Lipschitz Gaussienne : Dérivation de la borne de concentration finale en utilisant l'argument de Herbst et la borne de Chernoff.

À la connaissance des auteurs, cela constitue la première formalisation complète des outils d'analyse gaussienne dans n'importe quel prouveur de théorèmes.

2. Intégrale d'Entropie de Dudley pour les Processus Sub-Gaussiens

Le document fournit la première formalisation du théorème de l'intégrale d'entropie de Dudley pour les processus sub-gaussiens dans Lean 4. Ce résultat limite l'espérance de la borne supérieure d'un processus stochastique par une intégrale impliquant l'entropie métrique.

Défis de Formalisation : Les auteurs ont abordé la nécessité d'arguments de chaînage rigoureux, décomposant le processus en une somme télescopique sur des approximations dyadiques. Ils ont formalisé les nombres de recouvrement et de paquetage dans les espaces métriques et ont géré l'intégration des réels non négatifs étendus ( $\mathbb{R}_{\ge 0}^\infty$ ) par rapport aux fonctions à valeurs réelles, garantissant que la borne est applicable aux processus sub-gaussiens généraux.

3. Application : Cadre des Moindres Carrés via les Processus Empiriques Localisés

Les auteurs ont démontré l'utilité pratique de leur infrastructure en développant un cadre unifié pour la régression des moindres carrés basé sur le processus empirique localisé.

Borne d'Erreur Maîtresse : Ils ont formalisé l'inégalité critique reliant l'erreur de prédiction au rayon critique $\delta^*$ , dérivée de la complexité gaussienne localisée.
Taux Précis : Le cadre a été appliqué à la régression linéaire et à la régression sous contrainte $\ell_1$ (Lasso). En bornant les nombres de recouvrement (en utilisant la réduction euclidienne et la méthode empirique de Maurey pour les enveloppes convexes $\ell_1$ ), les auteurs ont obtenu des taux précis jusqu'au niveau minimax, récupérant des résultats tels que $O(\sigma^2 r/n)$ pour la régression linéaire et $O(R\sqrt{\log d/n})$ pour la régression parcimonieuse de haute dimension.

4. Paradigme de Formalisation Collaboratif Humain-IA

Le document détaille une méthodologie pour la formalisation à grande échelle :

Spécifications Structurées : Réduction des taux d'échec dès la première tentative de ~70 % à ~15 % en fournissant des pointeurs d'infrastructure explicites et des plans de preuve au niveau des tactiques.
Évolution Itérative : Utilisation des échecs de l'IA pour faire émerger les hypothèses humaines implicites (ex: mesurabilité, intégrabilité, contraintes de domaine) et raffiner les spécifications de manière itérative.
Décomposition Quantitative : Environ 40 % des déclarations ont été prouvées sous des plans de preuve en langage naturel complet, 30 % sous forme de croquis guidés, 15 % de manière autonome, et 15 % ont nécessité une intervention humaine critique (ex: correction de stratégies mathématiques erronées ou vérification de la cohérence des énoncés).

Résultats

Base de Code : Une bibliothèque d'environ 30 000 lignes de code Lean 4 contenant plus de 1 000 théorèmes et lemmes.
Complétude : Toutes les formalisations compilent sans sorry ni axiomes, garantissant la correction vérifiable par machine.
Résolution des Écarts : La formalisation a exposé et résolu les hypothèses implicites dans les manuels de SLT standards, telles que les conditions de mesurabilité pour les variables aléatoires de supremum, l'intégrabilité des fonctionnelles d'entropie et la non-vacuité des sphères empiriques.
Performance : Le cadre a réussi à dériver des taux minimax précis pour les contextes de régression tant paramétriques (linéaire) que non paramétriques (parcimonieuse), validant l'utilité de l'approche par processus empirique localisé.

Signification

Le document affirme que ce travail établit une fondation formelle réutilisable pour la théorie de l'apprentissage statistique. En allant au-delà de la simple traduction mécanique pour atteindre une compréhension granulaire, ligne par ligne, de la théorie, le projet impose un standard de rigueur qui clarifie les dépendances logiques et les hypothèses cachées.

La signification est double :

Rigueur Théorique : Il fournit une bibliothèque vérifiée par machine pour la SLT, permettant une analyse théorique automatisée et scalable des systèmes d'apprentissage automatique et servant de terrain d'entraînement principalisé pour les étudiants souhaitant maîtriser l'ensemble de la pile technique de la SLT.
Avancement Méthodologique : Il démontre que les projets de formalisation à grande échelle peuvent être considérablement accélérés grâce à une collaboration humain-IA bien conçue, offrant un modèle pour les développements futurs de la théorie de l'apprentissage automatique et d'autres domaines mathématiques complexes.

Les auteurs soulignent que ce travail n'est pas seulement un exercice de rigueur mais une étape nécessaire pour gérer la complexité croissante de la théorie de l'apprentissage automatique moderne, ouvrant la voie à de futurs développements formels dans le domaine.