Offre de thèse : Spécification formelle et validation des systèmes basés sur la perception (H/F)

Sujet de thèse :
Les systèmes autonomes perçoivent leur environnement externe à l’aide de capteurs tels que des caméras et des lidars, et utilisent des algorithmes d’apprentissage automatique (par exemple, des réseaux de neurones) pour reconnaître des motifs et des objets. Ces systèmes ayant de nombreuses applications dans des domaines critiques pour la sécurité, où les comportements imprévus peuvent être graves, une question clé est de savoir comment faire confiance à un système basé sur la perception pour qu’il se comporte comme prévu.

Cependant, exprimer des exigences formelles pour ces systèmes est un défi, car les entrées des composants d’apprentissage sont riches et non structurées (par exemple, une séquence d’images).

Cette thèse visera à :
- explorer la problématique de la spécification d’exigences formelles pour les systèmes basés sur la perception à l’aide de logiques temporelles, en comblant le fossé entre les caractéristiques brutes et les spécifications dites "sémantiques" ;
- étudier des algorithmes de raisonnement automatique (par exemple, basés sur la vérification de modèles) pour valider automatiquement ces exigences ;
- étudier des algorithmes pour vérifier automatiquement des spécifications sémantiques sur des réseaux de neurones.

Une description complète de la thèse est disponible sur : http://sergiomover.eu/saif_phd.pdf.
Contexte :
Le LIX (Laboratoire d’Informatique de l’École Polytechnique) est une unité mixte de recherche placée sous la tutelle conjointe de deux institutions : l’École Polytechnique, membre de l’Institut Polytechnique de Paris (regroupement d’établissements comprenant l’École Polytechnique, Télécom Paris, ENSTA Paris, Télécom Sud Paris et ENSAE), et le Centre National de la Recherche Scientifique (CNRS). Il compte également un partenaire, Inria Saclay, avec lequel il partage des bâtiments et des équipes mixtes.

Le LIX est structuré en quatre pôles : « Mathématiques informatiques », « Analyse de données et apprentissage machine », « Communications efficaces et sûres », « Modélisation, simulation et apprentissage » et « Preuves et algorithmes ».

Le doctorant ou la doctorante intégrera l’équipe Cosynus, rattachée au pôle « Preuves et algorithmes ». Les membres de l’équipe Cosynus travaillent sur la sémantique et l’analyse statique des systèmes logiciels — qu’ils soient séquentiels, concurrents ou distribués — ainsi que sur les systèmes hybrides/de contrôle et les systèmes cyber-physiques.

Le doctorant ou la doctorante bénéficiera d’un environnement stimulant au sein du LIX, notamment du Département d’Informatique de l’École Polytechnique (DIX), où il ou elle pourra donner des cours, et du Département Informatique, Données et 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), dans le cadre du Programme national de recherche en intelligence artificielle PEPR IA.