Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

Ce papier présente un cadre novateur qui permet de générer automatiquement des spécifications formelles à partir de descriptions en langage naturel, élargissant ainsi considérablement l'applicabilité des outils de vérification de réseaux de neurones à des exigences sémantiques de haut niveau.

L'essentiel

Imaginez que vous avez un chef cuisinier robot ultra-intelligent (le réseau de neurones) qui prépare des plats pour des millions de personnes. Ce robot est incroyable, mais il y a un problème : il ne parle que le langage des mathématiques pures et des coordonnées précises.

Si vous voulez lui dire : "Assure-toi que le plat reste bon même si on cache un peu le fromage", il ne comprend pas. Il a besoin que vous lui disiez exactement : "Modifiez les pixels 102 à 150 sur la ligne 40, en augmentant la luminosité de 10%." C'est fastidieux, risqué d'erreur, et personne ne veut faire ce travail de traduction manuelle.

C'est exactement là que cette recherche intervient. Voici l'explication simple de leur solution, avec quelques images pour bien comprendre.

1. Le Problème : Le "Mur de Traduction"

Aujourd'hui, pour vérifier si un robot (comme une voiture autonome ou un diagnostic médical) est sûr, les experts doivent écrire des règles très techniques.

• L'ancien système : C'est comme essayer de donner des instructions à un chef en lui écrivant une liste de coordonnées GPS pour chaque ingrédient. Si vous voulez vérifier la sécurité d'un plat, vous devez dire : "Si je change la couleur du pixel 45, le goût ne doit pas changer."
• La conséquence : Beaucoup de règles importantes (comme "Le robot ne doit pas paniquer si un enfant traverse la route") sont trop complexes à traduire en coordonnées. Donc, on ne les vérifie pas, ce qui est dangereux.

2. La Solution : Le "Traducteur Magique"

Les auteurs ont créé un pont automatique entre votre langage naturel et le langage du robot. Ils ont ajouté une couche intelligente entre vous et le vérificateur.

Imaginez que vous avez trois amis qui travaillent ensemble pour vous aider :

1. Le Traducteur (Le Grand Livre) : C'est un modèle de langage (comme une IA très savante). Quand vous dites "Vérifie si l'oiseau est toujours reconnu même si son bec est caché", ce traducteur comprend que vous parlez d'un "bec" et d'une action "cacher". Il ne cherche pas encore les pixels, il comprend juste le sens.
2. Le Détective (Le Loup-Garou) : C'est un modèle de vision par ordinateur. Il prend l'image de l'oiseau et le mot "bec" du traducteur. Il cherche dans l'image et dit : "Ah ! Le bec se trouve exactement ici, aux pixels 120 à 140." Il localise la zone précise.
3. L'Architecte (Le Constructeur) : Il prend les coordonnées du détective et les transforme en une règle mathématique que le vérificateur robot peut comprendre. Il dit au robot : "Vérifie maintenant si le résultat change si on cache cette zone précise (120-140)."

3. L'Analogie du "Filtre à Café"

Pensez à ce système comme un filtre à café :

• L'eau brute (Vos mots) : Vous versez des phrases naturelles et un peu floues ("Et si le bruit de forage est plus fort ?").
• Le filtre (Le système proposé) : Il nettoie l'eau. Il sépare le sens (le bruit de forage) de la forme (l'image ou le son), et trouve exactement où se trouve le bruit dans le fichier audio.
• Le café prêt (La vérification) : Ce qui sort de l'autre côté est une goutte pure, mathématique et parfaite, que le vérificateur robot peut boire sans se plaindre.

4. Pourquoi c'est génial ?

• Pas de réinvention de la roue : Ils n'ont pas créé un nouveau robot vérificateur (ce qui serait très long et difficile). Ils ont juste créé un traducteur qui utilise des outils existants (des IA de langage et de vision) pour parler aux anciens robots.
• C'est flexible : Que ce soit pour des tableaux de chiffres (comme les notes de crédit bancaire), des images (comme les oiseaux) ou même des sons (comme les sirènes d'urgence), le système s'adapte.
• La sécurité avant tout : Cela permet de vérifier des règles de sécurité "réelles" que les humains comprennent, et non pas des règles mathématiques abstraites.

En résumé

Cette recherche dit : "Arrêtons de demander aux humains de parler le langage des machines. Créons un interprète automatique qui traduit nos intentions humaines en règles mathématiques strictes."

C'est comme donner un microphone à un citoyen lambda pour qu'il puisse parler directement à un juge robot, sans avoir besoin d'apprendre le code juridique complexe. Cela rend la sécurité des intelligences artificielles beaucoup plus accessible et réaliste pour le monde réel.

Résumé technique

1. Problématique

Les outils de vérification formelle des réseaux de neurones profonds (DNN) actuels souffrent d'une limitation majeure : ils ne supportent qu'une classe étroite de spécifications, généralement exprimées sous forme de contraintes numériques de bas niveau sur les entrées et sorties brutes (par exemple, des perturbations bornées par une norme $L_p$ ou des contraintes géométriques fixes).

Cette limitation pose deux problèmes critiques :

• Expressivité réduite : De nombreuses exigences de sécurité et de correction, qui sont naturellement formulées à un niveau sémantique élevé (ex: « L'oiseau est correctement classifié même si son bec est occlus »), ne peuvent pas être encodées directement.
• Barrière à l'adoption : Les utilisateurs finaux doivent posséder une expertise technique pour traduire manuellement leurs intentions de haut niveau en contraintes mathématiques spécifiques à l'outil, ce qui est fastidieux, sujet aux erreurs et peu évolutif.

Le défi réside dans le fait que les DNN apprennent des représentations internes qui n'ont pas de mappage explicite vers des caractéristiques compréhensibles par l'humain, rendant difficile la connexion entre l'intention sémantique et la vérification formelle.

2. Méthodologie

L'article propose un cadre novateur qui agit comme une couche d'intégration entre les spécifications sémantiques en langage naturel et les moteurs de vérification existants. L'approche ne modifie pas les algorithmes de vérification sous-jacents, mais automatise la génération des requêtes de vérification.

Le pipeline proposé se compose de trois étapes principales :

1. Analyse et Parsing (LLM) :

   • Un Grand Modèle de Langage (LLM) analyse la spécification en langage naturel.
   • Il extrait deux éléments clés : (i) un ensemble d'objets sémantiques à localiser dans l'entrée (ex: « bec », « âge », « bruit de forage ») et (ii) une opération décrivant la modification souhaitée (ex: « occlusion », « amplification », « suppression »).

2. Ancrage Sémantique (Perception) :

   • Un modèle de perception (Vision-Language Model ou Audio-Language Model) localise les objets identifiés dans l'entrée concrète (image, tableau de données, signal audio).
   • Pour les images, des modèles de détection « open-vocabulary » (comme Grounding DINO) sont utilisés pour obtenir des coordonnées de boîtes englobantes.
   • Pour les données tabulaires, une correspondance directe est établie entre les noms de caractéristiques et les indices d'entrée.
   • Pour l'audio, des modèles de localisation d'événements sonores identifient les intervalles temporels pertinents.

3. Génération de Spécification Formelle :

   • Un générateur transforme les coordonnées localisées et l'opération en une requête de vérification numérique standard ($P_x$).
   • Cette requête est ensuite soumise à un vérificateur DNN existant (sans modification de celui-ci) pour déterminer si le modèle satisfait la propriété (SAFE) ou pour produire un contre-exemple (UNSAFE).

3. Contributions Clés

Les auteurs apportent trois contributions principales :

1. Identification d'un goulot d'étranglement d'utilisabilité : Ils mettent en évidence le besoin croissant de spécifier des exigences de correction sémantiques pour les systèmes DNN déployés et identifient la difficulté de traduction manuelle comme un obstacle majeur à l'adoption de la vérification formelle.
2. Mécanisme de génération automatique de spécifications : Ils proposent un système qui mappe l'intention utilisateur (langage naturel) vers des spécifications formelles en identifiant automatiquement les caractéristiques d'entrée ou les objets sémantiques pertinents. Ce mécanisme est applicable aux domaines structurés (tableaux) et non structurés (images, audio).
3. Démonstration empirique d'applicabilité : Ils valident l'approche sur des études de cas réelles, prouvant que le pipeline génère des requêtes vérifiables fiables sans modifier les backends de vérification existants.

4. Résultats Expérimentaux

L'évaluation a été menée sur deux types de benchmarks :

• Données tabulaires : Un réseau de classification de risque de crédit (Statlog German Credit).
• Images : Un classifieur ResNet-18 sur le jeu de données CUB-200-2011 (classification fine d'espèces d'oiseaux).

Résultats quantitatifs :

• Parsing (LLM) : Les modèles (GPT-5 Mini, Gemini 3 Flash) atteignent des taux de précision élevés (85% à 100%) pour l'identification des objets et des actions. GPT-5 Mini offre la meilleure précision, tandis que Gemini 3 Flash est plus rapide.
• Ancrage (Détection) : La phase de localisation visuelle est plus complexe. Avec Grounding DINO, la précision pour une configuration unique atteint 55%. Cependant, en combinant plusieurs configurations (mode « any »), le taux de succès global pour localiser correctement l'objet atteint 83%. Cela suggère que l'incertitude peut être gérée par des ensembles de modèles ou des heuristiques multiples.
• Audio : Bien que le cadre théorique soit défini pour l'audio, la composante de détection audio n'a pas été implémentée dans cette étude, mais le pipeline de traduction est décrit.

Résultats qualitatifs :
L'étude de cas sur les images montre que le système peut traduire des requêtes complexes comme « La prédiction peut-elle changer si l'épine violette du bas est plus bruyante ? » en une contrainte de robustesse locale précise, ciblant uniquement les pixels de l'épine détectée, évitant ainsi les perturbations globales inutiles.

5. Signification et Impact

Cet travail est significatif car il élargit considérablement le champ d'application de la vérification formelle des DNN vers des exigences de haut niveau, sans nécessiter de réinventer les algorithmes de vérification.

• Réutilisabilité : En s'appuyant sur des composants existants (LLM, modèles de perception, vérificateurs classiques), l'approche est immédiatement applicable et évolutive.
• Accessibilité : Elle démocratise l'accès à la vérification formelle pour des utilisateurs non experts, permettant de vérifier des propriétés de sécurité critiques (sécurité routière, diagnostic médical) exprimées dans un langage naturel.
• Futur : Le cadre ouvre la voie à la vérification de spécifications temporelles (vidéo, audio) et à un ancrage plus fin (segmentation au niveau du pixel).

En résumé, l'article propose un pont essentiel entre l'intention sémantique humaine et la rigueur mathématique de la vérification formelle, rendant les outils de vérification applicables à des scénarios du monde réel complexes et variés.