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. 

…

Télécharger l’article complet :

Sur le même sujet :

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

Notre offre IA à Kereval :

• Ingénierie du test de l’IA