Alors que l’IA occupe une place de plus en plus importante dans notre quotidien, son déploiement au sein de systèmes critiques est un enjeu clé de son succès. Dans ces systèmes, où la moindre défaillance peut provoquer des dommages humains, économiques ou environnementaux irréparables, il est indispensable que toute application logicielle soit certifiée (c’est-à-dire que son comportement soit jugé conforme au cahier des charges en conditions d’utilisation nominales).
C’est dans cet objectif que les équipes du CEA-List développent des outils de vérification formelle destinés aux applications d’intelligence artificielle. Ils apportent des garanties mathématiques fortes quant au fonctionnement des IA, en vue de leur application en contexte industriel et opérationnel. C’est notamment la vocation de notre outil de vérification formelle de réseaux de neurones, PyRAT, créé en 2019.
PyRAT permet de vérifier la stabilité d’un réseau de neurones (RdN) face à de légères perturbations de ses entrées. Par exemple, dans le domaine de la vision par ordinateur pour l’automobile, considérant un RdN chargé de la reconnaissance automatique des panneaux de signalisation routière, PyRAT contrôlera que la réponse de l’IA ne change pas lorsqu’il pleut ou que la luminosité baisse.
Il est également possible de vérifier qu’un RdN respecte certaines contraintes de son cahier des charges, dès lors que ces dernières peuvent être exprimées par une formule mathématique.
Pour mener à bien cette procédure de vérification (notoirement complexe), PyRAT se base sur des méthodes classiques d’interprétation abstraite et les combine à des optimisations logicielles adaptées aux RdN (parallélisation sur carte graphique, opérations matricielles…). PyRAT intègre également une représentation précise des opérations complexes des RdN, lui permettant de minimiser les erreurs d’abstractions durant l’analyse. Enfin, l’ajout de méthodes itératives dites « diviser pour régner » ainsi que de nouvelles méthodes d’optimisation ont permis une nette amélioration des performances (précision du résultat et rapidité d’analyse) de PyRAT en l’espace d’un an.
En effet, PyRAT a participé deux années consécutives à la compétition internationale de vérification de RdN, atteignant la 3e place en 2023 et la 2e place en 2024. Ce résultat montre l’excellence académique de cet outil utilisé dans l’industrie, renforçant notre position de leader en vérification formelle. Nos futurs travaux vont permettre d’optimiser encore les performances de l’outil, tout en étendant son champ d’application à de nouveaux types de RdN, plus complexes (transformers, RNN…). Enfin, PyRAT va également être adapté à l’analyse des RdN destinés à l’embarqué (RdN quantifiés).
Cette deuxième place à la VNN-Comp confirme l’efficacité de PyRAT pour assurer la sûreté et la sécurité des systèmes à base d’IA.
“Neural Network Verification with PyRAT”, ArXiv preprint 2410.23903
