Doctorat
Equipe : Apprentissage et Optimisation
Vérification et validation de techniques d'apprentissage machine
Début le 06/02/2020
Direction : SCHOENAUER, Marc
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI - AO
Soutenue le 09/11/2021 devant le jury composé de :
Direction de thèse :
- M. Marc SCHOENAUER
Rapporteurs :
- M. Antoine MINÉ
- M. Pawan KUMAR
Co-encadrants de thèse :
- M. Zakaria CHIHANI
- M. Guillaume CHARPIAT
Examinateurs :
- Mme Sylvie PUTOT
- Mme Caterina URBAN
- M. Gilles DOWEK
Activités de recherche :
Résumé :
L'apprentissage machine, en particulier au moyen des réseaux de neurones artificiels, connaît depuis une dizaine d'année une expansion impressionnante.
Véhicules autonomes, capteurs d'anomalies d'ancrage sur des plateformes offshores, détecteurs de collision d'aéronefs, aide au diagnostic pour différents cancers sont autant d'applications faisant intervenir les technologies d'apprentissage profond au sein de systèmes critiques; ouvrant des perspectives inexplorées pour les sociétés humaines.
Bien que bénéfique en apparence, cette révolution a de quoi inquiéter à mesure qu'elle se concrétise: la fragilité de ces techniques d'apprentissage est désormais un fait scientifique établi.
La taxonomie des vulnérabilités, qu'elles soient accidentelles ou malicieuses, remet en question la possibilité d'intégrer des réseaux de neurones dans des domaines critiques qui pourraient pourtant en bénéficier.
A l'heure actuelle, peu de méthodes permettent de démontrer formellement la fiabilité d'un réseau de neurones.
Par contraste, le domaine du logiciel critique, quant à lui, jouit d’une multitude de méthodes et techniques: vérification formelle, model checking, simulation, interprétation abstraite, tests dirigés, etc.
L'objectif de cette thèse est de réconcilier l'abondance des techniques de vérification de programmes classiques et l'absence de garanties sur les réseaux de neurones, ce pour permettre aux logiciels critiques de conserver le haut niveau de confiance qu'ils ont atteint quand ils seront inévitablement modifiés avec des mécanismes d'apprentissage machine.
Nous étudions d'abord en détail les raisons qui empêchent l'application directe des approches de vérification formelle classique. Nous mettons ainsi en évidence que l'absence de spécification formelle inhérente aux entrées à hautes dimensions, la structure linéaire par morceau des réseaux de neurones entraînant une explosion combinatoire, et l'absence de représentation adaptée à la vérification empêchent l'emploi de la plupart des approches.
Pour pallier le problème de la spéficiation, nous présentons CAMUS, une approche théorique permettant de formuler un problème de vérification formelle avec l'aide d'un simulateur. Nous exploitons la structure linéaire par morceau pour proposer DISCO, un algorithme de vérification parallèle pour contourner l'explosion combinatoire.
Enfin, nous implémentons nos contributions au sein d'ISAIEH, un prototype de plate-forme d'encodage pour les réseaux de neurones à vérifier.
