Motivations 

L’Intelligence Artificielle (IA) est aujourd’hui très présente dans de nombreux services que nous utilisons et tend à l’être de plus en plus, notamment dans les systèmes critiques tels que la conduite autonome, l’aviation ou l’imagerie médicale. Parallèlement à cet essor, il a été découvert ces dernières années, que ces systèmes basés IA sont sensibles à certaines perturbations dans les entrées ou dans les modèles. Cette faiblesse pose un problème précisément pour les systèmes critiques. Effectivement, une voiture autonome ne détectant pas un piéton à cause d’une perturbation n’est pas envisageable. Il s’agit donc de tester les modèles utilisant l’IA. 

Les techniques de test sont très répandues dans le monde du génie logiciel mais ne sont pas directement applicables à l’IA. Effectivement, dans les logiciels qui n’en utilisent pas, le programmeur spécifie tout le processus qui suit une certaine logique. À contrario, dans les systèmes basés IA, il décrit un comportement souhaité pour le système mais la logique est définie par le modèle entraîné à partir de données, comme dans la figure suivante. 

Pour répondre à cette demande de test, on distingue deux types de techniques : d’une part les méthodes de test qui cherchent à mettre en évidence les défauts du système vis-à-vis d’un ensemble de cas (e.g., scénarios d’utilisation), et les méthodes formelles qui utilisent la logique et les mathématiques pour prouver certaines propriétés du système et garantir l’absence de défauts. 

Dans ce projet, nous avons étudié la vérification formelle pour les réseaux de neurones de classification d’images. 

Fonctionnement 

La classification d’images consiste à prendre une image en entrée et à la classer dans une des catégories définies préalablement. Les réseaux de neurones les plus utilisés pour la classification d’images sont les réseaux convolutifs qui combinent des couches de convolution, de pooling et de neurones fully-connected. En sortie, le nombre de neurones correspond au nombre de classes possibles et le système retourne la classe avec la probabilité la plus élevée comme dans l’exemple suivant : 

Le test d’un tel système peut être abordé sous l’angle de la robustesse, en utilisant des images perturbées en entrée. Une première idée serait de modifier manuellement les images et vérifier si le réseau prédit le même résultat. Néanmoins, cela serait bien trop long car une infinité de types et niveaux de perturbations sont possibles. L’avantage de la vérification formelle est qu’elle permet de garantir la robustesse d’un modèle pour un ensemble de niveaux de perturbations. Une perturbation, en pratique, correspond à une diminution ou augmentation des valeurs des pixels de l’image qui est en entrée du réseau.  

Méthodes 

> Interprétation abstraite 

Une méthode de vérification formelle est l’interprétation abstraite. Elle consiste à borner les valeurs des neurones par l’utilisation de transformateurs abstraits qui permettent de propager la perturbation appliquée en entrée du réseau. Cette méthode permet d’obtenir en sortie, des bornes autour de chaque probabilité de classe et considérer notre IA robuste pour une image si la borne de la vraie classe est séparée des autres. Ce processus est illustré dans le schéma suivant. 

> Approximation linéaire 

Une autre méthode est l’approximation linéaire. Elle ressemble fortement à l’interprétation abstraite, mais elle utilise des bornes linéaires autour des valeurs des neurones au lieu de transformateurs abstraits (cf. figure ci-dessous).  

En application, l’interprétation abstraite et l’approximation linéaire ont des résultats généralement similaires. 

> Branch-and-Bound 

Une autre méthode est le Branch-and-Bound (BaB), qui consiste à combiner, comme son nom l’indique, une partie de bornage, et une autre de découpage en sous-problèmes. Un sous-domaine est « vérifié » si sa borne inférieure est supérieure à 0. La procédure de BaB se termine lorsque tous les sous-domaines sont vérifiés ou que le temps imparti est écoulé. Si tous les sous-domaines sont vérifiés, le modèle est garanti robuste face à la perturbation énoncée précédemment pour l’image utilisée. Le BaB peut s’utiliser en complément de l’interprétation abstraite et de l’approximation linéaire afin d’affiner la vérification.  

Cas d’étude  

Trois déclinaisons de ces méthodes sont :

• DeepZono qui utilise l’interprétation abstraite seule,
• Mn-BaB qui utilise l’interprétation abstraite couplée avec du BaB,
• et Alpha-Beta-CROWN qui utilise l’approximation linéaire couplée avec du BaB. 

Celles-ci ont été utilisées sur le jeu de données CIFAR10, qui comprend environ 60 000 images réparties en 10 classes : avion, voiture, oiseau, chat, cerf, chien, grenouille, cheval, bateau, camion. Le modèle utilisé est un réseau de neurones convolutif (4 couches de convolution sans pooling et 2 couches linéaires) de classification d’images entrainé de quatre manières : 

• Classique ; 
• Sur des exemples antagonistes générés par FGSM 
• Sur des exemples antagonistes générés par PGD 
• Par une méthode d’entrainement pour la robustesse Crown-IBP

Des exemples antagonistes sont des données perturbées dans l’objectif de tromper un modèle IA. De nombreuses autres méthodes pour les générer existent dans la littérature. 

Résultats  

Le niveau de robustesse correspond au ratio entre le nombre d’images pour lesquelles le modèle est certifié robuste par rapport au nombre d’images bien classées par le modèle. Ainsi, un niveau de robustesse de 1 représente le cas où le modèle est certifié robuste pour toutes les images bien classées par ce dernier. Un niveau de robustesse de 0 représente le cas où le modèle est certifié robuste pour aucune image bien classée par ce dernier. 

Les résultats diffèrent entre les modèles et également entre les méthodes. L’application Alpha-Beta-CROWN est plus précise que les autres et parvient à garantir la robustesse des modèles sur davantage d’images que les autres applications. Également, le modèle entrainé sur Crown-IBP est plus robuste que les autres, pour les perturbations utilisées dans ces applications. Le modèle entrainé classiquement est très sensible aux perturbations appliquées.  

Quelle utilisation ? 

Ces travaux sur CIFAR10 et un autre jeu de données d’images de taille plus élevée, Imagenette, ont révélé la complexité d’utilisation actuelle des méthodes formelles pour des cas concrets. En effet, plusieurs difficultés sont rencontrées : 

1. Taille des réseaux de neurones : plus le réseau est grand, plus la précision est faible, le temps de calcul est élevé et la quantité de mémoire utilisée est importante. Ce qui peut poser des problèmes car, dans le monde industriel, les réseaux utilisés sont de tailles bien plus importantes que ceux de cette étude. 

2. Certaines couches ne sont pas toujours supportées (Pooling, BatchNormalisation), or ce sont des couches largement utilisées en pratique. 

3. Peu de types de perturbations sont supportées (𝐿∞L∞, rotation géométrique), or en pratique, il est nécessaire de garantir la robustesse face à des perturbations plus variées). 

4. Ces méthodes ne sont, pour l’heure, pas utilisables sur des systèmes de détection ou de segmentation d’objets, largement utilisés dans des systèmes tels que la voiture autonome. 

Par rapport aux perturbations applicables, seules celles présentées dans le graphique suivant sont réalisables. 

Quel avenir ? 

La recherche en vérification formelle appliquée aux modèles IA est récente et florissante. Ces méthodes qui, pour l’instant, ne sont pas applicables aux systèmes industriels, pourraient dans un futur proche permettre d’apporter des garanties de robustesse pour les modèles IA et améliorer la confiance de l’humain envers eux. Ces travaux viennent renforcer la vision d’ensemble du test de l’Intelligence Artificielle chez Kereval.  

Sur le même sujet :

• Article sur l’explicabilité du test de l’IA
• Webinar « Comment tester une IA » – La taverne du testeur