De nombreux outils comme PyRAT peuvent être utiliser pour vérifier la sûreté ou la sécurité d'un réseau de neurones. Chacun d'entre eux, même s'ils se basent sur différentes méthodes ou implémentations se heurtent à une limite quand confrontés à des réseaux très complexes de grande taille. Le nombre élevé de paramètres et de couches introduit une grande imprécision dans l'analyse qui ne permet alors pas de vérifier complètement le réseau.
Des premiers résultats d'entraînement robuste avec des méthodes formelles sur un réseau de neurones ont montré que cet entraînement pouvait non seulement réduire le temps de la vérification mais aussi augmenter la précision de celle-ci. L'influence d'autres techniques d'entraînement tels qu'avec des réseaux quantifiés, Lipschitz, ou sparse sur le procédé de vérification pourrait être un moyen de surmonter la complexité des grands réseaux.

Le but de ce stage est d'aider dans l'étude du lien entre ces techniques d'entraînement et de vérification. Ce stage pourra être divisé en deux parties: l'entraînement des différents réseaux avec les différentes techniques sur des datasets différents et la vérification correspondante de ces réseaux. Pour la vérification en fonction de l'architecture du réseau des développements supplémentaires pourront être réalisés sur l'outil de vérification. Après avoir tester les techniques existantes, de nouvelles techniques pourront être extrapolées et testées à leur tour.
Ce travail s’effectuera en collaboration avec un doctorant.

#StageList

Étudiant en Bac +4/5 dans le domaine de l'informatique avec des connaissances en Python et des connaissances en réseaux de neurones.