Résumé technique : Langages de requête pour les modèles d'apprentissage automatique

Énoncé du problème

L'article traite du défi que représente l'analyse formelle et l'interrogation des modèles d'apprentissage automatique (ML), spécifiquement les réseaux de neurones, qui sont intrinsèquement des « modèles hybrides » combinant des structures discrètes (topologie du graphe) avec des composantes numériques continues (poids et biais). Bien que la théorie des modèles finis ait analysé avec succès les bases de données relationnelles et les problèmes de calcul discrets, les logiques standards manquent de mécanismes pour gérer l'agrégation numérique et l'arithmétique nécessaires pour décrire le comportement de structures pondérées comme les réseaux de neurones.

Les approches existantes de l'analyse du ML reposent souvent sur des méthodes d'explication génériques et fixes (par exemple, des contrefactuels pour des entrées spécifiques) ou traitent les modèles comme des boîtes noires. L'auteur plaide pour une perspective ancrée dans la théorie des bases de données et la théorie des modèles finis, proposant que les modèles de ML soient traités comme des structures de données soumises à des requêtes logiques flexibles. Cela permet l'étude de la fonctionnalité des composants locaux ainsi que des propriétés sémantiques globales (par exemple, la robustesse, la correction ou les intégrales sur l'espace des fonctions) sans être restreint à l'évaluation d'entrées spécifiques.

Méthodologie

L'article étudie deux logiques spécifiques conçues pour les structures finies pondérées (structures avec un univers fini et des fonctions de poids faisant correspondre à des nombres réels étendus, $\mathbb{R}_\perp$) :

1. FO(SUM) : La logique du premier ordre étendue avec un opérateur de sommation ($\sum$) et des termes conditionnels. Cette logique permet l'agrégation des poids sur des ensembles définissables au sein de la structure.
2. IFP(SUM) : L'extension récursive de FO(SUM) utilisant des opérateurs de point fixe inflationnistes. Cela permet de définir des processus inductifs, nécessaires pour évaluer des réseaux de neurones de profondeur non bornée.

La méthodologie comprend :

• La formalisation des réseaux de neurones : Représenter les réseaux de neurones à propagation avant (FNN) comme des graphes orientés acycliques pondérés avec un vocabulaire spécifique ($\{wt, bias, \le_{in}, \le_{out}\}$).
• La définition des sémantiques : Établir la sémantique de ces logiques sur des structures pondérées, où les termes évaluent des valeurs dans $\mathbb{R}_\perp$ et les formules des valeurs booléennes.
• L'analyse de l'expressivité : Déterminer quelles propriétés des FNN (par exemple, l'évaluation, le comptage des paramètres, la recherche d'arêtes inutiles, le calcul d'intégrales) peuvent être exprimées dans ces logiques.
• L'analyse de la complexité : Analyser la complexité des données pour l'évaluation de ces requêtes, en considérant à la fois les classes de complexité de circuits uniformes (par exemple, $\mathsf{TC}^0$) et le temps polynomial ($\mathsf{P}$).
• Les requêtes agnostiques au modèle : Étudier les requêtes dont les résultats dépendent uniquement de la fonction calculée par le réseau ($f^N$) plutôt que de l'architecture ou des poids spécifiques, en distinguant les propriétés « agnostiques au modèle » et « pleinement agnostiques au modèle ».

Contributions clés et résultats

1. Expressivité de FO(SUM)

• Évaluation à profondeur bornée : FO(SUM) peut exprimer l'évaluation de FNN de profondeur bornée. La logique peut définir récursivement la valeur d'un nœud jusqu'à une profondeur $d$ fixée en utilisant la sommation pour agréger les entrées pondérées et des termes conditionnels pour simuler la fonction d'activation ReLU.
• Propriétés globales : La logique peut définir des propriétés globales telles que le nombre total de poids, l'ensemble des arêtes « inutiles » (arêtes dont le retrait ne modifie pas la sortie), et des intégrales sur la fonction calculée par le réseau (via la décomposition en cellules cylindriques de fonctions linéaires par morceaux).
• Limitations sur la profondeur non bornée : FO(SUM) ne peut pas exprimer la fonction d'évaluation pour des FNN de profondeur non bornée. La logique est limitée aux propriétés locales ; elle ne peut pas simuler la récursion non bornée requise pour l'évaluation générale des FANN.
• Limitations de l'agnosticisme au modèle : Un résultat négatif central (Théorème 3.14) stipule que toute phrase FO(SUM) qui est agnostique au modèle (invariante par rapport à différentes architectures calculant la même fonction) sur la classe de tous les FNN doit être triviale (soit vraie pour tous, soit fausse pour tous). Ainsi, les requêtes non triviales agnostiques au modèle (comme vérifier si un réseau produit zéro partout) ne sont pas exprimables dans FO(SUM) pour une profondeur non bornée.
• Équivalence de profondeur bornée : Cependant, pour les FNN de profondeur bornée ($N_d(m, 1)$), FO(SUM) est étonnamment puissante. Le Théorème 3.18 établit que toute requête exprimable dans la logique du premier ordre sur le corps ordonné des réels étendue par la fonction ($FO(\mathbb{R}_{lin}, f)$) est également exprimable dans FO(SUM). Ceci est réalisé en simulant la quantification sur les réels via la quantification sur les cellules de la décomposition cylindrique de la fonction.

2. Expressivité de IFP(SUM)

• Profondeur non bornée : IFP(SUM) surmonte la limitation de profondeur de FO(SUM) en introduisant des opérateurs de point fixe. Elle peut exprimer la fonction d'évaluation pour des FNN de profondeur non bornée (Exemple 4.1).
• Complexité et fragments scalaires : Bien que la logique de point fixe standard sur les structures ordonnées capture le temps polynomial, l'IFP(SUM) sur des structures pondérées fait face à un obstacle de complexité : les termes peuvent croître exponentiellement en taille (par exemple, le carré répété). Pour y remédier, l'article introduit le fragment scalaire sIFP(SUM), qui restreint les multiplications et divisions impliquant des symboles intentionnels.
  • Théorème 4.5 : La complexité des données de sIFP(SUM) est dans P (temps polynomial) sur les structures pondérées rationnelles.
• Limites d'expressivité : Malgré la capture du temps polynomial dans le modèle de Blum-Shub-Smale, l'IFP(SUM) (et l'sIFP(SUM)) ne peut pas exprimer toutes les requêtes agnostiques au modèle calculables en temps polynomial. Le Théorème 4.7 démontre l'existence d'une requête agnostique au modèle décidable en temps polynomial sur $N(1, 1)$ qui n'est pas exprimable dans l'IFP(SUM), même avec des poids binaires. Cette limitation provient de l'incapacité de la logique à effectuer des calculs arbitraires sur les valeurs numériques (absence de variables allant sur les nombres).
• FNN réduits : L'article introduit les « FNN réduits » (factorisation par une équivalence de type bisimularité). Le Théorème 4.8 montre que pour les FNN dont la forme réduite possède des poids de taille de bits bornée, l'sIFP(SUM) capture toutes les requêtes agnostiques au modèle décidables en temps polynomial.

3. Résultats de complexité

• FO(SUM) : La complexité des données pour l'évaluation des expressions FO(SUM) est dans $\mathsf{TC}^0$ uniforme (Théorème 3.9). Cette classe permet les portes de seuil et l'addition itérée, suffisantes pour les opérations arithmétiques requises.
• sIFP(SUM) : Sa complexité des données est dans P (Théorème 4.5).

Signification et affirmations

L'article se positionne comme une « perspective personnelle » et une étape fondamentale de l'application de la théorie des modèles finis à l'apprentissage automatique. Sa signification principale réside dans :

1. La formalisation de l'interrogation du ML : Il fournit un cadre logique rigoureux pour interroger la sémantique interne des réseaux de neurones, passant de l'évaluation boîte noire à l'analyse structurelle et fonctionnelle.
2. Le pont entre discret et continu : Il démontre comment la méta-théorie des modèles finis (étendant la théorie des modèles finis aux structures hybrides) peut être appliquée aux réseaux de neurones, qui sont naturellement représentés comme des graphes pondérés.
3. La définition des limites d'expressivité : Les résultats délimitent clairement les frontières entre ce qui peut et ne peut pas être exprimé logiquement. Notamment, il souligne que si les réseaux de profondeur bornée sont propices à l'analyse logique via FO(SUM), la profondeur non bornée introduit une complexité qui nécessite la récursion (IFP) mais fait toujours face à des barrières fondamentales d'expressivité concernant les propriétés agnostiques au modèle.
4. Aperçus de complexité : Le travail relie l'expressivité logique à la complexité computationnelle, montrant que même avec des opérateurs de point fixe, la capture de toutes les propriétés agnostiques au modèle en temps polynomial nécessite des restrictions sur la taille de bits des poids.

L'auteur conclut que bien que des progrès significatifs aient été réalisés dans [22, 23], de nombreuses questions restent ouvertes, particulièrement concernant l'extension des résultats à des dimensions d'entrée arbitraires, le passage des hypothèses de profondeur bornée sans hypothèses de complexité, et l'inter-définissabilité de différents opérateurs d'agrégation. L'article ne prétend pas résoudre entièrement le problème de « l'IA explicable », mais offre un outil théorique pour définir et analyser des types spécifiques d'explications et de vérifications.