Doctorant H/F en Atteignabilité de propriétés quantifiées pour l'explicabilité de l'intelligence artifi

Sujet de thèse :
L’IA est désormais intégrée à un certain nombre d’applications de la vie quotidienne. De plus en plus, nous dépendons des réseaux de neurones pour effectuer même des tâches critiques, comme le contrôle et la planification de déplacement des voitures autonomes, et il est primordial de pouvoir vérifier leur comportement correct.

La vérification de la sécurité basée sur l'abstraction pour les réseaux neuronaux a récemment reçu une attention considérable, avec en particulier l'analyse de l'accessibilité des réseaux neuronaux à l'aide d'abstractions polyédriques telles que [9, 10], avec une application en particulier à l'analyse de robustesse locale. Le contexte de ce travail est de développer des abstractions garanties pour aborder des propriétés de robustesse plus générales. Plus spécifiquement, l'objectif est de proposer des explications prouvables du comportement des réseaux neuronaux alors que la plupart des techniques existantes sont heuristiques [8].

Les approximations internes et externes des plages de fonctions proposées dans [3] sont un élément de base pour prouver des problèmes d'accessibilité quantifiés très généraux [4]. Elles constituent une base à partir de laquelle le doctorant concevra de nouvelles méthodes ensemblistes pour aborder les propriétés des réseaux de neurones qui peuvent être exprimées sous forme de problèmes quantifiés d'accessibilité. Les objectifs sont d'identifier certaines propriétés d'intérêt qui peuvent être exprimées dans ce cadre, et de concevoir et d'expérimenter des analyses d'accessibilité inspirées des techniques de [3, 4] pour évaluer rigoureusement ces propriétés. Comme point de départ, nous pouvons explorer les propriétés d'équité, dans la lignée de [6, 2, 7]. Un autre axe consiste à s’intéresser à des propriétés d'explicabilité rigoureuses des réseaux de neurones telles que l'explication abductive [5, 1] ​​: un sous-ensemble minimum de caractéristiques d'entrée, qui déterminent par elles-mêmes la classification produite par le DNN. Nous envisageons également d'utiliser de telles approches pour guider les approches de production de réseaux de neurones de petite dimension à qualité prouvée, dans le but de produire des algorithmes frugaux d’intelligence artificielle.

[1] Shahaf Bassan and Guy Katz. Towards formal xai: Formally approximate minimal explanations of neural networks. In Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I, page 187–207, Berlin, Heidelberg, 2023. Springer-Verlag.
[2] Sumon Biswas and Hridesh Rajan. Fairify: Fairness verification of neural networks. In Proceedings of the 45th International Conference on Software Engineering, ICSE ’23, page 1546–1558. IEEE Press, 2023.
[3] Eric Goubault and Sylvie Putot. Robust
Voir plus sur le site emploi.cnrs.fr...