Résumé Technique : Vérification de Réseaux de Neurones à Virgule Flottante au Niveau Logiciel
Énoncé du Problème
Bien que la vérification des réseaux de neurones ait progressé de manière significative en fournissant des garanties formelles pour des modèles idéalisés à valeurs réelles, ces approches échouent souvent à prendre en compte les détails d'implémentation spécifiques des systèmes déployés. Dans les applications critiques pour la sécurité (par exemple, les CPS, l'IoT), les réseaux de neurones sont implémentés en utilisant une arithmétique à précision finie (généralement le standard IEEE 754 en 32 bits) et reposent sur des bibliothèques mathématiques standards (par exemple, math.h). Ces détails de bas niveau introduisent des erreurs d'arrondi et des comportements non associatifs qui peuvent invalider les preuves de sécurité dérivées de modèles à précision infinie. Par exemple, l'article démontre que la fonction d'activation SoftSign, qui est croissante dans l'arithmétique réelle, cesse de l'être lors de son implémentation en virgule flottante 32 bits.
Les tentatives existantes de vérification du code de réseaux de neurones au niveau logiciel ont donné des résultats mitigés. Les vérificateurs logiciels peinent souvent à passer à l'échelle pour de grandes instances de réseaux de neurones, forçant les praticiens à revenir à des modèles de précision infinie non-sound ou à abandonner la vérification au profit de tests. De plus, certains outils existants ont été observés comme produisant des résultats incorrects dans certains contextes, jetant le doute sur leur fiabilité en tant qu'oracles de sécurité pour les implémentations en virgule flottante. Il existe un manque d'évaluation rigoureuse et standardisée des vérificateurs de logiciels automatisés spécifiquement sur le code de réseaux de neurones.
Méthodologie
Pour combler ces lacunes, les auteurs ont mené une évaluation rigoureuse de huit vérificateurs de logiciels automatisés de pointe sur du code de réseaux de neurones. La méthodologie comprenait trois composantes principales :
Construction du Benchmark (NeuroCodeBench 2.0) : Les auteurs ont construit un benchmark complet comprenant 912 exemples de vérification. Ce benchmark couvre :
- Fonctions Mathématiques : 58 instances testant des propriétés (ex: monotonie, périodicité, bornes linéaires) de fonctions standards de
math.h.
- Fonctions d'Activation : 57 instances testant les propriétés d'activations courantes (ex: ReLU, TanH, SoftSign, GELU).
- Couches Neurales : 86 instances couvrant les transformations affines, la normalisation, le pooling et les couches SoftMax.
- Réseaux de Neurones Complets : 711 instances incluant des réseaux de Hopfield, des réseaux ReLU encodés par SAT, des réseaux d'approximation polynomiale, des réseaux à bornes de Lipschitz, et des réseaux dérivés de VNN-COMP (tâches de Densité de Probabilité et d'Apprentissage par Renforcement).
- Vérité Terrain (Ground Truth) : Chaque instance est pré-étiquetée comme "sûre" ou "non sûre" en utilisant des techniques telles que le test par force brute, la construction exhaustive ou la génération de contre-exemples, garantissant un verdict correct connu pour l'évaluation.
Standardisation et Compatibilité : Pour assurer une comparaison équitable et la reproductibilité, les auteurs ont converti tous les exemples du benchmark au format utilisé par l'International Competition on Software Verification (SV-COMP). Cela a impliqué la création de fichiers C autonomes incluant l'implémentation du modèle, les propriétés de sécurité et les dépendances nécessaires. Le flux de travail a utilisé le framework BenchExec pour gérer les limites de ressources et l'exécution, garantissant que les outils soient exécutés avec les mêmes configurations que celles utilisées pour l'édition 2024 de SV-COMP.
Évaluation Expérimentale : L'étude a évalué huit outils (2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer) sous deux conditions :
- Baseline : Exécution des vérificateurs sur les instances brutes du benchmark.
- Modèles Opérationnels : Fourniture d'implémentations C explicites de la bibliothèque
math.h (utilisant MUSL et CORE-MATH) pour voir si la fourniture des définitions de fonctions améliore les résultats de la vérification.
- Analyse Historique : Les auteurs ont également analysé la performance historique d'un outil (ESBMC) de 2018 à 2026 pour observer les tendances dans le domaine.
Contributions Clés
- NeuroCodeBench 2.0 : La création d'un benchmark à grande échelle, doté d'une vérité terrain, spécifiquement conçu pour la vérification logicielle de réseaux de neurones à virgule flottante. Il comprend 912 instances allant de fonctions simples à des réseaux complets avec jusqu'à 170K paramètres.
- Intégration SV-COMP : Le benchmark a été formaté pour être compatible avec l'infrastructure SV-COMP, ce qui en fait partie intégrante de l'ensemble de benchmarks officiel pour l'édition 2026. Cela permet une évaluation automatisée et reproductible à l'aide de configurations d'outils standards.
- Évaluation Rigoureuse : La première étude systématique comparant huit vérificateurs de logiciels de pointe sur le code de réseaux de neurones, révélant une variance significative de performance et de correction.
- Analyse des Modèles Opérationnels : Une enquête sur la question de savoir si la fourniture d'implémentations explicites de bibliothèques mathématiques (MUSL, CORE-MATH) améliore les performances des vérificateurs, concluant que l'impact est dépendant de l'outil et est souvent négligeable ou négatif.
Résultats
L'évaluation a produit plusieurs conclusions critiques concernant l'état actuel de la vérification logicielle pour les réseaux de neurones :
- Faible Correction et Scalabilité : Les résultats ont été décrits comme "plutôt décevants". Les outils ont montré une grande variance à travers le benchmark, le meilleur outil (CBMC) ayant résolu correctement 371 instances sur 912, tandis que d'autres en résolvaient nettement moins. Le taux de résolution moyen par catégorie variait, certaines catégories complexes (ex: Apprentissage par Renforcement) affichant des taux de résolution aussi bas que 3 %. La plupart des outils n'ont pas réussi à vérifier plus d'une seule couche neuronale à la fois.
- Verdict Incorrects : Plusieurs outils ont produit un taux élevé de résultats incorrects. Par exemple, CBMC a produit près de 25 % de verdicts définitifs incorrects (principalement des faux positifs), et Pinaka ainsi qu'UAutomizer ont également montré des taux d'erreur importants. Seul ESBMC n'a produit aucun verdict incorrect parmi les outils ayant résolu un nombre substantiel d'instances.
- Impact des Modèles Opérationnels : La fourniture d'implémentations explicites de
math.h (MUSL ou CORE-MATH) n'a pas conduit à des améliorations visibles globalement. Pour certains outils (CBMC, ESBMC, Pinaka), la performance a en réalité diminué en raison de la complexité ajoutée de la vérification du code de la bibliothèque. Pour d'autres (CPAChecker, PeSCo), le nombre d'instances résolues a augmenté, mais cela s'est souvent accompagné d'une explosion des verdicts incorrects.
- Limites de Scalabilité : Les outils ont lutté de manière significative avec les réseaux de neurones complets. Le taux de résolution est tombé à un chiffre pour des catégories complexes comme l'Apprentissage par Renforcement et la Densité de Probabilité. Même pour des réseaux synthétiques, des outils comme ESBMC ne pouvaient résoudre que des instances avec de très petites largeurs (ex: largeur 4) avant d'atteindre le timeout.
- Progrès Historiques : L'analyse d'ESMC de 2018 à 2026 a montré des améliorations non monotones mais généralement constantes. Un pic notable de verdicts incorrects en 2022-2023 a été attribué à une erreur d'implémentation dans un algorithme de k-induction, qui a été corrigée suite à la publication de NeuroCodeBench 1.0. L'introduction de NeuroCodeBench 1.0 en 2024 a conduit à une réduction drastique des verdicts incorrects dans toute la communauté, bien que l'impact de NeuroCodeBench 2.0 (fin 2025) ait été plus modéré.
Signification et Revendications
L'article affirme que bien que la vérification des réseaux de neurones au niveau logiciel soit conceptuellement faisable, les vérificateurs de logiciels de pointe actuels ne sont pas encore prêts à gérer cette tâche efficacement. L'étude souligne que les outils actuels ne peuvent pas vérifier de manière fiable plus d'une seule couche, renvoient fréquemment des résultats incorrects et manquent de support complet pour les bibliothèques mathématiques standards.
Les auteurs soutiennent que leur travail sert de "réalité check" nécessaire pour la communauté de la vérification. En fournissant un benchmark rigoureux avec une vérité terrain connue, ils démontrent que l'écart entre la vérification idéalisée et l'implémentation logicielle est actuellement trop large pour que les outils existants puissent le combler sans améliorations significatives. L'article pose que la publication de NeuroCodeBench a déjà stimulé le progrès, comme en témoigne la réduction des verdicts incorrects suite à sa première version. Cependant, les auteurs concluent que certifier l'implémentation complète des réseaux de neurones contre les déviations numériques extrêmes reste un défi à long terme nécessitant un support natif pour les bibliothèques mathématiques et des procédures de décision personnalisées adaptées à l'arithmétique de virgule flottante.