Sintesi Tecnica: Le Reti Neurali a Virgola Mobile sono Approssimatori Universali Provabilmente Robusti

1. Definizione del Problema

Il classico teorema di Approssimazione Universale (UA) e il più recente teorema di Approssimazione Universale ad Intervalli (IUA) stabiliscono che le reti neurali possono approssimare funzioni continue e le loro mappe di immagine diretta (intervalli) con un'accuratezza arbitraria. Tuttavia, questi risultati teorici si basano sull'assunzione irrealistica che le reti neurali operino su numeri reali dotati di precisione infinita. In pratica, le implementazioni software utilizzano l'aritmetica a virgola mobile a precisione finita, il che introduce discretizzazione, limitazione (boundedness), errori di arrotondamento e potenziali overflow/underflow.

La questione centrale aperta affrontata da questo articolo è se il teorema IUA sia valido nell'ambito della virgola mobile. Nello specifico, può una rete neurale a virgola mobile, quando analizzata tramite interpretazione astratta (dominio degli intervalli), catturare perfettamente la mappa di immagine diretta di una funzione target arrotondata? Il lavoro precedente non ha stabilito questo, in gran parte perché gli errori di arrotondamento inerenti alle operazioni in virgola mobile invalidano le tecniche di prova utilizzate per le reti a valori reali (ad esempio, la costruzione di sub-reti specifiche che si affidano all'aritmetica esatta fallisce a causa dell'arrotondamento).

2. Metodologia

Gli autori sviluppano un rigoroso framework teorico per colmare il divario tra la teoria a valori reali e la pratica a virgola mobile.

2.1 Formalizzazione della Semantica della Virgola Mobile

Il documento definisce le reti neurali come funzioni sull'insieme dei numeri a virgola mobile finiti $\mathcal{F}$, utilizzando operazioni conformi allo standard IEEE-754 ($\oplus, \ominus, \otimes$) con la modalità "round to nearest (ties to even)" (arrotondamento al più vicino, pareggio verso il numero pari). La semantica ad intervalli $\nu^\sharp$ è definita su intervalli astratti $\langle a, b \rangle$, che rappresentano l'insieme dei float all'interno di $[a, b]$.

2.2 Condizioni sulle Funzioni di Attivazione

Per dimostrare il teorema, gli autori introducono la Condizione 1, un insieme di vincoli sulla funzione di attivazione $\sigma: \mathcal{F} \to \mathcal{F}$. Queste condizioni garantiscono che la funzione possa:

1. Generare esattamente lo zero e un valore specifico non nullo entro un intervallo limitato.
2. Esibire monotonia o comportamenti di soglia specifici attorno a un valore critico $\eta$.
3. Soddisfare un vincolo di tipo Lipschitz-simile per prevenire una crescita illimitata.

Il documento dimostra che le versioni correttamente arrotondate di comuni funzioni di attivazione (ReLU, GELU, Sigmoid, Tanh, ecc.) soddisfano queste condizioni, spesso sfruttando il Lemma 1, che mappa le proprietà delle funzioni a valori reali ai loro corrispettivi in virgola mobile.

2.3 Strategia di Dimostrazione: Separabilità e Costruzione di Indicatori

Il nucleo della dimostrazione consiste nella costruzione di una rete neurale che agisca come un "approssimatore universale di intervalli". La metodologia procede in due fasi principali:

1. Separabilità: Gli autori definiscono una proprietà chiamata $([a, b]_\mathcal{F}, \eta, K, L_\phi, L_\psi)$-separabilità. Questa proprietà garantisce l'esistenza di reti in grado di implementare funzioni indicatrici scalate (ad esempio, mappando gli input $\le z$ a 0 e gli input $> z$ a $K$) sotto la semantica degli intervalli.

   • La dimostrazione costruisce specifiche sub-reti (ad esempio, $\mu_z$, $\tau_{\theta, \theta'}$) che sfruttano gli errori di arrotondamento per "contrarre" gli intervalli. Ad esempio, una rete è progettata in modo tale che gli input in un determinato intervallo vengano mappati a un intervallo singleton $\langle \eta, \eta \rangle$ o $\langle \eta^+, \eta^+ \rangle$ dopo il passaggio attraverso la funzione di attivazione.
   • Fondamentalmente, la costruzione evita valori infiniti nei livelli intermedi, affrontando i problemi di overflow che affliggono le prove a valori reali quando si scalano i pesi a magnitudini arbitrarie.

2. Composizione per l'Approssimazione Universale: Utilizzando la proprietà di separabilità, gli autori costruiscono reti per:

   • Funzioni indicatrici di box arbitrari.
   • Funzioni indicatrici di sottoinsiemi arbitrari dello spazio di input.
   • Infine, la funzione target stessa, esprimendola come una combinazione lineare in virgola mobile di queste funzioni indicatrici. La dimostrazione gestisce attentamente la sommatoria in virgola mobile per garantire che l'accumulo degli errori di arrotondamento si allinei perfettamente per ricostruire la mappa di immagine della funzione target.

3. Contributi Chiave

3.1 Il Teorema IUA a Virgola Mobile (Teorema 1)

Il documento dimostra che per qualsiasi funzione target $f: \mathbb{R}^d \to \mathbb{R}$ e per una vasta classe di funzioni di attivazione che soddisfano la Condizione 1, esiste una rete neurale a virgola mobile $\nu$ la cui semantica ad intervalli $\nu^\sharp$ calcola esattamente la mappa di immagine diretta della funzione target arrotondata $\hat{f}$ sul dominio $[-1, 1]^d \cap \mathcal{F}^d$.

• Esattezza: A differenza dell'IUA a valori reali che raggiunge un'approssimazione $\delta$, la versione a virgola mobile raggiunge $\delta = 0$ (corrispondenza esatta), poiché il dominio è finito.
• Generalità: Il teorema è valido per funzioni target arbitrarie (non solo continue) e per una vasta gamma di funzioni di attivazione, incluse la funzione identità (che è impossibile nell'IUA a valori reali).

3.2 Esistenza di Reti Provabilmente Robuste (Teorema 2)

Come corollario, il documento dimostra che se esiste un classificatore ideale robusto (anche se non una rete neurale), esiste una rete neurale a virgola mobile che è provabilmente robusta tramite analisi degli intervalli e compie predizioni identiche. Questo risolve la questione se esistano limiti fondamentali all'espressività delle reti neurali provabilmente robuste nell'ambito della virgola mobile: tali limiti non esistono.

3.3 Completezza degli Intervalli a Virgola Mobile (Teorema 3)

Il documento stabilisce un risultato sorprendente riguardante la completezza computazionale: la classe di programmi a virgola mobile a linea retta (straight-line programs) che utilizzano solo l'addizione ($\oplus$) e la moltiplicazione ($\otimes$) è intervallo-completa per la virgola mobile. Ciò significa che tali programmi semplici possono simulare la semantica degli intervalli di qualsiasi programma a virgola mobile terminante che prenda come input float finiti e restituisca float finiti o infiniti. Questo risultato estende il teorema IUA alla funzione di attivazione identità su l'intero dominio $\mathcal{F}^d$.

4. Risultati e Confronti

Il documento evidenzia tre distinzioni fondamentali tra il nuovo teorema IUA a virgola mobile e i precedenti risultati a valori reali:

1. Funzioni Target: L'IUA a valori reali approssima funzioni continue; l'IUA a virgola mobile calcola esattamente l'immagine di qualsiasi funzione target arrotondata (poiché il dominio è finito).
2. Funzioni di Attivazione: L'IUA a valori reali richiede attivazioni "schiacciabili" (non affini); l'IUA a virgola mobile è valido anche per la funzione identità. Questo accade perché le trasformazioni affini in virgola mobile non sono strettamente affini rispetto ai reali a causa degli errori di arrotondamento, permettendo loro di rompere la linearità e approssimare comportamenti non lineari.
3. Approssimazione vs Esattezza: I risultati a valori reali forniscono $\delta$-approssimazioni; i risultati a virgola mobile forniscono corrispondenze esatte per la funzione target arrotondata.

5. Significato e Rivendicazioni

Gli autori affermano che questo lavoro colma il divario teorico tra la verifica della robustezza basata sull'interpretazione astratta e le implementazioni pratiche a virgola mobile.

• Assicurazione Teorica: Dimostra che la mancanza di accuratezza allo stato dell'arte nelle reti neurali provabilmente robuste non è dovuta a un limite fondamentale della loro capacità espressiva, ma probabilmente a sfide di ottimizzazione o agli algoritmi di verifica specifici utilizzati.
• Completezza: Il risultato sulla completezza degli intervalli suggerisce che semplici operazioni aritmetiche sono sufficienti per simulare comportamenti complessi in virgola mobile sotto la semantica degli intervalli, offrendo nuove intuizioni sul potere computazionale dei programmi a virgola mobile.
• Rilevanza Pratica: Validando il teorema IUA per i numeri a virgola mobile, il documento fornisce una base teorica per l'uso dell'analisi degli intervalli in domini critici per la sicurezza (sanità, guida autonoma) dove l'aritmetica a virgola mobile è lo standard.

Il documento dichiara esplicitamente che queste sono dimostrazioni di esistenza; non afferma che gli attuali algoritmi di addestramento possano trovare facilmente tali reti, né propone nuovi metodi di addestramento. Il contributo è strettamente teorico, stabilendo che il "tetto di espressione" per le reti neurali a virgola mobile provabilmente robuste è, di fatto, inesistente.