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

Technical Summary: Range-Arithmetic – Verifiable Deep Learning Inference on an Untrusted Party

Problem Statement
Decentralized machine learning (ML) systems increasingly rely on offloading resource-intensive tasks, such as deep neural network (DNN) inference, to untrusted external parties (provers) to overcome blockchain limitations. A critical challenge in this paradigm is ensuring the integrity of these outsourced computations without requiring the verifier to re-execute the entire process, which is often prohibitively expensive.

Existing Verifiable Computing (VC) techniques face significant hurdles when applied to ML. Most VC schemes operate over finite fields and are restricted to arithmetic operations (additions and multiplications). However, standard ML computations involve non-arithmetic operations, specifically:

1. Fixed-point rounding: Required after matrix multiplications to manage precision and prevent overflow.
2. Non-linear activation functions: Such as ReLU (Rectified Linear Unit).

Representing these operations within conventional VC frameworks often necessitates complex Boolean circuit encodings, high-degree polynomials, or large precomputed lookup tables. These approaches introduce substantial overhead in prover effort, verifier cost, and communication bandwidth, or fail to support essential operations like ReLU and rounding simultaneously.

Methodology: The Range-Arithmetic Framework
The authors propose Range-Arithmetic, a novel framework designed to verify DNN inference efficiently while maintaining compatibility with finite-field-based proof systems. The core innovation lies in transforming non-arithmetic operations into arithmetic steps verifiable via sum-check protocols and concatenated range proofs, thereby avoiding Boolean encodings and large lookup tables.

The framework operates through the following mechanisms:

1. Matrix Multiplication Verification:
   The verification of matrix multiplication ($C = AB$) is reformulated as a sum-check problem. By representing matrix elements as Multilinear Extensions (MLEs) over a finite field, the correctness of the product is reduced to verifying a polynomial identity. The authors utilize the Schwartz-Zippel lemma to check this identity at random points, employing the sum-check protocol to reduce communication complexity to $O(\log n)$.

2. Rounding Verification:
   To verify the rounding operation $R(x)$ applied after multiplication, the authors decompose the process into arithmetic constraints. They define the discarded portion of the rounding ($E$) and the numerator of the rounding fraction ($D$). Correctness is ensured by proving two conditions via aggregated range proofs:

   • The discarded bits lie within a specific small interval ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • The remaining value is an integer multiple of $2^s$ without wrap-around.
     This approach allows rounding to be verified using standard range proofs without requiring large finite fields to prevent overflow.

3. ReLU Verification:
   The ReLU function, defined as $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, is verified by:

   • Proving that the absolute value $Y = |A|$ is non-negative using a range proof.
   • Proving that $a_i^2 = y_i^2$ for all elements using a sum-check protocol on the polynomial $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • Verifying the final linear combination $B = (A + Y)/2$.

4. Composition:
   The framework treats neural network inference as a sequence of layers. Each layer (matrix multiplication with rounding or ReLU activation) is verified independently. The output commitment of one layer serves as the input for the next, allowing the modular composition of verification algorithms without re-transmitting large intermediate matrices.

Key Contributions
The paper claims the following specific contributions:

• Unified Framework: Range-Arithmetic is the first method to simultaneously achieve $O(n^3)$ prover complexity, $O(n^2)$ verifier complexity, and $O(\log n)$ communication complexity while supporting both fixed-point rounding and ReLU.
• Elimination of Overhead: The approach avoids the need for Boolean circuit encodings, large finite fields (to prevent overflow), and large precomputed lookup tables, which are common in prior works.
• No Preprocessing: Unlike R1CS-based or arithmetic circuit approaches, the method requires no preprocessing or encoding overhead.
• Practicality: By not requiring the enlargement of the finite field to avoid overflow, the scheme remains practical for cryptographically sized primes.

Experimental Results
The authors evaluated the proposed algorithm on a linear neural network and a case study involving a four-layer fully connected network trained on the MNIST dataset (using 6 integer and 8 fractional bits).

• Performance Comparison: Compared to the state-of-the-art method [20] (which lacks ReLU support and requires field enlargement), Range-Arithmetic demonstrated superior performance as the number of network layers increased.
• Metrics: The proposed method reduced the computational cost for both the prover and the verifier and lowered communication overhead.
• Specifics: In the MNIST case study, the prover runtime was approximately 230 milliseconds, and the verifier runtime was approximately 154 milliseconds.
• Scalability: As matrix sizes increased, the communication cost grew logarithmically, while prover and verifier runtimes scaled polynomially.

Significance and Claims
The paper positions Range-Arithmetic as providing the "most balanced trade-off" among prover effort, verifier cost, communication, and feature completeness for verifiable DNN inference on untrusted parties. The authors emphasize that while lookup-based methods may be faster for pure ReLU verification, their requirement for large auxiliary tables makes them impractical for resource-constrained verifiers. Range-Arithmetic replaces these tables with lightweight range proofs, offering a more general and efficient solution for the specific constraints of decentralized ML systems. The work aims to facilitate trustworthy and autonomous AI applications in open, dynamic environments by enabling efficient verification of complex, non-arithmetic ML operations without re-execution.