Riepilogo Tecnico: Verifica Formale delle Reti Neurali Analogiche in Presenza di Variazioni di Processo mediante Zonoetopi Polinomiali

Enunciato del Problema

Le reti neurali analogiche (ANN) offrono vantaggi significativi in termini di consumo energetico, velocità di elaborazione e area del chip rispetto alle controparti digitali, rendendole ideali per applicazioni Internet of Things (IoT) vincolate dall'energia. Tuttavia, in quanto circuiti fisici, le ANN sono altamente suscettibili alle variazioni del processo di fabbricazione (ad esempio, larghezza del gate, tensione di soglia, spessore dell'ossido). Queste variazioni causano deviazioni rispetto al modello nominale, potenzialmente compromettendo la sicurezza e l'accuratezza della rete.

I metodi di verifica tradizionali si basano su simulazioni Monte Carlo, estremamente dispendiose in termini di tempo, per convalidare la funzionalità del circuito in presenza di tali variazioni. Per reti complesse, come le Reti Neurali Convoluzionali (CNN), queste simulazioni possono richiedere giorni per completarsi, creando un collo di bottiglia nel ciclo di progettazione. Inoltre, gli approcci di modellazione esistenti spesso non riescono a catturare il comportamento completo a livello di sistema o mancano di scalabilità attraverso diverse architetture di rete.

Metodologia

Gli autori propongono un framework di verifica formale che sostituisce le simulazioni Monte Carlo con un'analisi di raggiungibilità basata su insiemi utilizzando zonoetopi polinomiali. La metodologia consta di tre fasi principali:

1. Analisi di Sensibilità e Riduzione dei Parametri

Gli autori hanno analizzato un circuito di neurone analogico CMOS da 130 nm utilizzando il modello di transistor PSP. Attraverso un'analisi di sensibilità di oltre 50 parametri di processo, hanno identificato che solo due parametri dominanti ($\phi_1$ e $\phi_2$), che influenzano il potenziale di superficie dei transistor NMOS, impattano significativamente sulle prestazioni del circuito. È stato riscontrato che gli altri parametri hanno effetti trascurabili o sono mitigati dalla topologia del circuito (ad esempio, specchi di corrente).

2. Modellazione Parametrica Basata su Polinomi

Invece di simulare la fisica completa del circuito per ogni variazione, gli autori hanno derivato un modello polinomiale per astrarre il comportamento del neurone.

• Modellazione dei Pesi: I pesi ($\tilde{W}_k$) sono modellati come polinomi di terzo ordine dei parametri dominanti $\phi_1$ e $\phi_2$.
• Bias e Rumore: I termini di bias sono considerati trascurabili, mentre le rimanenti variazioni minori sono catturate da un singolo simbolo di rumore di terzo ordine ($d_3$).
• Formulazione: Il comportamento della rete è espresso come funzione di questi parametri, permettendo ai pesi di essere rappresentati come insiemi piuttosto che valori fissi. Nello specifico, i pesi sono modellati come:
  $$\tilde{W}_k = \sum_{i=0}^{3} \sum_{j=0}^{3} A_{k,i,j} \phi_1^i \phi_2^j + d_3$$
  dove i coefficienti sono determinati tramite regressione polinomiale sui dati Monte Carlo per ogni peso quantizzato.

3. Analisi di Raggiungibilità con Zonoetopi Polinomiali

Il processo di verifica propaga gli insiemi di input attraverso la rete utilizzando zonoetopi polinomiali, una rappresentazione di insiemi capace di gestire le dipendenze tra le variabili.

• Propagazione dell'Insieme: L'insieme di input è propagato strato per strato. Gli strati lineari coinvolgono la moltiplicazione di matrici con gli insiemi di pesi polinomiali.
• Gestione della Non Linearità: Le funzioni di attivazione ReLU sono racchiuse utilizzando tecniche standard per il calcolo basato su insiemi.
• Verifica: L'insieme di output finale è racchiuso. Se questo involucro non interseca l'insieme degli output "non sicuri" (ad esempio, i confini di classificazione errata), la rete è formalmente verificata come sicura per il range di variazione specificato (ad esempio, $\pm 3\sigma$).

Contributi Chiave

1. Modello Polinomiale Ottimizzato: Un modello parametrico che astrae con precisione le prestazioni del neurone analogico in presenza di variazioni di processo utilizzando solo due parametri dominanti e un termine di rumore, riducendo la complessità mantenendo l'accuratezza.
2. Verifica Formale a Livello di Sistema: L'applicazione dell'analisi di raggiungibilità con zonoetopi polinomiali per verificare modelli a livello di circuito in presenza di variazioni di processo, evitando la necessità di simulazioni Monte Carlo esaustive.
3. Scalabilità: L'approccio è dimostrato essere scalabile attraverso diverse architetture, incluse le reti neurali completamente connesse e convoluzionali (CNN).
4. Efficienza: Il metodo riduce drasticamente il tempo di verifica racchiudendo allo stesso tempo un'alta percentuale di campioni di variazione.

Risultati Sperimentali

L'approccio è stato valutato su tre dataset: Wisconsin Breast Cancer, Iris e MNIST (sia architetture completamente connesse che CNN).

• Tempo di Verifica: Il metodo proposto ha ridotto il tempo di verifica da giorni a secondi.
  • CNN MNIST: La simulazione Monte Carlo con Cadence ha richiesto circa 29.592 secondi (circa 8,2 ore); l'approccio proposto ha richiesto 3,37 secondi.
  • Iris: La simulazione ha richiesto circa 865 secondi; l'approccio proposto ha richiesto 1,15 secondi.
• Accuratezza dell'Involucro: L'involucro dello zonoetopo polinomiale ha catturato con successo circa il 99% dei campioni di variazione Monte Carlo su tutti i dataset (variando dal 97,77% al 99,51%).
• Necessità del Modello: Uno studio di ablazione che confrontava gli zonoetopi polinomiali con gli zonoetopi standard (rilassamenti lineari) ha dimostrato che i modelli lineari erano insufficienti. Gli zonoetopi standard producevano involucri che attraversavano i confini decisionali, fallendo nel verificare la sicurezza, mentre gli zonoetopi polinomiali fornivano involucri stretti che verificavano con successo le specifiche.

Significato e Affermazioni

Il documento afferma che il suo significato principale risiede nel consentire la verifica formale delle reti neurali analogiche in presenza di variazioni di processo in un lasso di tempo computazionalmente fattibile. Spostandosi dalla simulazione statistica (Monte Carlo) all'analisi deterministica basata su insiemi, gli autori abilitano:

• Cicli di Progettazione Rapidi: I progettisti possono valutare rapidamente la robustezza dei circuiti analogici contro le variazioni di fabbricazione senza attendere giorni di simulazione.
• Garanzie di Sicurezza: Il metodo fornisce garanzie formali che la rete funzionerà correttamente entro un range di variazione specificato (ad esempio, il 99% dei campioni), aspetto critico per applicazioni IoT safety-critical.
• Valutazione della Robustezza: L'approccio consente di quantificare quanti circuiti fabbricati potrebbero essere difettosi (ad esempio, identificando che i circuiti che deviano oltre $2\sigma$ potrebbero perdere accuratezza), guidando la necessità di progetti di circuiti più robusti.

Gli autori notano che, sebbene i modelli attuali siano relativamente piccoli, questo è un limite della robustezza fisica dei circuiti analogici piuttosto che del metodo di verifica stesso. Concludono che questo approccio può accelerare significativamente il ciclo di progettazione per circuiti di inferenza analogici più grandi e robusti.