Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

Questo lavoro presenta un nuovo framework che colma il divario tra i requisiti semantici di alto livello e gli strumenti di verifica formale delle reti neurali, traducendo automaticamente specifiche in linguaggio naturale in query verificabili per estendere l'applicabilità della verifica DNN a scenari reali complessi.

L'essenziale

Immagina di avere un cervello digitale (una rete neurale) che guida un'auto a guida autonoma o fa diagnosi mediche. Questo cervello è incredibilmente intelligente, ma ha un problema: è un po' "sordo" al linguaggio umano.

Se tu gli chiedessi: "Se il cane attraversa la strada, l'auto frena?", il cervello digitale non capisce cosa sia un "cane" o cosa significhi "attraversare". Per fargli capire, oggi dovresti essere un programmatore esperto e dirgli: "Se i pixel nelle coordinate (x=100, y=200) cambiano di colore, allora l'output deve essere 'ferma'". È come se dovessi spiegare a un umano come funziona il suo stesso cervello, pixel per pixel. È noioso, difficile e facile sbagliare.

La Soluzione: Il "Traduttore Magico"

Questo articolo presenta un nuovo sistema, un ponte tra quello che diciamo noi (in linguaggio naturale) e quello che capisce il verificatore formale (il "controllore di sicurezza" della rete neurale).

Ecco come funziona, usando una metafora culinaria:

1. L'Ordinazione (L'Input Utente):
   Tu, come cliente, vuoi verificare che un piatto sia sicuro. Invece di scrivere una lista chimica di ingredienti, dici semplicemente: "Voglio assicurarmi che se il pomodoro è coperto da un foglio di basilico, il sapore non cambi".
   Nel paper: L'utente scrive una specifica in linguaggio naturale (es. "L'uccello è classificato correttamente anche se il becco è coperto").

2. Lo Chef Traduttore (Il Modello Linguistico - LLM):
   Qui entra in gioco il nostro "traduttore". È un'intelligenza artificiale molto brava con le parole. Il suo compito non è cucinare, ma tradurre la tua richiesta in un ordine preciso per la cucina.
   Nel paper: Un modello linguistico (come GPT o Gemini) legge la tua frase e capisce: "Ok, l'oggetto da cercare è 'becco dell'uccello' e l'azione da simulare è 'coprirlo'".

3. Il Cameriere con gli Occhiali Magici (Il Modello di Percezione):
   Una volta che il traduttore ha detto "cerca il becco", il cameriere (un modello di visione artificiale) guarda il piatto (l'immagine) e ti indica esattamente dove si trova quel becco. Non dice "è a sinistra", ma ti dà le coordinate esatte: "È in quel quadrato rosso qui".
   Nel paper: Un modello di rilevamento (come Grounding DINO) trova l'oggetto specifico nell'immagine e ne estrae le coordinate.

4. Il Controllore di Sicurezza (Il Verificatore Formale):
   Ora che abbiamo le coordinate esatte, il sistema invia un messaggio al "controllore di sicurezza" (il verificatore formale). Questo controllore è molto rigoroso e non parla il linguaggio umano, ma capisce perfettamente la matematica. Gli viene detto: "Simula il rumore solo su questo quadrato rosso (il becco) e controlla se il risultato cambia".
   Nel paper: Il sistema genera una query matematica standard che il verificatore esistente può risolvere immediatamente.

Perché è una Rivoluzione?

Prima di questo lavoro, era come se volessi controllare la sicurezza di un aereo, ma fossi costretto a scrivere le specifiche in codice binario, indicando ogni singolo bullone. Se volevi dire "le ali devono resistere al vento", dovevi prima calcolare manualmente quali bulloni compongono l'ala e scrivere equazioni complesse per ognuno.

Ora, con questo sistema:

• Parli come un umano: Puoi dire "Se il becco è coperto" o "Se il rumore di trapano è più forte".
• Il sistema fa il lavoro sporco: Traduce automaticamente la tua frase in matematica precisa.
• Nessuno cambia le regole: Il "controllore di sicurezza" (il verificatore) rimane lo stesso, potente e affidabile di prima. È solo che ora capisce cosa gli diciamo grazie al traduttore.

In Sintesi

Gli autori hanno creato un ponte linguistico. Hanno preso strumenti che già esistono (modelli di linguaggio come ChatGPT, modelli di visione come quelli che riconoscono oggetti nelle foto) e li hanno collegati agli strumenti di verifica formale.

Il risultato? Possiamo ora chiedere alle reti neurali: "Se nascondi il becco dell'uccello, la macchina sbaglia ancora?" e ottenere una risposta matematica certa, senza dover essere esperti di matematica o di codice. È come avere un interprete che ti permette di parlare con un genio matematico nella sua lingua madre, senza dover studiare la matematica tu stesso.

Sommario tecnico

1. Il Problema: Il Divario tra Intento Semantico e Vincoli di Verifica

Le reti neurali profonde (DNN) sono sempre più utilizzate in sistemi critici per la sicurezza (guida autonoma, diagnosi medica, ecc.). Sebbene esistano strumenti avanzati per la verifica formale di queste reti, la loro adozione pratica è limitata da un collo di bottiglia fondamentale: la difficoltà di esprimere le specifiche di correttezza.

Attualmente, gli strumenti di verifica richiedono specifiche a basso livello, definite come vincoli numerici rigidi su dimensioni di input fisse (es. "l'input $x_3$ deve essere $\le 50$"). Questo approccio presenta due gravi limitazioni:

1. Mancanza di espressività semantica: Molti requisiti di correttezza sono naturalmente espressi a un livello semantico più alto (es. "Il modello non deve cambiare decisione se l'età è inferiore a 50" o "L'uccello è classificato correttamente anche se il becco è oscurato").
2. Sforzo manuale ed errore-prone: Gli utenti devono tradurre manualmente questi intenti ad alto livello in vincoli numerici specifici per lo strumento, un processo che richiede competenze specialistiche e che è soggetto a errori.
3. Incapacità di gestire input non strutturati: Per input come immagini o audio, le regioni semantiche rilevanti (es. un "becco" o un "suono di trapano") variano da istanza a istanza e non possono essere catturate da coordinate fisse o perturbazioni globali uniformi.

2. Metodologia: Un Pipeline di Generazione Automatica delle Specifiche

Gli autori propongono un nuovo componente di integrazione che colma il divario tra l'intento dell'utente (espresso in linguaggio naturale) e i motori di verifica formale esistenti. L'approccio non modifica gli algoritmi di verifica sottostanti, ma costruisce un livello di traduzione automatica basato su modelli fondazionali (Foundation Models).

Il sistema opera attraverso una pipeline automatizzata in tre fasi (Algoritmo 1):

1. Parsing (Analisi Semantica):

   • Un Large Language Model (LLM) analizza la specifica in linguaggio naturale.
   • Estrae due elementi chiave: (i) un insieme di oggetti semantici da localizzare nell'input (es. "becco", "età", "suono di trapano") e (ii) l'operazione da eseguire (es. "oscurare", "amplificare", "rimuovere").

2. Grounding (Ancoraggio al Contesto):

   • Un modello di percezione specializzato (Vision-Language Model o Audio-Language Model) localizza gli oggetti estratti nell'input concreto.
   • Per immagini: Utilizza modelli open-vocabulary come Grounding DINO per identificare le coordinate spaziali (bounding box) degli oggetti descritti.
   • Per audio: Utilizza modelli di localizzazione di eventi sonori (es. DASM, FlexSED) per identificare intervalli temporali.
   • Per dati tabulari: Mappa direttamente i nomi delle feature estratte agli indici delle colonne del dataset.
   • Nota: Il sistema include un passaggio di approvazione interattiva dell'utente per confermare che l'ancoraggio sia corretto.

3. Generazione della Specifica Formale:

   • Un generatore di specifiche traduce l'ancoraggio (coordinate, intervalli, indici) e l'operazione in una query di verifica numerica standard ($P_x$).
   • Ad esempio, per l'immagine di un uccello, trasforma "oscura il becco" in un vincolo di robustezza locale: "Per tutte le immagini $x'$ ottenute mascherando la regione del becco rilevata, l'output della rete $N(x')$ deve essere uguale a $N(x)$".
   • Questa query è compatibile con qualsiasi verificatore DNN esistente (es. Marabou, Reluplex, ecc.).

3. Contributi Chiave

1. Identificazione del Gap di Usabilità: Il lavoro evidenzia come la necessità di tradurre manualmente intenti ad alto livello in vincoli a basso livello sia un ostacolo maggiore alla diffusione della verifica formale rispetto alla scalabilità degli algoritmi stessi.
2. Meccanismo di Generazione Automatica: Viene introdotto un framework end-to-end che mappa le specifiche in linguaggio naturale a query formali, supportando domini strutturati (tabulari) e non strutturati (immagini, audio) senza modificare i backend di verifica.
3. Riuso di Componenti Esistenti: L'approccio si basa su una composizione modulare di modelli LLM e di percezione già esistenti, dimostrando che l'integrazione di queste tecnologie mature può abilitare nuovi flussi di lavoro di verifica.

4. Risultati Sperimentali

Gli autori hanno valutato il framework su due benchmark principali:

• Dati Tabulari (Statlog - Credit Scoring): Verifica di vincoli legali/etici (es. limiti di età).
• Classificazione di Immagini (CUB-200-2011 - Uccelli): Verifica di robustezza semantica (es. occlusione di parti specifiche dell'uccello).

Risultati Quantitativi:

• Parsing: I modelli LLM (GPT-5 Mini e Gemini 3 Flash) hanno mostrato un'accuratezza molto elevata nel decomporre le specifiche (tra l'85% e il 100% per l'identificazione di oggetti e azioni).
• Grounding (Rilevamento): La fase di localizzazione degli oggetti è più complessa. Con Grounding DINO, l'accuratezza per una singola configurazione è stata del 55%, ma la tasso di successo complessivo (considerando che almeno una configurazione tra diverse modalità di "tightness" abbia trovato l'oggetto corretto) ha raggiunto l'83%.
• Efficienza: Il processo di traduzione introduce un overhead computazionale basso, rendendo il flusso di lavoro praticabile.

Risultati Qualitativi:
Il sistema è riuscito a gestire richieste complesse come "La previsione cambia se le spine viola in basso sono più rumorose?", traducendo correttamente il concetto semantico e spaziale in un vincolo di perturbazione locale specifico per quella regione dell'immagine, cosa impossibile per i verificatori tradizionali senza intervento manuale.

5. Significato e Impatto

Questo lavoro rappresenta un passo fondamentale verso l'adozione pratica della verifica formale delle DNN in scenari reali:

• Democratizzazione: Permette a utenti non esperti di definire requisiti di sicurezza complessi in linguaggio naturale.
• Estensibilità: Il framework è agnostico rispetto al verificatore sottostante; qualsiasi miglioramento nei modelli di linguaggio o di percezione si traduce immediatamente in una migliore capacità di ancoraggio delle specifiche.
• Versatilità: Estende la verifica formale da semplici vincoli numerici a specifiche semantiche ad alto livello, coprendo domini critici come la guida autonoma (oggetti rilevanti), la medicina (caratteristiche specifiche) e il controllo industriale.

In sintesi, gli autori dimostrano che è possibile rendere la verifica formale delle reti neurali accessibile e applicabile a requisiti del mondo reale, trasformando l'intento umano in garanzie matematiche rigorose attraverso un'interfaccia di traduzione automatica.