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

Technisches Resümee: Range-Arithmetic – Verifizierbare Deep-Learning-Inferenz auf einer vertrauensunwürdigen Partei

Problemstellung
Dezentralisierte maschinelle Lernsysteme (ML) verlassen sich zunehmend auf die Auslagerung ressourcenintensiver Aufgaben, wie etwa der Deep Neural Network (DNN) Inferenz, an vertrauensunwürdige externe Parteien (Prover), um die Beschränkungen der Blockchain zu überwinden. Eine kritische Herausforderung in diesem Paradigma besteht darin, die Integrität dieser ausgelagerten Berechnungen zu gewährleisten, ohne dass der Verifizierer den gesamten Prozess erneut ausführen muss, was oft prohibititiv teuer ist.

Bestehende Techniken für das Verifiable Computing (VC) stehen bei der Anwendung auf ML vor erheblichen Hürden. Die meisten VC-Schemata operieren über endliche Körper und sind auf arithmetische Operationen (Additionen und Multiplikationen) beschränkt. Standardmäßige ML-Berechnungen beinhalten jedoch nicht-arithmetische Operationen, insbesondere:

1. Fixed-point Rounding (Festkomma-Rundung): Erforderlich nach Matrixmultiplikationen, um die Präzision zu verwalten und Überläufe zu verhindern.
2. Nicht-lineare Aktivierungsfunktionen: Wie etwa ReLU (Rectified Linear Unit).

Die Darstellung dieser Operationen innerhalb konventioneller VC-Frameworks erfordert oft komplexe Boolean-Schaltkreis-Kodierungen, Polynome hohen Grades oder große vorberechnete Lookup-Tabellen. Diese Ansätze führen zu erheblichem Overhead beim Prover-Aufwand, den Verifizierer-Kosten und der Kommunikationsbandbreite, oder sie können wesentliche Operationen wie ReLU und Rundung nicht gleichzeitig unterstützen.

Methodik: Das Range-Arithmetic-Framework
Die Autoren schlagen Range-Arithmetic vor, ein neuartiges Framework, das darauf ausgelegt ist, die DNN-Inferenz effizient zu verifizieren und gleichzeitig die Kompatibilität mit auf endlichen Körpern basierenden Beweissystemen zu wahren. Die zentrale Innovation liegt in der Transformation nicht-arithmetischer Operationen in arithmetische Schritte, die via Sum-Check-Protokollen und konkatinierten Range-Proofs verifizierbar sind, wodurch Boolean-Kodierungen und große Lookup-Tabellen vermieden werden.

Das Framework arbeitet durch folgende Mechanismen:

1. Verifizierung der Matrixmultiplikation:
   Die Verifizierung der Matrixmultiplikation ($C = AB$) wird als Sum-Check-Problem umformuliert. Durch die Darstellung der Matrizenelemente als Multilineare Erweiterungen (MLEs) über einem endlichen Körper wird die Korrektheit des Produkts auf die Verifizierung einer Polynomidentität reduziert. Die Autoren nutzen das Schwartz-Zippel-Lemma, um diese Identität an zufälligen Punkten zu prüfen, wobei das Sum-Check-Protokoll die Kommunikationskomplexität auf $O(\log n)$ reduziert.

2. Verifizierung der Rundung (Rounding):
   Um die nach der Multiplikation angewendete Rundungsoperation $R(x)$ zu verifizieren, zerlegen die Autoren den Prozess in arithmetische Constraints. Sie definieren den verworfenen Teil der Rundung ($E$) und den Zähler des Rundungsbruchs ($D$). Die Korrektheit wird durch die Beweisführung zweier Bedingungen mittels aggregierter Range-Proofs sichergestellt:

   • Die verworfenen Bits liegen innerhalb eines spezifischen kleinen Intervalls ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • Der verbleibende Wert ist ein ganzzahliges Vielfaches von $2^s$ ohne Überlauf (Wrap-around).
     Dieser Ansatz ermöglicht es, die Rundung unter Verwendung von Standard-Range-Proofs zu verifizieren, ohne große endliche Körper zur Vermeidung von Überläufen zu benötigen.

3. ReLU-Verifizierung:
   Die ReLU-Funktion, definiert als $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, wird verifiziert durch:

   • Den Beweis, dass der Absolutwert $Y = |A|$ nicht negativ ist, mittels eines Range-Proofs.
   • Den Beweis, dass $a_i^2 = y_i^2$ für alle Elemente gilt, unter Verwendung eines Sum-Check-Protokolls auf dem Polynom $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • Die Verifizierung der finalen linearen Kombination $B = (A + Y)/2$.

4. Komposition:
   Das Framework behandelt die Inferenz neuronaler Netze als eine Sequenz von Schichten (Layers). Jede Schicht (Matrixmultiplikation mit Rundung oder ReLU-Aktivierung) wird unabhängig verifiziert. Das Output-Commitment einer Schicht dient als Input für die nächste, was die modulare Komposition von Verifizierungsalgorithmen ermöglicht, ohne große Zwischenmatrizen erneut übertragen zu müssen.

Wesentliche Beiträge
Das Paper beansprucht die folgenden spezifischen Beiträge:

• Einheitliches Framework: Range-Arithmetic ist die erste Methode, die gleichzeitig eine Prover-Komplexität von $O(n^3)$, eine Verifizierer-Komplexität von $O(n^2)$ und eine Kommunikationskomplexität von $O(\log n)$ erreicht und dabei sowohl Fixed-point Rounding als auch ReLU unterstützt.
• Eliminierung von Overhead: Der Ansatz vermeidet die Notwendigkeit von Boolean-Schaltkreis-Kodierungen, großen endlichen Körpern (zur Vermeidung von Überläufen) und großen vorberechneten Lookup-Tabellen, die in früheren Arbeiten üblich waren.
• Keine Vorverarbeitung: Im Gegensatz zu R1CS-basierten oder arithmetischen Schaltkreis-Ansätzen erfordert die Methode keine Vorverarbeitungs- oder Kodierungs-Overheads.
• Praktikabilität: Da keine Vergrößerung des endlichen Körpers zur Vermeidung von Überläufen erforderlich ist, bleibt das Schema für kryptographisch dimensionierte Primzahlen praktikabel.

Experimentelle Ergebnisse
Die Autoren evaluierten den vorgeschlagenen Algorithmus an einem linearen neuronalen Netz und einer Fallstudie mit einem vierlagigen Fully Connected Network, das auf dem MNIST-Datensatz trainiert wurde (unter Verwendung von 6 Integer- und 8 Fractional-Bits).

• Leistungsvergleich: Im Vergleich zur State-of-the-Art-Methode [20] (die keine ReLU-Unterstützung bietet und eine Feldvergrößerung erfordert) zeigte Range-Arithmetic eine überlegene Performance, wenn die Anzahl der Netzwerkschichten zunahm.
• Metriken: Die vorgeschlagene Methode reduzierte die Rechenkosten sowohl für den Prover als auch für den Verifizierer und senkte den Kommunikations-Overhead.
• Spezifika: In der MNIST-Fallstudie betrug die Prover-Laufzeit etwa 230 Millisekunden und die Verifizierer-Laufzeit etwa 154 Millisekunden.
• Skalierbarkeit: Mit zunehmender Matrixgröße wuchs die Kommunikationskosten logarithmisch, während die Prover- und Verifizierer-Laufzeiten polynomiell skalierten.

Bedeutung und Ansprüche
Das Paper positioniert Range-Arithmetic als Methode, die den „ausgewogensten Kompromiss“ zwischen Prover-Aufwand, Verifizierer-Kosten, Kommunikation und Feature-Vollständigkeit für die verifizierbare DNN-Inferenz auf vertrauensunwürdigen Parteien bietet. Die Autoren betonen, dass, obwohl Lookup-basierte Methoden für die reine ReLU-Verifizierung schneller sein mögen, deren Anforderung an große Hilfstabellen sie für ressourcenbeschränkte Verifizierer unpraktisch macht. Range-Arithmetic ersetzt diese Tabellen durch leichtgewichtige Range-Proofs und bietet so eine allgemeinere und effizientere Lösung für die spezifischen Anforderungen dezentralisierter ML-Systeme. Die Arbeit zielt darauf ab, vertrauenswürdige und autonome KI-Anwendungen in offenen, dynamischen Umgebungen zu erleichtern, indem sie eine effiziente Verifizierung komplexer, nicht-arithmetischer ML-Operationen ohne Re-Execution ermöglicht.