Description du 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 under-approximations and application to reachability of non-linear control systems with disturbances. IEEE Control Systems Letters, 4(4):928–933, 2020.
[4] Eric Goubault and Sylvie Putot. Inner and outer approximate quantifier elimination for general reachability problems. In Proceedings of the 27th ACM International Conference on Hybrid Sys- tems: Computation and Control, HSCC ’24, New York, NY, USA, 2024. Association for Computing Machinery.
[5] Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. Abduction-based explanations for ma- chine learning models. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Sym- posium on Educational Advances in Artificial Intelligence, AAAI’19/IAAI’19/EAAI’19. AAAI Press, 2019.
[6] Haitham Khedr and Yasser Shoukry. Certifair: A framework for certified global fairness of neural networks, 2022.
[7] Brian Hyeongseok Kim, Jingbo Wang, and Chao Wang. Fairquant: Certifying and quantifying fairness of deep neural networks, 2024.
[8] Rabia Saleem, Bo Yuan, Fatih Kurugollu, Ashiq Anjum, and Lu Liu. Explaining deep neural net- works: A survey on the global interpretation methods. Neurocomputing, 513:165–180, 2022.
[9] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS’18, page 10825–10836, Red Hook, NY, USA, 2018. Curran Associates Inc.
[10] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(POPL), January 2019.

Contexte de travail

Le LIX (Laboratoire d'Informatique de l'Ecole Polytechnique) est une unité mixte de recherche avec deux établissements de tutelle, l'École Polytechnique, membre de l'Institut Polytechnique de Paris (pôle d'universités composé de l'Ecole Polytechnique, Télécom Paris, ENSTA Paris, Télécom Sud Paris, ENSAE), et le Centre National de la Recherche Scientifique (CNRS), et un partenaire, Inria Saclay, avec des bâtiments partagés et des équipes mixtes.

Le LIX est organisé en quatre pôles : « Mathématiques informatiques », « Analyse de données et apprentissage automatique », « Communications efficaces et sécurisées », « Modélisation, simulation et apprentissage » et « Preuves et algorithmes ». Le doctorat. L'étudiant fera partie de l'équipe Cosynus dans le pôle « Preuves et Algorithmes ». Les membres de l'équipe Cosynus travaillent sur la sémantique et l'analyse statique des systèmes logiciels, séquentiels, concurrents ou distribués, hybrides/contrôle et des systèmes cyber-physiques.

Le doctorant bénéficiera de l'environnement passionnant du LIX, notamment du Département d'Informatique de l'Ecole Polytechnique (DIX), dans lequel il pourra donner des cours, et du Département d'Informatique, de Données et d'Intelligence Artificielle de l'Institut Polytechnique de Paris. (IDIA). Il ou elle interagira également avec les membres du projet SAIF (Safe Artificial Intelligence through Formal Methods), du Programme National de Recherche sur l'Intelligence Artificielle PEPR IA.

Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.

Contraintes et risques

Pas de contrainte ni risque particulier, ceux inhérents à un travail de recherche.
Début de thèse prévu au 1er octobre 2025 mais possible à partir de janvier 2025