Sintesi Tecnica: Verifica di Reti Neurali a Virgola Mobile a Livello Software

Definizione del Problema

Sebbene la verifica delle reti neurali abbia fatto grandi progressi nel fornire garanzie formali per modelli idealizzati a valori reali, questi approcci spesso non tengono conto dei dettagli specifici di implementazione dei sistemi distribuiti. In applicazioni critiche per la sicurezza (ad es., CPS, IoT), le reti neurali sono implementate utilizzando l'aritmetica a virgola mobile a precisione finita (tipicamente IEEE 754 a 32 bit) e si affidano a librerie matematiche standard (ad es., math.h). Questi dettagli di basso livello introducono errori di arrotondamento e comportamenti non associativi che possono invalidare le prove di sicurezza derivate da modelli a precisione infinita. Ad esempio, il documento dimostra che la funzione di attivazione SoftSign, che è non decrescente nell'aritmetica reale, cessa di esserlo quando implementata in virgola mobile a 32 bit.

I tentativi esistenti di verificare il codice delle reti neurali a livello software hanno prodotto risultati contrastanti. I verificatori software spesso faticano a scalare verso grandi istanze di reti neurali, costringendo i professionisti a tornare a modelli unsound a precisione infinita o ad abbandonare la verifica a favore del testing. Inoltre, è stato osservato che gli strumenti esistenti producono risultati errati in determinate configurazioni, mettendo in dubbio la loro affidabilità come oracoli di sicurezza per le implementazioni a virgola mobile. Esiste una mancanza di valutazione rigorosa e standardizzata degli automatismi di verifica software specificamente sul codice delle reti neurali.

Metodologia

Per affrontare queste lacune, gli autori hanno condotto una valutazione rigorosa di otto verificatori automatizzati all'avanguardia sul codice di reti neurali. La metodologia ha previsto tre componenti primarie:

1. Costruzione del Benchmark (NeuroCodeBench 2.0): Gli autori hanno costruito un benchmark completo comprendente 912 esempi di verifica. Questo benchmark copre:

   • Funzioni Matematiche: 58 istanze che testano le proprietà (ad es., monotonia, periodicità, limiti lineari) di funzioni standard di math.h.
   • Funzioni di Attivazione: 57 istanze che testano le proprietà di attivazioni comuni (ad es., ReLU, TanH, SoftSign, GELU).
   • Layer Neurali: 86 istanze che coprono trasformazioni affini, normalizzazione, pooling e layer SoftMax.
   • Reti Neurali Complete: 711 istanze che includono reti di Hopfield, reti ReLU codificate tramite SAT, reti di approssimazione polinomiale, reti con limite di Lipschitz e reti derivate da VNN-COMP (compiti di Densità di Probabilità e Apprendimento per Rinforzo).
   • Ground Truth: Ogni istanza è pre-etichettata come "sicura" o "non sicura" utilizzando tecniche come il testing brute-force, la costruzione esaustiva o la generazione di controesempi, garantendo un verdetto corretto noto per la valutazione.

2. Standardizzazione e Compatibilità: Per garantire un confronto equo e la riproducibilità, gli autori hanno convertito tutte le istanze del benchmark nel formato utilizzato dall'International Competition on Software Verification (SV-COMP). Ciò ha comportato la creazione di file C autonomi che includono l'implementazione del modello, le proprietà di sicurezza e le dipendenze necessarie. Il workflow ha utilizzato il framework BenchExec per gestire i limiti di risorse ed l'esecuzione, assicurando che gli strumenti venissero eseguiti con le stesse configurazioni utilizzate per l'edizione 2024 di SV-COMP.

3. Valutazione Sperimentale: Lo studio ha valutato otto strumenti (2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer) sotto due condizioni:

   • Baseline: Esecuzione dei verificatori sulle istanze semplici del benchmark.
   • Modelli Operativi: Fornitura di implementazioni C esplicite della libreria math.h (utilizzando MUSL e CORE-MATH) per vedere se la fornitura delle definizioni delle funzioni migliora gli esiti della verifica.
   • Analisi Storica: Gli autori hanno anche analizzato le prestazioni storiche di uno strumento (ESBMC) dal 2018 al 2026 per osservare le tendenze nel campo.

Contributi Chiave

• NeuroCodeBench 2.0: La creazione di un benchmark su larga scala, con ground truth, specificamente progettato per la verifica a livello software di reti neurali a virgola mobile. Include 912 istanze che spaziano da funzioni semplici a intere reti con fino a 170K parametri.
• Integrazione SV-COMP: Il benchmark è stato formattato per essere compatibile con l'infrastruttura SV-COMP, rendendolo parte del set di benchmark ufficiale per l'edizione 2026. Ciò consente una valutazione automatizzata e riproducibile utilizzando configurazioni standard degli strumenti.
• Valutazione Rigorosa: Il primo studio sistematico che confronta otto verificatori software all'avanguardia sul codice di reti neurali, rivelando una significativa varianza nelle prestazioni e nella correttezza.
• Analisi dei Modelli Operativi: Un'indagine su quanto la fornitura di implementazioni esplicite delle librerie matematiche (MUSL, CORE-MATH) migliori le prestazioni del verificatore, riscontrando che l'impatto è dipendente dallo strumento e spesso trascurabile o negativo.

Risultati

La valutazione ha prodotto diverse scoperte critiche riguardanti lo stato attuale della verifica del software per le reti neurali:

• Bassa Correttezza e Scalabilità: I risultati sono stati descritti come "piuttosto deludenti". Gli strumenti hanno mostrato una grande varianza attraverso il benchmark, con il miglior strumento (CBMC) che risolveva correttamente 371 istanze su 912, mentre altri ne risolvevano significativamente meno. Il tasso medio di risoluzione tra le categorie variava, con alcune categorie complesse (ad es., Reinforcement Learning) che vedevano tassi di risoluzione così bassi come il 3%. La maggior parte degli strumenti non è riuscita a verificare più di un singolo layer alla volta.
• Verdetto Errato: Diversi strumenti hanno prodotto un alto tasso di risultati errati. Ad esempio, CBMC ha prodotto quasi il 25% di verdeti definitivi errati (prevalentemente falsi positivi), e anche Pinaka e UAutomizer hanno mostrato tassi di errore significativi. Solo ESBMC non ha prodotto verdeti errati tra gli strumenti che hanno risolto un numero sostanziale di istanze.
• Impatto dei Modelli Operativi: La fornitura di implementazioni esplicite di math.h (MUSL o CORE-MATH) non ha portato a miglioramenti visibili complessivamente. Per alcuni strumenti (CBMC, ESBMC, Pinaka), le prestazioni sono effettivamente diminuite a causa della maggiore complessità della verifica del codice della libreria. Per altri (CPAChecker, PeSCo), il numero di istanze risolte è aumentato, ma ciò è spesso avvenuto con un aumento dei verdeti errati.
• Limiti di Scalabilità: Gli strumenti hanno incontrato grandi difficoltà con le reti neurali complete. Il tasso di risoluzione è sceso a singole cifre per categorie complesse come Reinforcement Learning e Probability Density. Anche per le reti sintetiche, strumenti come ESBMC potevano risolvere solo istanze con larghezze molto piccole (ad es., larghezza 4) prima di andare in timeout.
• Progresso Storico: L'analisi di ESBMC dal 2018 al 2026 ha mostrato miglioramenti non monotoni ma generalmente costanti. Un picco notevole di verdeti errati nel 2022-2023 è stato attribuito a un errore di implementazione in un algoritmo di k-induzione, che è stato corretto dopo il rilascio del precedente NeuroCodeBench 1.0. L'introduzione di NeuroCodeBench 1.0 nel 2024 ha portato a una drastica riduzione dei verdeti errati in tutta la comunità, sebbene l'impatto di NeuroCodeBench 2.0 (fine 2025) sia stato più moderato.

Significato e Rivendicazioni

Il documento sostiene che, sebbene la verifica delle reti neurali a livello software sia concettualmente fattibile, gli attuali verificatori software all'avanguardia non sono ancora pronti per gestire questo compito in modo efficace. Lo studio evidenzia che gli strumenti attuali non possono verificare in modo affidabile più di un singolo layer, restituiscono frequentemente risultati errati e mancano di un supporto completo per le librerie matematiche standard.

Gli autori sostengono che il loro lavoro serva come necessario "controllo di realtà" per la comunità di verifica. Fornendo un benchmark rigoroso con ground truth noto, dimostrano che il divario tra la verifica idealizzata e l'implementazione software è attualmente troppo ampio per essere colmato dagli strumenti esistenti senza miglioramenti significativi. Il documento pone che il rilascio di NeuroCodeBench ha già stimolato il progresso, come dimostrato dalla riduzione dei verdeti errati a seguito del suo rilascio iniziale. Tuttavia, gli autori concludono che la certificazione dell'implementazione completa delle reti neurali contro le deviazioni numeriche del caso peggiore rimane una sfida a lungo termine che richiede il supporto nativo per le librerie matematiche e procedure decisionali personalizzate adattate all'aritmetica a virgola mobile.