Doctorant en Vérification de Propriétés Probabilistes pour l'Intelligence Artificielle H/F CNRS

Détail du poste

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.
Pour certaines applications, comme la perception dans les systèmes autonomes, on ne peut qu'espérer une sécurité probabiliste grâce aux classificateurs. De plus, dans les systèmes réels, des modèles précis et représentatifs des données ne sont pas toujours disponibles. Par exemple, plusieurs modèles probabilistes peuvent être plausibles pour décrire un problème, ou un modèle probabiliste peut être connu mais avec des paramètres incertains. Par conséquent, nous devons considérer à la fois les informations probabilistes et l'incertitude épistémique. Récemment a été introduite dans [1] une approche basée sur des probabilités imprécises ou p-boxes, qui généralisent les incertitudes probabilistes et épistémiques en définissant des ensembles de distributions de probabilité, pour la vérification quantitative des réseaux de neurones. Cette approche fournit des mesures qualitatives de la probabilité que les sorties d'un réseau neuronal présentent un certain comportement, compte tenu de certaines hypothèses sur les entrées spécifiées comme probabilités imprécises. Sur la base d'une abstraction et d'une propagation d'ensembles de distributions de probabilité dans des réseaux neuronaux, la probabilité d'une satisfaction de propriété peut être limitée et les régions de l'espace d'entrée les plus susceptibles de conduire à une violation de propriété peuvent être identifiées.
L'approche de [1] s'est avérée à la fois plus générale et plus efficace en terme de calcul que l'état de l'art. Cependant, de nombreux défis restent à relever quant à l'applicabilité à des problèmes du monde réel. Comme point de départ du problème, les extensions suivantes peuvent être étudiées :
- L'abstraction actuelle des p-boxes repose sur une discrétisation en escalier à pas constant qui s'adaptera difficilement à la dimension d'entrée des réseaux ; nous aimerions explorer d'autres abstractions ;
- L'indépendance est actuellement supposée entre les entrées du réseau ; nous aimerions également gérer les distributions d'entrées multivariées, par exemple en utilisant des copules [4] comme par ex. [2].
Un objectif à plus long terme est d'étudier l'extension de l'approche à l'analyse des réseaux de neurones bayésiens, où les poids et les biais du réseau sont également définis par des distributions de probabilité multivariées (imprécises). Cela étend le cas des distributions d'entrées multivariées, mais dans une dimension beaucoup plus élevée, nécessitant probablement une nouvelle vision de l'approche. Enfin, le projet étudiera l'application à l'un ou aux deux des éléments suivants :
- Application à la sécurité des systèmes autonomes, comme la robustesse de perception et de décision dans la vision de drones avec des informations probabilistes imprécises sur les trajectoires ;
- Contribution à l'analyse d'équité et plus généralement à l'explicabilité du comportement du réseau [3].
[1] Eric Goubault and Sylvie Putot. A zonotopic Dempster-Shafer approach to the quantitative verification of neural networks. In Formal Methods : 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, page 324-342, Berlin, Heidelberg, 2024. Springer-Verlag.
[2] Ander Gray, Marcelo Forets, Christian Schilling, Scott Ferson, and Luis Benet. Verified propagation of imprecise probabilities in non-linear odes. International Journal of Approximate Reasoning, 164, 2024.
[3] Rabia Saleem, BO Yuan, Fatih Kurugollu, Ashiq Anjum, and Lu Liu. Explaining deep neural networks : A survey on the global interpretation methods. Neurocomputing, 513 :165-180, 2022.
[4] Bernhard Schmelzer. Random sets, copulas and related sets of probability measures. International Journal of Approximate Reasoning, 160 :108952, 2023.
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, éventuellement possible plus tôt (financement disponible)