​Comment prouver qu'un réseau de neurones auquel on a « appris » à reconnaître un piéton est fiable ? La validation formelle des réseaux de neurones appliqués à la reconnaissance d'images, impérative dans les secteurs critiques, constituait un verrou technique majeur. Car avant de vérifier, par exemple, la capacité d'un véhicule à éviter efficacement tous les piétons, il faut savoir spécifier de manière non ambigüe ce qu'est un piéton.

Puisque décrire mathématiquement un piéton est impossible, les chercheurs du CEA-List ont eu l'idée de s'appuyer sur les générateurs d'images (appelés simulateurs) qui servent à « entraîner » les réseaux de neurones. Ce choix est d'autant plus intéressant que les simulateurs sont largement utilisés, notamment par les constructeurs automobiles, pour pallier le manque de données d'entraînement venant du monde réel. Les chercheurs ont ainsi proposé un nouveau formalisme de spécification qui intègre le simulateur au cœur du processus de validation, où il joue le rôle de spécification formelle des propriétés que le réseau de neurones doit satisfaire. Les méthodes d'analyse formelle classiques, expertise reconnue des équipes du CEA-List, peuvent ensuite être appliquées à ce dernier pour valider sa conformité.

Les résultats théoriques ont été publiés dans une conférence majeure en intelligence artificielle (European Conference on Artificial Intelligence -ECAI 2020) [1], et la preuve de concept a été réalisée avec succès sur un simulateur « réduit » spécialement conçu pour cet usage. Si la prochaine étape consiste à valider la théorie par un « passage à l'échelle », cette approche pionnière est une avancée importante et concrète vers l'IA de confiance.

[1] Girard-Satabin, J.; Charpiat, G.; Chihani, Z. & Schoenauer, M. "CAMUS: A Framework to Build Formal Specifications for Deep Perception Systems Using Simulators" ECAI 2020