Résumé Technique : Les réseaux de neurones à virgule flottante sont des approximateurs universels prouvables

1. Énoncé du problème

Le théorème classique de l'approximation universelle (UA) et le théorème plus récent de l'approximation universelle par intervalles (IUA) établissent que les réseaux de neurones peuvent approximer des fonctions continues et leurs applications d'image directe (intervalles) avec une précision arbitraire. Cependant, ces résultats théoriques reposent sur l'hypothannie irréaliste que les réseaux de neurones opèrent sur des nombres réels d'une précision infinie. En pratique, les implémentations logicielles utilisent l'arithmétique à virgule flottante à précision finie, ce qui introduit une discrétisation, une bornage, des erreurs d'arrondi et des risques de dépassement de capacité (overflow) ou de sous-capacité (underflow).

La question centrale adressée par cet article est de savoir si le théorème IUA est valable dans le cadre de la virgule flottante. Plus précisément, un réseau de neurones à virgule flottante, lorsqu'il est analysé via l'interprétation abstraite (domaine d'intervalles), peut-il capturer parfaitement l'application d'image directe d'une fonction cible arrondie ? Les travaux précédents n'ont pas établi cela, principalement parce que les erreurs d'arrondi inhérentes aux opérations en virgule flottante invalident les techniques de preuve utilisées pour les réseaux à valeurs réelles (par exemple, la construction de sous-réseaux spécifiques reposant sur une arithmétique exacte échoue en raison de l'arrondi).

2. Méthodologie

Les auteurs développent un cadre théorique rigoureux pour combler le fossé entre la théorie des valeurs réelles et la pratique de la virgule flottante.

2.1 Formalisation de la sémantique de la virgule flottante

L'article définit les réseaux de neurones comme des fonctions sur l'ensemble des nombres à virgule flottante finis $\mathcal{F}$, utilisant des opérations conformes à la norme IEEE-754 ($\oplus, \ominus, \otimes$) avec le mode de « l'arrondi au plus proche (liens vers l'pair) ». La sémantique d'intervalle $\nu^\sharp$ est définie sur des intervalles abstraits $\langle a, b \rangle$, représentant l'ensemble des flottants dans $[a, b]$.

2.2 Conditions sur les fonctions d'activation

Pour prouver le théorème, les auteurs introduisent la Condition 1, un ensemble de contraintes sur la fonction d'activation $\sigma: \mathcal{F} \to \mathcal{F}$. Ces conditions garantissent que la fonction peut :

1. Produire un zéro exact et une valeur non nulle spécifique dans une plage bornée.
2. Présenter une monotonie ou un comportement de seuillage spécifique autour d'une valeur critique $\eta$.
3. Satisfaire une contrainte de continuité de type Lipschitz pour empêcher une croissance non bornée.

L'article démontre que les versions correctement arrondies des fonctions d'activation courantes (ReLU, GELU, Sigmoïde, Tanh, etc.) satisfont ces conditions, souvent en exploitant le Lemme 1, qui fait correspondre les propriétés des fonctions à valeurs réelles à leurs équivalents en virgule flottante.

2.3 Stratégie de preuve : Séparabilité et construction d'indicateurs

Le cœur de la preuve implique la construction d'un réseau de neurones agissant comme un « approximateur d'intervalles universel ». La méthodologie procède en deux étapes principales :

1. Séparabilité : Les auteurs définissent une propriété appelée $([a, b]_\mathcal{F}, \eta, K, L_\phi, L_\psi)$-séparabilité. Cette propriété garantit l'existence de réseaux capables d'implémenter des fonctions indicatrices scalées (par exemple, cartographier les entrées $\le z$ vers 0 et les entrées $> z$ vers $K$) sous la sémantique d'intervalle.

   • La preuve construit des sous-réseaux spécifiques (par exemple, $\mu_z$, $\tau_{\theta, \theta'}$) qui exploitent les erreurs d'arrondi pour « contracter » les intervalles. Par exemple, un réseau est conçu de telle sorte que les entrées dans une plage spécifique soient mappées vers un intervalle singleton $\langle \eta, \eta \rangle$ ou $\langle \eta^+, \eta^+ \rangle$ après le passage par la fonction d'activation.
   • Crucialement, la construction évite les valeurs infinies dans les couches intermédiaires, traitant ainsi les problèmes de dépassement de capacité qui affectent les preuves sur les réels lors de la mise à l'échelle des poids vers des magnitudes arbitraires.

2. Composition pour l'approximation universelle : En utilisant la propriété de séparabilité, les auteurs construisent des réseaux pour :

   • Les fonctions indicatrices de boîtes arbitraires.
   • Les fonctions indicatrices de sous-ensembles arbitraires de l'espace d'entrée.
   • Enfin, la fonction cible elle-même, en l'exprimant comme une combinaison linéaire en virgule flottante de ces fonctions indicatrices. La preuve gère soigneusement la sommation en virgule flottante pour s'assurer que les erreurs d'arrondi accumulées s'alignent parfaitement pour reconstruire la carte d'image de la fonction cible.

3. Contributions clés

3.1 Le théorème IUA de la virgule flottante (Théorème 1)

L'article prouve que pour toute fonction cible $f: \mathbb{R}^d \to \mathbb{R}$ et une large classe de fonctions d'activation satisfaisant la Condition 1, il existe un réseau de neurones à virgule flottante $\nu$ tel que sa sémantique d'intervalle $\nu^\sharp$ calcule exactement l'application d'image directe de la fonction cible arrondie $\hat{f}$ sur le domaine $[-1, 1]^d \cap \mathcal{F}^d$.

• Exactitude : Contrairement à l'IUA sur les réels qui atteint une $\delta$-approximation, la version virgule flottante atteint $\delta = 0$ (correspondance exacte) car le domaine est fini.
• Généralité : Le théorème est valable pour des fonctions cibles arbitraires (pas seulement continues) et une large gamme de fonctions d'activation, y compris la fonction identité (ce qui est impossible dans l'IUA sur les réels).

3.2 Existence de réseaux prouvablement robustes (Théorème 2)

En tant que corollaire, l'article prouve que si un classificateur robuste idéal existe (même s'il ne s'agit pas d'un réseau de neurones), il existe un réseau de neurones à virgule flottante qui est prouvablement robuste via l'analyse d'intervalles et qui produit des prédictions identiques. Cela résout la question de savoir s'il existe des limites fondamentales sur l'expressivité des réseaux prouvables robustes dans le cadre de la virgule flottante : ces limites n'existent pas.

3.3 Complétude d'intervalle de la virgule flottante (Théorème 3)

L'article établit un résultat surprenant concernant la complétude computationnelle : la classe des programmes à virgule flottante à lignes droites utilisant uniquement l'addition ($\oplus$) et la multiplication ($\otimes$) est complète pour les intervalles de virgule flottante. Cela signifie que de tels programmes simples peuvent simuler la sémantique d'intervalle de n'importe quel programme à virgule flottante terminant qui prend des flottants finis en entrée et retourne des flottants finis ou infinis. Ce résultat étend le théorème IUA à la fonction d'activation identité sur l'ensemble du domaine $\mathcal{F}^d$.

4. Résultats et comparaisons

L'article souligne trois distinctions fondamentales entre le nouvel IUA de la virgule flottante et les résultats précédents sur les réels :

1. Fonctions cibles : L'IUA sur les réels approxime des fonctions continues ; l'IUA sur virgule flottante calcule exactement l'image de n'importe quelle fonction cible arrondie (puisque le domaine est fini).
2. Fonctions d'activation : L'IUA sur les réels nécessite des activations « écrasables » (non affines) ; l'IUA sur virgule flottante est valable même pour la fonction identité. Cela est dû au fait que les transformations affines en virgule flottante ne sont pas strictement affines sur les réels en raison des erreurs d'arrondi, ce qui leur permet de briser la linéarité et d'approximer des comportements non linéaires.
3. Approximation vs Exactitude : Les résultats sur les réels fournissent des $\delta$-approximations ; les résultats sur virgule flottante fournissent des correspondances exactes pour la cible arrondie.

5. Signification et revendications

Les auteurs affirment que ce travail comble le fossé théorique entre la vérification de la robustesse basée sur l'interprétation abstraite et les implémentations pratiques en virgule flottante.

• Assurance théorique : Il démontre que l'absence de précision de pointe dans les réseaux robustes n'est pas due à une limitation fondamentale de leur puissance d'expression, mais probablement à des défis d'optimisation ou aux algorithmes de vérification spécifiques utilisés.
• Complétude : Le résultat de complétude d'intervalle suggère que des opérations arithmétiques simples sont suffisantes pour simuler des comportements complexes de virgule flottante, offrant de nouvelles perspectives sur la puissance de calcul des programmes en virgule flottante.
• Pertinence pratique : En validant le théorème IUA pour les nombres à virgule flottante, l'article fournit un fondement théorique à l'utilisation de l'analyse d'intervalles dans les domaines critiques pour la sécurité (santé, conduite autonome), où l'arithmétique à virgule flottante est la norme.

L'article précise explicitement qu'il s'agit de preuves d'existence ; il ne prétend pas que les algorithmes d'entraînement actuels peuvent facilement trouver de tels réseaux, ni qu'il propose de nouvelles méthodes d'entraînement. La contribution est strictement théorique, établissant que le « plafond d'expressivité » pour les réseaux de neurones à virgule flottante prouvables est effectivement inexistant.