Exécution symbolique pour les réseaux de neurones

Pour évaluer la confiance que l'on peut avoir dans un réseau de neurones, l'un des enjeux est de comprendre comment le réseau classifie les données. La taille des réseaux de neurones utilisés industriellement, en termes de nombre de chemins d'exécutions, mais aussi en terme de nombre de paramètres manipulées, est telle qu'une analyse humaine n'est pas possible. Il faut donc automatiser cette analyse et parmi les approches récemment explorées dans l'état de l'art, on trouve des techniques basées sur l'exécution symbolique. Cette approche reposant sur l'exploration des différents chemins d'exécutions d'un programme permet, d'effectuer des couvertures structurelles, de mettre en ?uvre des heuristiques dédiées à l'atteignabilité de partie du programme ou à la vérification de propriétés, et de générer des cas de test pour ces objectifs. Cette thèse a pour objet de proposer des adaptations des techniques existantes d'exécution symboliques pour les appliquer à la vérification des réseaux de neurones qui proposent de nouveaux défis en terme d'exploration de programme, afin d'y révéler et analyser les comportements indésirables après les avoir caractérisés.