Propriétés quantifiées d'atteignabilité pour l'explicabilité garantie en IA // Quantified reachability properties for provably explainable AI

L'intelligence artificielle est désormais intégrée à de nombreuses applications de la vie quotidienne. Nous dépendons de plus en plus des réseaux de neurones même dans des situations critiques, comme le contrôle et la planification des mouvements des voitures autonomes, et il est primordial de pouvoir vérifier leur bon comportement.
La vérification par abstraction de la sureté de réseaux de neurones a récemment reçu une attention considérable, avec en particulier l'analyse d'accessibilité des réseaux de neurones par des 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 pour aborder des propriétés de robustesse plus générales. Plus spécifiquement, l'objectif est de proposer des approches garanties pour l'explicabilité du comportement des réseaux de neurones, tandis que la plupart des techniques existantes sont heuristiques [8].

Objectifs : Les approximations intérieures et extérieures de l'image ensembliste 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]. Ceux-ci constituent une base à partir de laquelle l'étudiant doit concevoir de nouvelles méthodes basées sur des ensembles pour aborder les propriétés des réseaux de neurones qui peuvent être exprimées sous forme de problèmes d'accessibilité quantifiés. 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 le sens par ex. [6, 2, 7]. Un autre axe consiste à fournir 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 à elles seules la classification produite par le DNN. On peut également imaginer utiliser de telles approches pour guider la sparsification des réseaux de neurones.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Artificial Intelligence is now embedded into a number of everyday life appli- cations. More and more, we depend on neural networks even in critical situations, such as control and motion planning for autonomous cars, and it is of primary importance to be able to verify their correct behavior.
Abstraction-based safety verification for neural networks has received considerable attention recently, with in particular reachability analysis of neural networks using polyhedric abstractions such as [9, 10], with application in particular to local robustness analysis. The context of this work is to develop sound abstractions for addressing more general robustness properties. More specifically, the objective is to propose provably correct explanations of neural networks behavior while most existing techniques are heuristic [8].

Objectives: The tractable inner and outer-approximations of ranges of functions proposed in [3] are a building block for proving very general quantified reachability problems [4]. These constitute a basis from which the student is expected to design new set-based methods to tackle properties of neural networks that can be expressed as quantified reachability problems. The objectives are to identify some properties of interest that can be expressed in this framework, and design and experiment reachability analyzes inspired from the techniques of [3, 4] to rigorously assess these properties. As a starting point, we can explore fairness properties, in the line of e.g. [6, 2, 7]. Another axis consists in providing rigorous explainability properties of neural networks such as abductive explanation [5, 1]: a minimum subset of input features, which by themselves determine the classification produced by the DNN. We can also imagine using such approaches to guide the sparsification of neural networks.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Other public funding

ANR Financement d'Agences de financement de la recherche*

École polytechnique

626 Ecole Doctorale de l'Institut Polytechnique de Paris

Les candidats doivent avoir une solide expérience en informatique, avec un accent sur les méthodes formelles et un intérêt pour l'intelligence artificielle.
Candidates should have a strong background in computer science with a focus on formal methods and interest for artificial intelligence.