🤖 machine learning

VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

Ce papier présente VNN-LIB 2.0, une norme rigoureusement formalisée pour la vérification des réseaux de neurones qui introduit une abstraction de « théorie des réseaux » pour découpler la spécification des modèles ONNX en évolution, tout en fournissant une syntaxe précise, un système de types et une sémantique mécanisés dans Agda pour garantir la cohérence interne et l'interopérabilité.

Auteurs originaux : Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

Publié 2026-05-11

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de faire résoudre une énigme à une équipe de robots différents. Dans le monde de l'Intelligence Artificielle, ces « robots » sont des réseaux de neurones (les cerveaux derrière l'IA), et l'« énigme » est la vérification (vérifier si l'IA prendra une décision sûre ou correcte).

Pendant longtemps, les personnes qui construisaient ces robots et celles qui les vérifiaient ne parlaient pas la même langue. Elles utilisaient une norme appelée VNN-LIB 1.0, mais c'était comme un dictionnaire avec des mots manquants, sans règles de grammaire, et des définitions qui changeaient à chaque fois que quelqu'un les regardait.

Ce document présente VNN-LIB 2.0, un nouveau « langage » rigoureux qui résout ces problèmes. Voici comment les auteurs l'expliquent en utilisant des concepts simples :

1. Le Problème : Un Traducteur Défectueux

Imaginez VNN-LIB 1.0 comme un traducteur qui essayait de parler deux langues à la fois mais qui restait confus.

Pas de Grammaire : Il n'avait pas de règles strictes sur la façon de formuler une question. Ainsi, un robot pouvait comprendre une phrase d'une manière, et un autre robot pouvait la comprendre différemment.
Vocabulaire Limité : Il ne pouvait gérer que des énigmes simples (une entrée, une sortie). L'IA du monde réel a souvent des entrées complexes (comme une image et du texte) et plusieurs sorties.
Confusion sur les Nombres à Virgule Flottante : Les ordinateurs utilisent des nombres « approximatifs » (comme 3,14159...), mais l'ancienne norme ne spécifiait pas si vous deviez les traiter comme des mathématiques exactes ou des approximations grossières. Cela a conduit à des erreurs dangereuses où un robot pensait être sûr, alors qu'il ne l'était pas.
Le Problème de la « Boîte Noire » : L'ancienne norme s'appuyait sur un format de fichier appelé ONNX (le plan de l'IA). Mais ONNX n'avait pas de définition stricte et officielle de ce que signifiaient ses symboles. C'était comme donner à un robot un plan dessiné au crayon de cire qui changeait d'avis à chaque instant sur ce qu'est un « mur ».

2. La Solution : La « Théorie des Réseaux » (L'Adaptateur Universel)

La plus grande innovation de ce document est un concept appelé une Théorie des Réseaux.

Imaginez que vous construisez un adaptateur électrique universel. Vous ne voulez pas construire un nouvel adaptateur pour chaque prise murale de chaque pays (chaque version d'ONNX). Au lieu de cela, vous créez une interface universelle qui dit : « Tant que la prise fournit de l'électricité, de la tension et une terre, je peux brancher. »

La Théorie des Réseaux ( $\Psi$ ) : C'est cette interface universelle. Elle ne se soucie pas exactement de la façon dont le plan ONNX est dessiné. Elle demande simplement : « Avez-vous un moyen de définir un nombre ? Une forme ? Une connexion ? »
Le Résultat : VNN-LIB 2.0 peut maintenant parler à n'importe quelle version d'ONNX, même les futures, sans avoir besoin d'être réécrit. Il sépare la question (la requête) du plan (le modèle), permettant à chacun d'évoluer indépendamment.

3. Le Nouveau Langage : VNN-LIB 2.0

Avec cette nouvelle fondation, les auteurs ont construit un langage beaucoup plus intelligent avec trois améliorations principales :

Phrases Plus Riches (Syntaxe) : Vous pouvez maintenant poser des questions sur des scénarios complexes. Au lieu de simplement vérifier un seul robot, vous pouvez demander : « Si le Robot A et le Robot B travaillent ensemble, restent-ils sûrs ? » Vous pouvez aussi jeter un coup d'œil à l'intérieur du « cerveau » du robot pour vérifier ses pensées cachées (couches cachées), et pas seulement la réponse finale.
Grammaire Stricte (Système de Types) : Le langage vous force maintenant à être précis. Si vous essayez d'ajouter une « température » à une « couleur », le langage dira : « Non, cela n'a pas de sens. » Cela empêche l'ordinateur de faire des erreurs mathématiques en mélangeant différents types de nombres.
Signification Claire (Sémantique) : Chaque mot du nouveau langage a une définition prouvée mathématiquement. Il n'y a pas de devinettes. Si vous écrivez une requête, l'ordinateur sait exactement quel problème mathématique vous lui demandez de résoudre.

4. L'Option « Monde Réel » vs « Mathématiques Parfaites »

Le document reconnaît une situation délicate : certains robots sont vérifiés en utilisant des « mathématiques parfaites » (nombres réels), tandis que le robot réel fonctionne avec des « mathématiques approximatives » (nombres à virgule flottante).

L'Ancienne Façon : C'était un danger caché. Le vérificateur dirait « Sûr », mais le vrai robot pourrait planter.
La Nouvelle Façon : VNN-LIB 2.0 vous permet de dire explicitement : « Je sais que cela utilise des mathématiques approximatives, mais je veux quand même le vérifier en utilisant des mathématiques parfaites. » Il place une étiquette d'avertissement sur la requête : « Procédez avec prudence, cela pourrait être légèrement imprécis. » Cela permet aux chercheurs d'utiliser des outils puissants sans prétendre que les mathématiques sont parfaites alors qu'elles ne le sont pas.

5. La Preuve « Référence Or »

Pour s'assurer qu'ils n'avaient fait aucune erreur en écrivant ce nouveau langage, les auteurs ne se sont pas contentés de l'écrire ; ils l'ont programmé dans un robot de preuve mathématique appelé Agda.

Imaginez Agda comme un éditeur ultra-sévère qui vérifie chaque règle du nouveau langage pour s'assurer qu'il n'y a aucune faille logique.
Parce que le langage est « mécanisé » dans Agda, n'importe qui peut maintenant utiliser cette preuve pour vérifier que ses propres outils (solveurs) fonctionnent correctement. Cela transforme la norme d'une « suggestion » en un « contrat mathématiquement garanti ».

Résumé

En bref, VNN-LIB 2.0 est un nouveau langage strict et flexible pour poser des questions de sécurité à l'IA. Il répare la grammaire défectueuse du passé, permet des questions complexes sur plusieurs modèles d'IA, et fournit une fondation mathématiquement prouvée afin que, lorsqu'un outil dit « Cette IA est sûre », nous puissions réellement faire confiance au fait qu'il signifie exactement ce qu'il dit.

Résumé Technique : VNN-LIB 2.0 : Fondements Rigoureux pour la Vérification des Réseaux de Neurones

Énoncé du Problème

La communauté de la vérification des réseaux de neurones s'est de plus en plus appuyée sur la norme VNN-LIB (Version 1.0) pour faciliter l'interopérabilité entre les solveurs et les outils de haut niveau. Cependant, la Version 1.0 souffre de quatre déficiences critiques qui l'empêchent de servir de fondement formel rigoureux :

Absence de Syntaxe Formelle : La Version 1.0 ne définit pas formellement la syntaxe du langage de requêtes, ce qui conduit à des implémentations mutuellement incompatibles par différents solveurs.
Expressivité Limitée : La norme suppose un seul réseau avec une seule entrée et une seule sortie. Elle ne peut pas prendre en charge nativement plusieurs réseaux, plusieurs entrées/sorties, ou l'accès aux couches cachées, contraignant les utilisateurs à fusionner artificiellement les modèles, ce qui obscurcit la relation entre les artefacts vérifiés et les modèles déployés.
Absence de Système de Types : Il n'existe aucun mécanisme pour spécifier les types numériques (par exemple, virgule flottante par rapport à des valeurs réelles), créant une ambiguïté et une éventuelle insoundness lorsque les solveurs traitent l'arithmétique de précision finie comme des valeurs réelles.
Absence de Sémantique : La norme manque d'une sémantique formelle, rendant impossible la preuve formelle de la correction des solveurs, des générateurs de requêtes ou des transformations, et entravant le développement de certificats de preuve.

Un défi unique pour VNN-LIB, le distinguant de normes comme SMT-LIB, est que les requêtes ne sont pas autonomes ; elles spécifient des propriétés de modèles de réseaux de neurones externes (généralement au format ONNX). Puisque ONNX lui-même manque d'une sémantique formelle et continue d'évoluer, définir une norme VNN-LIB rigoureuse nécessite de découpler le langage de requêtes des versions spécifiques d'ONNX tout en maintenant la compatibilité.

Méthodologie

Les auteurs répondent à ces défis en développant les fondements théoriques de VNN-LIB 2.0. L'innovation méthodologique centrale est l'introduction de la Théorie des Réseaux ( $\Psi$ ).

1. Abstraction de la Théorie des Réseaux

Les auteurs définissent une « théorie des réseaux » comme une spécification abstraite capturant la syntaxe minimale, les jugements de typage et la sémantique requis d'un format de modèle de réseau de neurones pour définir VNN-LIB.

Découplage : $\Psi$ agit comme une interface. Une implémentation concrète de $\Psi$ (par exemple, pour ONNX v1.20.0) fournit des définitions spécifiques pour les types d'éléments, les représentations de tenseurs, les structures de modèles et les références de sortie de nœuds.
Modularité : VNN-LIB 2.0 est défini par rapport à un $\Psi$ abstrait. Cela permet à la norme de rester stable même si ONNX évolue ; seule l'instanciation de $\Psi$ doit être mise à jour pour les nouvelles versions d'ONNX, et non la norme VNN-LIB elle-même.
Formalisation : L'ensemble de la norme, y compris la syntaxe, le typage et la sémantique, est mécanisé dans le prouveur de théorèmes interactif Agda pour assurer la cohérence interne et éliminer les ambiguïtés.

2. Syntaxe Formelle et Expressivité

S'appuyant sur la théorie des réseaux, les auteurs définissent une grammaire formelle pour VNN-LIB 2.0 qui étend considérablement l'expressivité :

Multiples Réseaux : Les requêtes peuvent déclarer plusieurs réseaux, prenant en charge des scénarios tels que la vérification enseignant-élève ou les architectures encodeur-décodeur.
Équivalence de Réseaux : La norme introduit les déclarations equal-to (faisant référence au même fichier de modèle exact) et isomorphic-to (faisant référence à des modèles ayant la même structure de graphe mais potentiellement des poids différents). Cela permet aux solveurs de partager des déductions (par exemple, des bornes de variables) à travers des copies de réseaux.
Nœuds Cachés : La construction declare-hidden permet des contraintes sur les sorties des couches intermédiaires, essentielles pour raisonner sur les encodages ou les mécanismes d'attention.
Entrées/Sorties Multidimensionnelles : Prise en charge d'un nombre arbitraire d'entrées et de sorties, accommodant les réseaux multimodaux.

3. Système de Types et Sémantique

Typage : Un système de types formel impose la soundness numérique. Il garantit que les opérations arithmétiques et les comparaisons sont effectuées sur des types compatibles (par exemple, empêchant le mélange de float32 et int32 sans règles de coercition explicites). Le système de types repose sur les jugements fournis par la théorie des réseaux sous-jacente $\Psi$ .
Sémantique : La sémantique d'une requête est définie comme un problème de satisfaisabilité mathématique. Étant donné un ensemble de modèles $M$ (instanciés à partir de $\Psi$ ) et une affectation d'entrée $X$ , la sémantique détermine s'il existe une affectation où toutes les affirmations s'évaluent à vrai.
Requêtes à Valeurs Réelles : Pour accommoder les solveurs existants qui traitent les modèles comme des fonctions sur les nombres réels ( $\mathbb{R}$ ), la norme introduit un mécanisme pour les « requêtes à valeurs réelles ». En utilisant un type real distinct, l'auteur de la requête autorise explicitement le solveur à interpréter les modèles sur $\mathbb{R}$ , reconnaissant une éventuelle insoundness due à l'imprécision de la virgule flottante. Cela est réalisé en construisant une théorie de réseau spécifique $\Psi_{\mathbb{R}}$ dérivée de la théorie de base.

Contributions Clés

Théorie des Réseaux ( $\Psi$ ) : L'introduction d'une abstraction novatrice définissant l'interface sémantique minimale requise d'un format de modèle, permettant à VNN-LIB d'être défini indépendamment des versions spécifiques d'ONNX.
Syntaxe et Grammaire Formelles : Une grammaire précise et sans contexte pour VNN-LIB 2.0 qui prend en charge plusieurs réseaux, des couches cachées et des structures d'entrées/sorties complexes.
Système de Types Formel : Un système de typage qui impose la soundness des types numériques par rapport à la théorie des réseaux, traitant l'ambiguïté dans les représentations numériques.
Sémantique Formelle : Une définition mathématique rigoureuse de la sémantique des requêtes paramétrée par la théorie des réseaux, permettant des preuves formelles de correction pour les outils consommant ou générant VNN-LIB.
Mécanisation : L'ensemble de la norme est formalisé dans Agda, fournissant une implémentation de référence canonique et un fondement pour des preuves vérifiées par machine.
Extension à Valeurs Réelles : Une approche modulaire pour soutenir les analyses à valeurs réelles via une théorie de réseau dérivée, équilibrant le besoin de soundness avec la réalité des capacités actuelles des solveurs.

Résultats et Validation

Cohérence Interne : La formalisation Agda valide la cohérence interne de la syntaxe, du typage et de la sémantique, garantissant que la norme est exempte des ambiguïtés présentes dans la Version 1.0.
Démonstration d'Expressivité : L'article démontre comment une transformation simple de la théorie des réseaux $\Psi$ produit une instance complète pour les requêtes à valeurs réelles, mettant en évidence la flexibilité de l'abstraction.
Adoption par la Communauté : La norme a reçu des retours positifs de la communauté de vérification. Les équipes de solveurs leaders se sont engagées à soutenir VNN-LIB 2.0, et la nouvelle norme est prévue pour être utilisée dans la compétition VNN-COMP 2026.
Support d'Outils : Les auteurs ont publié une bibliothèque C++ haute performance (avec des liaisons Python et Julia) implémentant un analyseur syntaxique et un vérificateur de types conformes à la nouvelle norme, accompagnée de la formalisation Agda.

Importance

L'article affirme que VNN-LIB 2.0 fournit des fondements robustes et rigoureux pour une vérification fiable des réseaux de neurones. Son importance réside dans deux domaines complémentaires :

Interopérabilité Pratique : En étendant l'expressivité (multiples réseaux, nœuds cachés) et en standardisant la syntaxe, elle permet à la communauté de spécifier et de vérifier des propriétés plus riches de manière unifiée, facilitant un meilleur étalonnage et une comparaison des outils.
Rigueur Théorique : En fournissant une sémantique formelle et un système de types, elle établit un « contrat rigoureux » entre les outils et les solveurs. Cela permet la vérification formelle des outils eux-mêmes (solveurs, optimiseurs, vérificateurs de preuve) et résout des problèmes subtils concernant la soundness numérique (par exemple, la distinction entre les sémantiques à valeurs réelles et à virgule flottante).

Les auteurs soulignent que bien que le travail soit théorique, il a des conséquences concrètes : il garantit une interprétation sans ambiguïté des requêtes, fournit le langage pour résoudre des problèmes techniques et pose les bases de certificats de preuve formellement vérifiés à l'avenir.