Le 23 mai dernier, Fateh BOUDARDARA a soutenu sa thèse de doctorat de l’Université Gustave Eiffel intitulée « Contributions à la Vérification et au Monitoring des Systèmes de Réseaux de Neurones ».
Cette thèse s’est déroulée au sein de l’IRT RAILENIUM en partenariat avec le laboratoire ESTAS de l’Université Gustave Eiffel sous la direction de Mohamed GHAZEL et Abderraouf BOUSSIF.
Résumé :
L’évaluation et la vérification des réseaux neuronaux (NN), lors de leur conception et de leur déploiement sécurisé, suscitent un vif intérêt de recherche, en particulier à la lumière d’études récentes mettant en évidence leur sensibilité et leur vulnérabilité face à diverses conditions opérationnelles telles que les attaques adverses et les variations environnementales. Bien que leur importance soit cruciale dans l’assurance de la précision et de la fiabilité des NN, les approches fondées sur les tests pour l’évaluation des NN sont entravées par plusieurs limitations qui peuvent compromettre leur efficacité. Afin de remédier à ces limites, des travaux de recherche explorent la vérification formelle comme approche complémentaire pour vérifier la fiabilité et la sécurité des NN. Si les tests peuvent démontrer la capacité d’un système à maintenir ses performances dans des conditions variables, démontrer cela nécessite une analyse formelle approfondie. La vérification des NN vise ainsi à fournir des garanties formelles quant au comportement et aux propriétés des NN. Cela implique une analyse minutieuse des entrées, des sorties et des calculs internes du modèle pour s’assurer que le réseau se comporte correctement vis-à-vis des spécifications requises. Alors que la vérification des NN est, d’une manière générale, effectuée lors de la conception des systèmes, le monitoring des NN, quant à lui, est cruciale pour garantir l’exécution du bon comportement lors de la phase opérationnelle. Pour ce faire, un système de monitoring fonctionne en parallèle du NN, détectant toute anomalie ou comportement inattendu et déclenchant des alertes en cas de besoin. Bien que des succès aient été rencontrés dans certaines applications, la vérification et le monitoring des NN restent des défis, notamment lorsqu’il s’agit de NN complexes ou de taille importante. Cette difficulté découle en grande partie de la complexité et de la non-linéarité des modèles NN, ainsi que des limites des méthodes formelles existantes pour s’adapter à des modèles réels de grande taille.
Dans cette thèse, nous proposons deux contributions principales pour répondre aux deux défis susmentionnés. Concrètement, nous proposons des techniques d’abstraction des NN (réduction de modèle) à des fins de vérification, ainsi qu’une approche de monitoring des NN en temps réel spécifiquement conçu pour les tâches de classification d’images. Ces approches d’abstraction de NN visent à améliorer la scalabilité et l’efficacité de la vérification des NN. En se basant sur des formulations mathématiques, nous garantissons que les modèles abstraits résultants conservent les propriétés essentielles (e.g., la sur-approximation) des réseaux d’origine, assurant ainsi la validité des résultats de vérification. Pour la partie monitoring, nous développons un système de surveillance qui identifie et évalue en temps réel les décisions de classification des réseaux par rapport à des modèles de référence spécifiques (motives de surveillance). Enfin, nous validons nos approches à travers des expérimentations menées sur des benchmarks académiques, ainsi qu’un cas d’étude spécifique au domaine ferroviaire.
Nous félicitons chaleureusement Fateh et lui souhaitons le meilleur pour la suite de sa carrière professionnelle.