Sur-approximation de réseaux de neurones : applications à la vérification, la robustesse et les explications de réseaux de neurones

Depuis le début des années 2010, le succès de l'apprentissage profond a conduit à son adoption dans un large éventail d'applications, allant de la classification d'images au traitement du langage naturel. Cependant, le déploiement de modèles d'IA — en particulier dans des systèmes critiques — nécessite à la fois de fortes garanties et des moyens de comprendre et d'expliquer leurs prédictions. La robustesse — la capacité d'un modèle à maintenir ses performances face à de petites perturbations de ses entrées — constitue un prérequis important en matière de sécurité et contribue à l'explicabilité formelle des prédictions du modèle.Les techniques de sur-approximation, introduites par les communautés de l'apprentissage automatique et des méthodes formelles, se sont imposées comme un outil clé pour vérifier les réseaux de neurones et les entraîner avec des objectifs de robustesse prouvable. En bornant l'ensemble des sorties possibles d'un réseau, elles permettent de prouver certaines propriétés souhaitées pour toutes les entrées appartenant à un domaine donné. Dans cette thèse, nous étudions dans quelle mesure ces sur-approximations peuvent être utilisées de manière efficace pour améliorer la vérification, l'apprentissage et l'explicabilité formelle des réseaux de neurones.De telles sur-approximations sont essentielles pour rendre possible l'analyse de réseaux de neurones de taille réaliste, mais elles ont également tendance à être imprécises, en particulier pour des réseaux entraînés sans objectif explicite de robustesse. Dans une première contribution, nous exploitons des informations clés issues des sur-approximations pour affiner efficacement les bornes lors de la vérification de réseaux avec des espaces d'entrée de faible dimension. Cette technique est implémentée dans PyRAT, un outil de vérification de réseaux de neurones, et a contribué à ses bons résultats dans la dernière édition de la compétition internationale de vérification de réseaux de neurones (VNN-COMP 2024).Une seconde contribution montre que l'entraînement certifié — qui utilise des sur-approximations pour minimiser une borne de la fonction de coût dans le pire cas — peut être combiné à l'entraînement adversarial — qui calcule la fonction de coût sur des échantillons d'entraînement perturbés — afin d'améliorer la robustesse empirique et de prévenir le catastrophic overfitting, un mode d'échec de l'entraînement adversarial, dans certains contextes expérimentaux.Enfin, nous proposons d'utiliser les sur-approximations pour entraîner des modèles en vue d'une explicabilité formelle. Afin d'éviter le cas trivial où la robustesse rend toute explication vide, nous introduisons le Feature Subset Certified Training, un nouveau mode d'entraînement qui impose la robustesse uniquement sur certains sous-ensembles des features des échantillons, un premier pas vers de meilleurs compromis entre précision et concision des explications formelles.Dans l'ensemble, ces contributions illustrent comment les sur-approximations peuvent être mises à profit pour améliorer la robustesse et l'explicabilité, soutenant ainsi le développement de systèmes d'IA plus sûrs et plus dignes de confiance.