< Retour au sommaire
La confiance avec le contrôle : spécification et vérification d’hyperpropriétés sur réseaux de neurones
Guilhem Ardouin le
Lieu: Salle 1073
Suivre en visio
Abstract
L’apprentissage automatique consiste à produire des programmes qui res-
pectent certaines propriétés statistiques sur une distribution de probabilité. Ce
formalisme probabiliste se traduit notamment par la notion de « confiance »
qu’un programme porte sur sa sortie. Ainsi, un réseau de neurones peut modéliser
ses sorties comme une distribution de probabilité. La vérification de réseaux de
neurones se concentre encore majoritairement sur des propriétés dites « locales
» - c’est-à-dire ne portant que sur des points précis et sur leur voisinage. Nous
proposons dans cet article d’employer la notion de score de confiance pour écrire
des spécifications globales. Plus précisément, nous proposons de spécifier des
propriétés de robustesse sur des réseaux de neurones étant donné une certaine
probabilité affectée à une sortie - autrement dit, le niveau de confiance que le
programme accorde à sa prédiction. Contrairement aux propriétés de robustesse
locale communément rencontrées dans la littérature, notre approche permet une
spécification globale, c’est-à-dire pour tout point de l’espace d’entrée qui respecte
l’hypothèse de confiance. Cette approche ouvre ainsi la voie à la vérification de
propriétés portant sur tout l’espace d’entrée d’un réseau. Nous présentons un
travail de réécriture nécessaire pour traduire ces spécifications vers des prou-
veurs sur étagère, et évaluons les performances et limites de notre approche sur
plusieurs cas d’étude.