Riepilogo Tecnico: VNN-LIB 2.0: Fondamenti Rigorosi per la Verifica delle Reti Neurali

Enunciato del Problema

La comunità di verifica delle reti neurali ha fatto sempre più affidamento sullo standard VNN-LIB (Versione 1.0) per facilitare l'interoperabilità tra solver e strumenti di livello superiore. Tuttavia, la Versione 1.0 presenta quattro carenze critiche che ne impediscono l'uso come fondamento formale rigoroso:

1. Mancanza di Sintassi Formale: La Versione 1.0 non definisce formalmente la sintassi del linguaggio di query, portando a implementazioni reciprocamente incompatibili da parte di diversi solver.
2. Espressività Limitata: Lo standard assume una singola rete con un singolo input e un singolo output. Non supporta nativamente reti multiple, input/outputs multipli o l'accesso a livelli nascosti, costringendo gli utenti a fondere artificialmente i modelli, il che oscura la relazione tra gli artefatti verificati e i modelli distribuiti.
3. Assenza di un Sistema di Tipi: Non esiste alcun meccanismo per specificare i tipi numerici (ad esempio, punto flottante rispetto a valori reali), creando ambiguità e potenziale insoundness quando i solver trattano l'aritmetica a precisione finita come valori reali.
4. Mancanza di Semantica: Lo standard manca di una semantica formale, rendendo impossibile dimostrare formalmente la correttezza di solver, generatori di query o trasformazioni, e ostacolando lo sviluppo di certificati di prova.

Una sfida unica per VNN-LIB, che lo distingue da standard come SMT-LIB, è che le query non sono autonome; specificano proprietà di modelli di reti neurali esterni (tipicamente in formato ONNX). Poiché ONNX stesso manca di una semantica formale e continua a evolversi, definire uno standard VNN-LIB rigoroso richiede di disaccoppiare il linguaggio di query dalle versioni specifiche di ONNX mantenendo al contempo la compatibilità.

Metodologia

Gli autori affrontano queste sfide sviluppando i fondamenti teorici per VNN-LIB 2.0. L'innovazione metodologica centrale è l'introduzione della Teoria delle Reti ($\Psi$).

1. Astrazione della Teoria delle Reti

Gli autori definiscono una "teoria delle reti" come una specifica astratta che cattura la sintassi minima, i giudizi di tipizzazione e la semantica richiesti da un formato di modello di rete neurale per definire VNN-LIB.

• Disaccoppiamento: $\Psi$ agisce come un'interfaccia. Un'implementazione concreta di $\Psi$ (ad esempio, per ONNX v1.20.0) fornisce definizioni specifiche per i tipi di elemento, le rappresentazioni dei tensori, le strutture dei modelli e i riferimenti agli output dei nodi.
• Modularità: VNN-LIB 2.0 è definito rispetto a un $\Psi$ astratto. Ciò consente allo standard di rimanere stabile anche mentre ONNX evolve; solo l'istanziazione di $\Psi$ deve essere aggiornata per le nuove versioni di ONNX, non lo standard VNN-LIB stesso.
• Formalizzazione: L'intero standard, inclusa sintassi, tipizzazione e semantica, è meccanizzato nel dimostratore di teoremi interattivo Agda per garantire la coerenza interna ed escludere ambiguità.

2. Sintassi Formale ed Espressività

Sulla base della teoria delle reti, gli autori definiscono una grammatica formale per VNN-LIB 2.0 che estende significativamente l'espressività:

• Reti Multiple: Le query possono dichiarare reti multiple, supportando scenari come la verifica insegnante-allievo o architetture encoder-decoder.
• Equivalenza di Rete: Lo standard introduce le dichiarazioni equal-to (che fa riferimento allo stesso file di modello esatto) e isomorphic-to (che fa riferimento a modelli con la stessa struttura del grafo ma potenzialmente pesi diversi). Ciò consente ai solver di condividere deduzioni (ad esempio, limiti delle variabili) tra copie di rete.
• Nodi Nascosti: La costruzione declare-hidden consente vincoli sugli output dei livelli intermedi, essenziali per il ragionamento su codifiche o meccanismi di attenzione.
• I/O Multidimensionali: Supporto per numeri arbitrari di input e output, adattandosi a reti multimodali.

3. Sistema di Tipi e Semantica

• Tipizzazione: Un sistema di tipi formale impone la correttezza numerica. Garantisce che le operazioni aritmetiche e i confronti siano eseguiti su tipi compatibili (ad esempio, impedendo la mescolanza di float32 e int32 senza regole esplicite di coercizione). Il sistema di tipi si basa sui giudizi forniti dalla teoria delle reti sottostante $\Psi$.
• Semantica: La semantica di una query è definita come un problema di soddisfacibilità matematica. Dato un insieme di modelli $M$ (istanziati da $\Psi$) e un'assegnazione di input $X$, la semantica determina se esiste un'assegnazione in cui tutte le asserzioni valutano vero.
• Query a Valori Reali: Per accogliere i solver esistenti che trattano i modelli come funzioni su numeri reali ($\mathbb{R}$), lo standard introduce un meccanismo per le "query a valori reali". Utilizzando un tipo distinto real, l'autore della query autorizza esplicitamente il solver a interpretare i modelli su $\mathbb{R}$, riconoscendo la potenziale insoundness dovuta all'imprecisione del punto flottante. Ciò è ottenuto costruendo una specifica teoria delle reti $\Psi_{\mathbb{R}}$ derivata dalla teoria di base.

Contributi Chiave

1. Teoria delle Reti ($\Psi$): L'introduzione di una nuova astrazione che definisce l'interfaccia semantica minima richiesta da un formato di modello, consentendo a VNN-LIB di essere definito indipendentemente da versioni specifiche di ONNX.
2. Sintassi e Grammatica Formali: Una grammatica libera dal contesto precisa per VNN-LIB 2.0 che supporta reti multiple, livelli nascosti e strutture complesse di input/output.
3. Sistema di Tipi Formale: Un sistema di tipizzazione che impone la correttezza del tipo numerico rispetto alla teoria delle reti, affrontando l'ambiguità nelle rappresentazioni numeriche.
4. Semantica Formale: Una definizione matematica rigorosa della semantica delle query parametrizzata dalla teoria delle reti, che consente prove formali di correttezza per gli strumenti che consumano o generano VNN-LIB.
5. Meccanizzazione: L'intero standard è formalizzato in Agda, fornendo un'implementazione di riferimento canonica e una base per prove verificate automaticamente.
6. Estensione a Valori Reali: Un approccio modulare per supportare analisi a valori reali tramite una teoria delle reti derivata, bilanciando la necessità di correttezza con la realtà delle capacità attuali dei solver.

Risultati e Validazione

• Coerenza Interna: La formalizzazione in Agda valida la coerenza interna della sintassi, della tipizzazione e della semantica, assicurando che lo standard sia privo delle ambiguità presenti nella Versione 1.0.
• Dimostrazione di Espressività: Il documento dimostra come una semplice trasformazione della teoria delle reti $\Psi$ produca un'istanza completa per query a valori reali, mostrando la flessibilità dell'astrazione.
• Adozione da Parte della Comunità: Lo standard ha ricevuto feedback positivi dalla comunità di verifica. I principali team di solver si sono impegnati a supportare VNN-LIB 2.0 e il nuovo standard è programmato per essere utilizzato nella competizione VNN-COMP 2026.
• Supporto Strumentale: Gli autori hanno rilasciato una libreria C++ ad alte prestazioni (con binding per Python e Julia) che implementa un parser e un controllore di tipi conformi al nuovo standard, insieme alla formalizzazione in Agda.

Significato

Il documento afferma che VNN-LIB 2.0 fornisce fondamenti robusti e rigorosi per una verifica affidabile delle reti neurali. Il suo significato risiede in due aree complementari:

1. Interoperabilità Pratica: Estendendo l'espressività (reti multiple, nodi nascosti) e standardizzando la sintassi, consente alla comunità di specificare e verificare proprietà più ricche in modo unificato, facilitando migliori benchmark e confronti tra strumenti.
2. Rigor Teorico: Fornendo semantica formale e un sistema di tipi, stabilisce un "contratto rigoroso" tra strumenti e solver. Ciò consente la verifica formale degli strumenti stessi (solver, ottimizzatori, controllori di prova) e risolve questioni sottili riguardanti la correttezza numerica (ad esempio, distinguendo tra semantica a valori reali e a punto flottante).

Gli autori sottolineano che, sebbene il lavoro sia teorico, ha conseguenze concrete: garantisce un'interpretazione inequivocabile delle query, fornisce il linguaggio per risolvere problemi tecnici e getta le basi per certificati di prova formalmente verificati in futuro.