\texttt{Range-Arithmetic}: Verifiable Deep Learning Inference on an Untrusted Party

Sintesi Tecnica: Range-Arithmetic – Inferenza di Deep Learning Verificabile su una Parte Non Fidata

Problematica
I sistemi di apprendimento automatico (ML) decentralizzati si affidano sempre più all'esternalizzazione di compiti ad alta intensità di risorse, come l'inferenza di reti neurali profonde (DNN), a parti esterne non fidate (prover) per superare i limiti della blockchain. Una sfida critica in questo paradigma è garantire l'integrità di tali computazioni esternalizzate senza richiedere al verificatore di rieseguire l'intero processo, il che è spesso proibitivo in termini di costi.

Le tecniche esistenti di Calcolo Verificabile (VC) affrontano ostacoli significativi quando applicate al ML. La maggior parte degli schemi VC opera su campi finiti ed è limitata alle operazioni aritmetiche (addizioni e moltiplicazioni). Tuttavia, le computazioni standard del ML coinvolgono operazioni non aritmetiche, nello specifico:

1. Arrotondamento a virgola fissa: Necessario dopo le moltiplicazioni tra matrici per gestire la precisione e prevenire l'overflow.
2. Funzioni di attivazione non lineari: Come ReLU (Rectified Linear Unit).

Rappresentare queste operazioni all'interno dei convenzionali framework VC richiede spesso complessi codifiche di circuiti booleani, polinomi di alto grado o grandi tabelle di lookup precomputate. Tali approcci introducono un overhead sostanziale nello sforzo del prover, nel costo del verificatore e nella larghezza di banda di comunicazione, oppure non riescono a supportare simultaneamente operazioni essenziali come ReLU e l'arrotondamento.

Metodologia: Il Framework Range-Arithmetic
Gli autori propongono Range-Arithmetic, un nuovo framework progettato per verificare l'inferenza di DNN in modo efficiente mantenendo la compatibilità con i sistemi di prova basati su campi finiti. L'innovazione principale risiede nella trasformazione delle operazioni non aritmetiche in passaggi aritmetici verificabili tramite protocolli sum-check e prove di intervallo (range proofs) concatenate, evitando così le codifiche booleane e le grandi tabelle di lookup.

Il framework opera attraverso i seguenti meccanismi:

1. Verifica della Moltiplicazione tra Matrici:
   La verifica della moltiplicazione tra matrici ($C = AB$) è riformulata come un problema di sum-check. Rappresentando gli elementi della matrice come Estensioni Multilineari (MLE) su un campo finito, la correttezza del prodotto viene ridotta alla verifica di un'identità polinomiale. Gli autori utilizzano il lemma di Schwartz-Zippel per controllare questa identità in punti casuali, impiegando il protocollo sum-check per ridurre la complessità di comunicazione a $O(\log n)$.

2. Verifica dell'Arrotondamento:
   Per verificare l'operazione di arrotondamento $R(x)$ applicata dopo la moltiplicazione, gli autori decompongono il processo in vincoli aritmetici. Definiscono la parte scartata dell'arrotondamento ($E$) e il numeratore della frazione di arrotondamento ($D$). La correttezza è garantita provando due condizioni tramite prove di intervallo aggregate:

   • I bit scartati rientrano in un intervallo specifico molto piccolo ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • Il valore rimanente è un multiplo intero di $2^s$ senza wrap-around.
     Questo approccio consente di verificare l'arrotondamento utilizzando standard range proofs senza richiedere grandi campi finiti per prevenire l'overflow.

3. Verifica di ReLU:
   La funzione ReLU, definita come $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, viene verificata:

   • Provando che il valore assoluto $Y = |A|$ è non negativo utilizzando una range proof.
   • Provando che $a_i^2 = y_i^2$ per tutti gli elementi utilizzando un protocollo sum-check sul polinomio $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • Verificando la combinazione lineare finale $B = (A + Y)/2$.

4. Composizione:
   Il framework tratta l'inferenza di una rete neurale come una sequenza di strati. Ogni strato (moltiplicazione tra matrici con arrotondamento o attivazione ReLU) viene verificato indipendentemente. L'output commitment di uno strato funge da input per il successivo, consentendo la composizione modulare degli algoritmi di verifica senza ritrasmettere grandi matrici intermedie.

Contributi Chiave
Il documento rivendica i seguenti contributi specifici:

• Framework Unificato: Range-Arithmetic è il primo metodo che riesce simultaneamente a raggiungere una complessità del prover di $O(n^3)$, una complessità del verificatore di $O(n^2)$ e una complessità di comunicazione di $O(\log n)$ supportando sia l'arrotondamento a virgola fissa che la funzione ReLU.
• Eliminazione dell'Overhead: L'approccio evita la necessità di codifiche di circuiti booleani, grandi campi finiti (per prevenire l'overflow) e grandi tabelle di lookup precomputate, comuni nei lavori precedenti.
• Nessun Preprocessing: A differenza degli approcci basati su R1CS o circuiti aritmetici, il metodo non richiede alcun overhead di preprocessing o codifica.
• Praticità: Non richiedendo l'ingrandimento del campo finito per evitare l'overflow, lo schema rimane pratico per numeri primi di dimensioni crittografiche.

Risultati Sperimentali
Gli autori hanno valutato l'algoritmo proposto su una rete neurale lineare e su un caso di studio che coinvolge una rete completamente connessa a quattro strati addestrata sul dataset MNIST (utilizzando 6 bit interi e 8 bit frazionari).

• Confronto delle Prestazioni: Rispetto al metodo allo stato dell'arte [20] (che manca del supporto per ReLU e richiede l'ingrandimento del campo), Range-Arithmetic ha dimostrato prestazioni superiori all'aumentare del numero di strati della rete.
• Metriche: Il metodo proposto ha ridotto il costo computazionale sia per il prover che per il verificatore e ha abbassato l'overhead di comunicazione.
• Specifiche: Nel caso di studio MNIST, il tempo di esecuzione del prover è stato di circa 230 millisecondi e il tempo di esecuzione del verificatore di circa 154 millisecondi.
• Scalabilità: All'aumentare delle dimensioni delle matrici, il costo di comunicazione è cresciuto in modo logaritmico, mentre i tempi di esecuzione del prover e del verificatore sono scalati in modo polinomiale.

Significatività e Rivendicazioni
Il documento posiziona Range-Arithmetic come fornitore del "compromesso più equilibrato" tra sforzo del prover, costo del verificatore, comunicazione e completezza delle funzionalità per l'inferenza di DNN verificabile su parti non fidate. Gli autori sottolineano che, sebbene i metodi basati su lookup possano essere più veloci per la pura verifica di ReLU, il loro requisito di grandi tabelle ausiliarie li rende impraticabili per i verificatori con risorse limitate. Range-Arithmetic sostituisce queste tabelle con lightweight range proofs, offrendo una soluzione più generale ed efficiente per i vincoli specifici dei sistemi di ML decentralizzati. Il lavoro mira a facilitare applicazioni di IA affidabili e autonome in ambienti aperti e dinamici, abilitando la verifica efficiente di operazioni di ML complesse e non aritmetiche senza riesecuzione.