Soutenance de thèse de Noémie COHEN

Vérification formelle des systèmes à haute dimension fondés sur l'apprentissage machine (ML)


Titre anglais : Formal verification of high-dimensional Machine Learning (ML) based systems
Ecole Doctorale : EDMITT - Ecole Doctorale Mathématiques, Informatique et Télécommunications de Toulouse
Spécialité : Informatique et Télécommunications
Etablissement : Institut Supérieur de l'Aéronautique et de l'Espace
Unité de recherche : ISAE-ONERA MOIS MOdélisation et Ingénierie des Systèmes
Direction de thèse : Claire PAGETTI- Xavier PUCEL - Mélanie DUCOFFE


Cette soutenance aura lieu mardi 07 juillet 2026 à 9h30
Adresse de la soutenance : ISAE-SUPAERO 10 avenue Marc Pélegrin 31400 Toulouse - salle Salle des thèses

devant le jury composé de :
Claire PAGETTI   Directrice de recherche   ONERA Toulouse   Directeur de thèse
Benedikt BOLLIG   Directeur de recherche   CNRS Île-de-France Gif-sur-Yvette   Rapporteur
Matthieu MARTEL   Professeur   Université de Perpignan Via Domitia   Rapporteur
Antoine  MINÉ   Professeur des universités   Sorbonne Université   Examinateur
Caterina  URBAN   Chargée de recherche   Inria de Paris   Examinateur
Arthur  CLAVIÈRE   Ingénieur de recherche   Collins Aerospace   Examinateur
Mélanie DUCOFFE   Ingénieure de recherche   Airbus Operations S.A.S   Co-directeur de thèse du monde socio-économique
Pierre-Loïc  GAROCHE   Professeur   ENAC   Examinateur


Résumé de la thèse en français :  

Cette thèse porte sur la vérification formelle pour garantir la robustesse de modèles de machine learning dédiés à la détection de pistes d'atterrissage. Dans un premier temps, les recherches se sont concentrées sur les perturbations plausibles liées au domaine opérationnel (ODD), menant au développement d'une méthodologie ainsi que d'un outil visant à démontrer la robustesse des modèles face aux transformations géométriques (rotation, translation, échelle, etc.). Cet outil utilise une optimisation Lipschitz et des relaxations linéaires pour encapsuler l'ensemble des images perturbées.

Par ailleurs, les garanties de robustesse, initialement appliquées à la classification, ont ensuite été étendues à la détection d'objets, un domaine jusqu'alors moins exploré. Une méthode de vérification a ainsi été mise au point en formalisant la métrique d'Intersection sur Union (Intersection over Union - IoU) pour des perturbations de luminosité, de bruit blanc et de contraste.

Enfin, les enjeux de certification (ED-324/ARP-6983, concept papers de l'EASA) appliqués au cas d'utilisation de la détection de piste, ont été définis.

 
Résumé de la thèse en anglais:  

This thesis focuses on formal verification to ensure the robustness of machine learning models dedicated to runway detection. Initially, the research concentrated on plausible perturbations related to the Operational Design Domain (ODD), leading to the development of a methodology and a tool aimed at demonstrating the robustness of the models against geometric transformations (rotation, translation, scaling, etc.). This tool uses Lipschitz optimization and linear relaxations to encapsulate the entire set of perturbed images.

Furthermore, the robustness guarantees, initially applied to classification, were subsequently extended to object detection, a domain that had previously been less explored. A verification method was thus developed by formalizing the Intersection over Union (IoU) metric for brightness, white noise, and contrast perturbations.

Finally, the certification challenges (ED-324/ARP-6983, EASA concept papers) for object detection models, applied to the runway detection use case, were defined.

Mots clés en français :Vérification formelle, Sûreté de fonctionnement, Solveur,
Mots clés en anglais :   Formal verification, Safety, Solvers,