Sélection de ReLU locale versus globale : la MILP partielle fait son retour pour la vérification des réseaux de neurones profonds

Pour traiter les instances complexes, nous revisitons une approche par division et conquête afin de réduire la complexité : au lieu de quelques appels coûteux à BaB (Branch-and-Bound), nous nous appuyons sur un grand nombre d'appels partiels à des problèmes MILP (Mixed-Integer Linear Programming) de petite taille. L'étape cruciale consiste à sélectionner un très petit nombre, mais très important, de neurones ReLU à traiter à l’aide de variables binaires (coûteuses). Les tentatives précédentes se sont révélées sous-optimales à cet égard. Pour sélectionner ces variables ReLU pertinentes, nous proposons une nouvelle méthode de notation des neurones ReLU, appelée solution-aware ReLU scoring (SAS), ainsi que l’adaptation des fonctions de branchement BaB-SR et BaB-FSB en fonctions de notation globale des ReLU (GS). Nous comparons ces approches théoriquement comme expérimentalement, et montrons que SAS est plus efficace pour sélectionner un ensemble de variables à ouvrir via des variables binaires. Par rapport aux approches antérieures, SAS permet de réduire le nombre de variables binaires d’environ six fois, tout en maintenant le même niveau de précision. Implémentée dans le cadre de Hybrid MILP, en appelant d’abord α,β-CROWN avec un délai court afin de traiter les instances plus simples, puis en passant aux appels partiels MILP, cette méthode produit un vérificateur à la fois très précis et efficace : elle réduit jusqu’à 40 % le nombre d’instances indécidées, les ramenant à des niveaux très faibles (8 à 15 %), tout en maintenant un temps d’exécution raisonnable (entre 46 et 417 secondes en moyenne par instance), même pour des réseaux de neurones convolutifs relativement grands comportant jusqu’à 2 millions de paramètres.