Résumé technique : Bornes de Taylor hiérarchiques de bout en bout pour la vérification complète des réseaux de neurones

Énoncé du problème

L'article aborde le défi de l'analyse de l'accessibilité des réseaux de neurones, spécifiquement la tâche de calculer ou de borner étroitement l'ensemble des sorties réalisables par un réseau de neurones sur un domaine d'entrée donné. Ce problème est central pour certifier la sécurité et la robustesse des systèmes physiques intégrant l'apprentissage, tels que la conduite autonome et le diagnostic médical.

Bien que le calcul exact de l'ensemble accessible soit généralement intraitable pour les fonctions non convexes, les méthodes existantes reposent sur des surapproximations traitables. Les auteurs observent que les méthodes actuelles de l'état de l'art pour les réseaux lisses, deux fois différentiables (par exemple, ceux utilisant des activations tanh ou sigmoïde) exploitent généralement au maximum des informations d'ordre deux (gradients et Hessiens) mais échouent à exploiter systématiquement la lissité d'ordre supérieur (spécifiquement, la continuité lipschitzienne du Hessien) pour contrôler les erreurs d'approximation. L'objectif est de dériver des bornes supérieures plus serrées et prouvables sur la valeur maximale d'une fonction $f(x)$ sur un ensemble d'entrée borné $X$, formulé comme :
$$\max_{x \in X} f(x)$$
où $X$ est typiquement une boule $\ell_2$ ou $\ell_\infty$.

Méthodologie : Cadre HITAB

Les auteurs proposent HITAB (Bornes de Taylor hiérarchiques de bout en bout), un cadre de vérification qui construit une hiérarchie de bornes supérieures basées sur des informations locales d'ordre zéro, un et deux, augmentées par la constante de Lipschitz du Hessien ($L_{\nabla^2 f}$).

1. Hiérarchie des bornes de Taylor

Le cadre définit une séquence de majorants $\bar{f}$ qui bornent la fonction $f(x_c + \delta)$ autour d'un point nominal $x_c$ :

• Ordre zéro : Utilise la valeur de la fonction $f(x_c)$ et la constante de Lipschitz globale $L_f$. La borne est linéaire en la taille de la perturbation $\epsilon$.
• Ordre un : Intègre le gradient $\nabla f(x_c)$ et la constante de Lipschitz du gradient $L_{\nabla f}$. Cela produit une borne de reste quadratique.
• Ordre deux (Contribution principale) : Intègre le Hessien $\nabla^2 f(x_c)$ et la constante de Lipschitz du Hessien $L_{\nabla^2 f}$. Cela résulte en un modèle de Taylor d'ordre deux avec un terme de reste cubique certifié :
  $$f(x_c + \delta) \leq f(x_c) + \nabla f(x_c)^\top \delta + \frac{1}{2}\delta^\top \nabla^2 f(x_c) \delta + \frac{1}{6}L_{\nabla^2 f}\|\delta\|_2^3$$
  Contrairement aux bornes d'ordre inférieur, la maximisation de ce majorant d'ordre deux sur une boule euclidienne est généralement non convexe et intraitable. Les auteurs proposent une relaxation « Séparer et Borner » (Split-and-Bound) pour dériver une borne supérieure fermée et traitable computationnellement.

2. Estimation compositionnelle de la constante de Lipschitz du Hessien

Un obstacle technique critique est le calcul de $L_{\nabla^2 f}$ pour les réseaux de neurones profonds. Les auteurs développent une procédure de propagation couche par couche (Théorème 5) pour borner cette constante.

• Ils définissent une règle de composition récursive pour la constante de Lipschitz du Hessien des applications de couche $F^I(x) = \sigma(W^I x + b^I)$.
• La borne dépend des constantes de Lipschitz de la fonction d'activation $\sigma$ et de ses dérivées ($L_\sigma, L_{\sigma'}, L_{\sigma''}$), ainsi que des poids du réseau et des constantes de Lipschitz précédemment calculées des sorties de couche et de leurs gradients.
• Cela permet un calcul efficace et modulaire de $L_{\nabla^2 f}$ depuis la couche d'entrée jusqu'à la couche de sortie.

3. Intégration avec Branch-and-Bound (BaB)

Pour atteindre une vérification complète, les bornes HITAB sont intégrées dans un pipeline Branch-and-Bound (BaB).

• L'algorithme partitionne itérativement le domaine d'entrée.
• À chaque nœud, la borne hiérarchique $\bar{f}_m$ (le minimum des certificats d'ordre zéro, un et deux) est calculée.
• Le processus continue jusqu'à ce que l'écart entre les bornes supérieure et inférieure tombe en dessous d'une tolérance prescrite.
• Le cadre prend en charge les ensembles d'entrée contraints $\ell_2$ et $\ell_\infty$, avec des adaptations spécifiques pour les boîtes $\ell_\infty$ utilisant des relations de norme.

Contributions clés

1. Borne de Lipschitz du Hessien compositionnelle : Un algorithme novateur et efficace pour borner $L_{\nabla^2 f}$ dans les réseaux feedforward profonds en propageant les bornes de courbure couche par couche.
2. Modèle de Taylor d'ordre deux de bout en bout : Une borne supérieure locale certifiée avec un terme de reste cubique, utilisant la continuité lipschitzienne du Hessien.
3. Hiérarchie unifiée de bornes : Un cadre qui unifie les bornes d'ordre zéro, un et deux, fournissant des conditions précises (seuils sur la taille de perturbation $\epsilon$) selon lesquelles les approximations d'ordre supérieur produisent prouvablement des certificats plus serrés que ceux d'ordre inférieur.
4. Pipeline de vérification pratique : L'intégration de ces bornes dans un vérificateur BaB complet (Algorithme 1) pour les réseaux de neurones lisses.

Résultats expérimentaux

Les auteurs ont évalué HITAB sur un benchmark de contrôle de quadrotor 6D, où un contrôleur de réseau de neurones (entraîné pour imiter un contrôleur prédictif de modèle) pilote un système tout en évitant des obstacles. La tâche impliquait le calcul d'ensembles accessibles sur 10 pas de temps sous des perturbations d'état bornées en $\ell_\infty$.

• Comparaison : HITAB a été comparé à une approche de bornage local d'ordre un de l'état de l'art (Sharifi et Fazlyab, 2024).
• Performance :
  • HITAB a considérablement réduit le nombre de branches requises par l'algorithme BaB (par exemple, ~119k branches contre ~908k branches à une tolérance de $10^{-2}$).
  • Cette réduction s'est traduite par des temps d'exécution plus rapides (par exemple, ~108s contre ~320s à une tolérance de $10^{-2}$).
• Observation : Les informations d'ordre deux ont fourni des approximations locales plus serrées, en particulier sur les plus petits sous-domaines générés au cours du processus de branchement, conduisant à une convergence plus efficace.

Signification et affirmations

L'article prétend présenter le premier cadre pratique d'analyse d'accessibilité pour les réseaux de neurones lisses qui exploite systématiquement la continuité lipschitzienne de la courbure (Hessien).

• Certificats plus serrés : En allant au-delà des approximations d'ordre un (gradient) ou d'ordre deux standard (Hessien) pour inclure la lissité du Hessien, HITAB produit des certificats de sécurité plus serrés.
• Amélioration systématique : Le travail clarifie les régimes où l'information d'ordre supérieur est bénéfique, montrant que le terme de reste cubique permet une réduction significative du conservatisme dans les régions de petite perturbation.
• Complétude : Contrairement à de nombreuses méthodes existantes pour les réseaux lisses qui sont incomplètes (heuristiques), HITAB est conçu pour être intégré dans des pipelines de vérification complets, garantissant que le processus de vérification peut converger vers une réponse exacte étant donné un temps suffisant.

Les auteurs reconnaissent des limitations, notant que leur implémentation actuelle est basée sur CPU et que des relaxations numériques plus serrées pour le problème de maximisation d'ordre deux (au-delà de la forme fermée Séparer-et-Borner) restent une voie pour un travail futur. Cependant, ils affirment que l'approche en forme fermée actuelle offre un compromis favorable entre précision et coût computationnel.