Partitionnement en régions linéaires pour la vérification formelle de réseaux de neurones

National audienceLa grande polyvalence et les résultats impressionnants des réseaux de neurones modernes viennent en partie de leur non-linéarité. Cette propriété fondamentale rend malheureusement très difficile leur vérification formelle, et ce, même si on se restreint à une structure linéaire par morceaux. Cependant, chacune de ces régions linéaires prise indépendamment est simple à analyser. Nous proposons dans cet article une méthode permettant de simplifier le problème de vérification en opérant une séparation en multiples sous-problèmes linéaires. Nous présentons également des résultats concernant la structure de ces régions linéaires ainsi que leur similarité. Ce travail en cours démontre déjà la faisabilité de l'approche sur des problèmes simples ainsi que quelques expériences face à l'état de l'art