Ph.D
Group : Learning and Optimization
Verification and validation of Machine Learning techniques
Starts on 06/02/2020
Advisor : SCHOENAUER, Marc
Funding : Contrat doctoral uniquement recherche
Affiliation : Université Paris-Saclay
Laboratory : LRI - AO
Defended on 09/11/2021, committee :
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
Research activities :
Abstract :
Machine Learning techniques, Neural Networks in particular, are going through an impressive expansion, permeating various domains, becoming the next frontier for human societies. Autonomous vehicles, aircraft collision avoidance, cancer detection, justice advisors, or mooring line failure detection are but a few examples of Neural Networks applications.
This effervescence, however, may hold more than benefits, as it slowly but surely reaches critical systems.
Indeed, the remarkable efficiency of neural nets comes at a price, more and more underlined by the scientific consensus: weakness to environmental or adversarial perturbations, unpredictability... which prevents their full-scale integration into critical systems.
While the domain of critical software enjoys a plethora of methods that help verify and validate software (abstract interpretation, model checking, simulation, bounded tests...), these methods are generally useless when it comes to Neural Nets.
This thesis aims at bridging formal software verification and machine learning, in order to bring trust in critical systems incorporating Neural Networks elements.
We first study the exact causes that prevent a straightforward application of existing verification techniques on Neural Nets. We state that those issues are three fold: the lack of formal specification on the inputs, the piecewise linear structure that yield a combinatorial explosion and the lack of a common representation.
To tackle those issues, we present CAMUS, a theoretical framework allowing the specification of verification problems on perceptual inputs using simulators. We exploit the piecewise linear structure of neural networks on DISCO, an algorithm of parallel verification, to circumvent the combinatory explosion. We implement those contributions into ISAIEH, a prototypal platform for neural network encoding and verification.
