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

Technische Samenvatting: Range-Arithmetic – Verifieerbare Deep Learning Inferentie bij een Onbetrouwbare Partij

Probleemstelling
Gedecentraliseerde machine learning (ML)-systemen vertrouwen steeds vaker op het uitbesteden van rekenintensieve taken, zoals deep neural network (DNN) inferentie, aan onbetrouwbare externe partijen (provers) om de beperkingen van blockchain te overwinnen. Een cruciale uitdaging in dit paradigma is het waarborgen van de integriteit van deze uitbestede berekeningen zonder dat de verifieerder het gehele proces opnieuw moet uitvoeren, wat vaak evenredig duur is.

Bestaande Verifiable Computing (VC)-technieken kampen met aanzienlijke hindernissen wanneer ze op ML worden toegepast. De meeste VC-schema's werken over eindige velden (finite fields) en zijn beperkt tot rekenkundige operaties (optellingen en vermenigvuldigingen). Echter, standaard ML-berekeningen omvatten niet-rekenkundige operaties, specifiek:

1. Fixed-point afronding: Vereist na matrixvermenigvuldigingen om precisie te beheren en overflow te voorkomen.
2. Niet-lineaire activatiefuncties: Zoals ReLU (Rectified Linear Unit).

Het representeren van deze operaties binnen conventionele VC-frameworks vereist vaak complexe Boolean circuit-encodings, hoogwaardige polynomen of grote vooraf berekende lookup-tabellen. Deze benaderingen introduceren aanzienlijke overhead in de inspanning van de prover, de kosten voor de verifieerder en de communicatiebandbreedte, of falen om essentiële operaties zoals ReLU en afronding simultaan te ondersteunen.

Methodologie: Het Range-Arithmetic Framework
De auteurs stellen Range-Arithmetic voor, een nieuw framework ontworpen om DNN-inferentie efficiënt te verifiëren terwijl de compatibiliteit met finite-field-gebaseerde bewijs-systemen behouden blijft. De kerninnovatie ligt in het transformeren van niet-rekenkundige operaties naar rekenkundige stappen die verifieerbaar zijn via sum-check protocollen en geconcateneerde range proofs, waardoor Boolean encodings en grote lookup-tabellen worden vermeden.

Het framework werkt via de volgende mechanismen:

1. Matrixvermenigvuldiging Verificatie:
   De verificatie van matrixvermenigvuldiging ($C = AB$) wordt geherformuleerd als een sum-check probleem. Door matrixelementen te representeren als Multilineaire Extensies (MLE's) over een eindig veld, wordt de correctheid van het product gereduceerd tot het verifiëren van een polynoomidentiteit. De auteurs maken gebruik van de Schwartz-Zippel lemma om deze identiteit op willekeurige punten te controleren, waarbij het sum-check protocol de communicatiecomplexiteit reduceert tot $O(\log n)$.

2. Afrondingsverificatie:
   Om de afrondingsoperatie $R(x)$ te verifiëren die na vermenigvuldiging wordt toegepast, deconstrueren de auteurs het proces in rekenkundige constraints. Ze definiëren het weggegooide deel van de afronding ($E$) en de teller van het afrondingsfractie ($D$). Correctheid wordt gewaarborgd door twee condities te bewijzen via geaggregeerde range proofs:

   • De weggegooide bits liggen binnen een specifiek klein interval ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • De resterende waarde is een geheel getal veelvoud van $2^s$ zonder wrap-around.
     Deze benadering maakt het mogelijk om afronding te verifiëren met standaard range proofs zonder dat grote eindige velden nodig zijn om overflow te voorkomen.

3. ReLU Verificatie:
   De ReLU-functie, gedefinieerd als $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, wordt geverifieerd door:

   • Te bewijzen dat de absolute waarde $Y = |A|$ niet-negatief is met behulp van een range proof.
   • Te bewijzen dat $a_i^2 = y_i^2$ voor alle elementen met behulp van een sum-check protocol op de polynoom $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • Het verifiëren van de uiteindelijke lineaire combinatie $B = (A + Y)/2$.

4. Compositie:
   Het framework behandelt neurale netwerk-inferentie als een sequentie van lagen. Elke laag (matrixvermenigvuldiging met afronding of ReLU-activatie) wordt onafhankelijk geverifieerd. De output-commitment van één laag dient als de input voor de volgende, wat de modulaire compositie van verificatie-algoritmen mogelijk maakt zonder de grote tussenliggende matrices opnieuw te verzenden.

Belangrijkste Bijdragen
Het artikel claimt de volgende specifieke bijdragen:

• Unified Framework: Range-Arithmetic is de eerste methode die simultaan $O(n^3)$ prover-complexiteit, $O(n^2)$ verifieerder-complexiteit en $O(\log n)$ communicatie-complexiteit bereikt terwijl het zowel fixed-point afronding als ReLU ondersteunt.
• Eliminatie van Overhead: De aanpak vermijdt de noodzaak voor Boolean circuit-encodings, grote eindige velden (om overflow te voorkomen) en grote vooraf berekende lookup-tabellen, wat gebruikelijk is in eerdere werken.
• Geen Preprocessing: In tegenstelling tot R1CS-gebaseerde of arithmetic circuit-benaderingen, vereist de methode geen preprocessing of encoding-overhead.
• Practicaliteit: Door niet de noodzaak te hebben om het eindige veld te vergroten om overflow te voorkomen, blijft het schema praktisch voor cryptografisch gepaste priemgetallen.

Experimentele Resultaten
De auteurs evalueerden het voorgestelde algoritme op een lineair neuraal netwerk en een casestudy bestaande uit een vierlaags volledig verbonden netwerk (fully connected network) getraind op de MNIST-dataset (met gebruik van 6 integer en 8 fractionele bits).

• Prestatievergelijking: Vergeleken met de state-of-the-art methode [20] (die geen ReLU-ondersteuning heeft en veldvergroting vereist), vertoonde Range-Arithmetic een superieure prestatie naarmate het aantal netwerklagen toenam.
• Metrieken: De voorgestelde methode verminderde de computationele kosten voor zowel de prover als de verifieerder en verlaagde de communicatie-overhead.
• Specificaties: In de MNIST casestudy was de prover-runtime ongeveer 230 milliseconden en de verifieerder-runtime ongeveer 154 milliseconden.
• Schaalbaarheid: Naarmate de matrixgroottes toenamen, groeide de communicatiekosten logaritmisch, terwijl de prover- en verifieerder-runtimes polynomiaal schaalden.

Betekenis en Claims
Het artikel positioneert Range-Arithmetic als een methode die de "meest gebalanceerde afweging" biedt tussen prover-inspanning, verifieerder-kosten, communicatie en feature-volledigheid voor verifieerbare DNN-inferentie bij onbetrouwbare partijen. De auteurs benadrukken dat hoewel lookup-gebaseerde methoden sneller kunnen zijn voor pure ReLU-verificatie, hun vereiste voor grote hulp-tabellen hen onpraktisch maakt voor hulpbron-beperkte verifieerders. Range-Arithmetic vervangt deze tabellen door lichtgewicht range proofs, wat een algemenere en efficiëntere oplossing biedt voor de specifieke beperkingen van gedecentraliseerde ML-systemen. Het werk beoogt vertrouwenswaardige en autonome AI-toepassingen in open, dynamische omgevingen te faciliteren door efficiënte verificatie van complexe, niet-rekenkundige ML-operaties mogelijk te maken zonder heruitvoering.