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

La grande polyvalence et les resultats impressionnants des reseaux de neurones modernes viennent en partie de leur non-linearite. Cette propriete fondamentale rend malheureusement tres difficile leur verification formelle, et ce, meme si on se restreint a une structure lineaire par morceaux. Cependant, chacune de ces regions lineaires prise independamment est simple a analyser. Nous proposons dans cet article une methode permettant de simplifier le probleme de verification en operant une separation en multiples sous-problemes lineaires. Nous presentons egalement des resultats concernant la structure de ces regions lineaires ainsi que leur similarite. Ce travail en cours demontre deja la faisabilite de l'approche sur des problemes simples ainsi que quelques experiences face a l'etat de l'art.