< Retour au sommaire

Computational techniques for boosting verification of deep learning algorithms

Julien Girard le

Lieu: salle 1073, bât 862

Abstract: For several years now, deep neural networks algorithms have been integrated in a wide range of software. Examples are numerous: object detection, image classification, robotic command and control, speech synthesis, natural language processing, time-data synthesis, etc. However, deep neural network based software display a range of vulnerabilites that still need to be addressed. At the same time, to integrate new code into critical software, strong guarantees are needed. Existing verification techniques tend not to scale on programs obtained with deep learning, and very few properties are currently researched. Modern SMT solvers struggle to verify simple satisfiable properties on simple networks. State of the art neural network verification usually relies on specific heuristics to cope with this. Modelling techniques help to lighten the burden on the solver, and specificities of deep neural networks are embedded within the tool reasoning engine. Some overapproximation techniques trade precision for scalability. During this talk, I will present the challenges one must tackle when verifying deep neural networks, and some techniques from the litterature to overcome those challenges.