Vers la certification des systèmes avioniques basés sur l'apprentissage automatique : exploitation des preuves mathématiques pour garantir la fiabilité
- Vidot, Guillaume (19..-....) (2022)
Thèse
- Titre en français
- Vers la certification des systèmes avioniques basés sur l'apprentissage automatique : exploitation des preuves mathématiques pour garantir la fiabilité
- Titre en anglais
- Towards the certification of machine learning-based avionic systems : leveraging mathematical proofs for ensuring trustworthiness
- Auteur
- Vidot, Guillaume (19..-....)
- Directeur de recherche
- Ober, Ileana (19..-.... ; enseignante-chercheuse en informatique)
- Co-directeur de recherche
- Ober, Iulian (19..-.... ; enseignant-chercheur en informatique)
- Gabreau, Christophe (19..-....)
- Date de soutenance
- 15 décembre 2022
- Établissement
- Université Toulouse-Jean Jaurès
- École doctorale
- MITT : Mathématiques Informatique Télécommunications de Toulouse
- Unité de recherche
- Institut de Recherche en Informatique de Toulouse - IRIT
- Mots-clés en français
- Certification
- Machine learning
- Système embarqué
- Généralisation
- Méthode formelle
- Mots-clés en anglais
- Certification
- Machine learning
- Embedded system
- Generalization
- Formal method
- Résumé en français
-
Récemment, les algorithmes d'apprentissage automatique (Machine Learning abrégé ML) ont prouvé leur grande efficacité dans la résolution de tâches (vision par ordinateur, reconnaissance vocale, détection d'objets, …) considérées comme difficiles à réaliser avec d'autres paradigmes de codage. Par conséquent, de nombreuses industries saisissent l'opportunité d'améliorer leurs produits et services en utilisant des algorithmes ML. Cependant, il est assez compliqué d'utiliser des algorithmes ML pour certaines de ces industries, comme l'automobile ou l’aéronautique, car elles utilisent des systèmes embarqués critiques.
Un système embarqué est critique lorsque sa défaillance entraîne des dommages aux produits et la mort ou la blessure de personnes. Ainsi, ces systèmes sont soumis à un processus de certification. Pourtant, il est impossible d'intégrer des systèmes basés sur le ML car certains objectifs de certification ne sont pas atteignables. L'industrie aéronautique dispose de nombreuses nouvelles applications intégrant des algorithmes ML sans pouvoir les utiliser car la certification des systèmes basés sur le ML n'est pas encore réalisable.
Cette thèse aborde dans un premier temps les lacunes qui empêchent la certification des systèmes basés sur le ML. Dans un second temps, nous développons les défis soulevés par ces lacunes avant de plonger dans les considérations de fiabilité des systèmes basés sur le ML. Parmi les questions liées à la certification, nous nous concentrerons sur deux sujets : la robustesse adversaire et la vérification formelle. La robustesse adversaire est la capacité d'un algorithme à résister à des "exemples adverses". Un "exemple adverse" est défini comme un exemple qui ressemble à un exemple "normal" mais qui trompe l'algorithme ML. La vérification formelle apporte la preuve que le modèle ML est conforme aux exigences.
Nous proposons dans cette thèse (i) d'améliorer la robustesse adversaire d'un algorithme ML en utilisant la théorie PAC-Bayes et (ii) l'analyse de la monotonie d'un réseau neuronal de substitution en utilisant un solveur MILP. Les deux contributions sont conformes aux premières directives fournies par l'EASA sur la certification des systèmes basés sur le ML. - Résumé en anglais
-
Lately, Machine Learning (ML) algorithms have proven their high efficiency in solving tasks (computer vision, speech recognition, object detection, etc.) that were considered hard to solve with other coding paradigms. As a result, numerous industries take the opportunity to improve their products and services using ML algorithms. However, for some of these industries, such as the automotive or the aeronautic industry, it is complicated to use ML algorithms since they deal with critical embedded systems.
An embedded system is critical when its failure leads to products damages and death or injury of people. Thus, critical embedded systems are subject to a certification process. Still, it is impossible to embed ML-based systems because some certification objectives are not reachable. The aeronautic industry has got many new applications using ML algorithms without the possibility of using them since the certification of ML-based systems is not yet achievable.
This thesis first discusses the gaps that prevent from certifying ML-based systems. Then, we elaborate on the challenges raised by these gaps before diving into the trustworthiness considerations of ML-based systems. Amongst the issues related to the certification, we will focus on two topics: adversarial robustness and formal verification. Adversarial robustness is the capacity of an algorithm to be resilient to adversarial examples. An adversarial example is defined as an example that looks like a “normal” example but fools the ML algorithm. Formal verification brings proof that the ML model complies with the requirements.
We propose in this thesis first to enhance the safety by design (during the learning process) by studying the adversarial robustness of an ML algorithm by using the PAC-Bayesian theory. Instead of deriving a worst-case analysis of the risk of a hypothesis over all the possible perturbations, we leverage the PAC-Bayesian framework to bound the averaged risk on the perturbations for majority votes (over the whole class of hypotheses). Then, we propose to improve the safety by verification (post learning) by analyzing the monotony property of a surrogate neural network using a MILP solver. This monotony analysis provides a lower and upper bound of the space volume where the property does not hold, which we denote ``Non-Monotonic Space Coverage''. Both contributions comply with the first guidance provided by the European Union Aviation Safety Agency (EASA) about ML-based systems certification. - Accès au document
- Accès libre
Citation bibliographique
Vidot, Guillaume (19..-....) (2022), Vers la certification des systèmes avioniques basés sur l'apprentissage automatique : exploitation des preuves mathématiques pour garantir la fiabilité [Thèse]