Spécification formelle et validation des systèmes basés sur la perception

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. École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris Direction : Sergio MOVER Financement : Financement d'une fondation pour la recherche française