Source-linked AI summary
SafetyNets: Verifiable Execution of Deep Neural Networks on an Untrusted Cloud
Zahra Ghodsi, Tianyu Gu, Siddharth Garg
TL;DR
Cloud outsourcing makes neural-network inference cheaper but leaves clients needing assurance that an untrusted server computed the requested model correctly. SafetyNets uses specialized interactive proofs for arithmetic-circuit neural networks, achieving low-cost verification, strong detection of incorrect computations, and high MNIST and TIMIT accuracy.
Problem
Clients outsourcing computationally expensive neural-network inference need assurance that an untrusted cloud has performed the computation correctly.
Method
SafetyNets composes specialized interactive-proof protocols to provide mathematical verification for neural networks representable as arithmetic circuits.
Results
SafetyNets achieves low-cost verification, detects incorrect server computations with probability vanishingly close to 1, and reaches 99.4% MNIST and 75.22% TIMIT accuracy.
Takeaways & Limitations
SafetyNets enables practical verifiable outsourcing of supported deep-neural-network inference without compromising reported classification accuracy.
Takeaways & Limitations
SafetyNets cannot catch inherent model misclassifications and is restricted to neural networks with polynomial activations such as quadratic activations in supported layers.
Abstract
from arXiv · showhide
Inference using deep neural networks is often outsourced to the cloud since it is a computationally demanding task. However, this raises a fundamental issue of trust. How can a client be sure that the cloud has performed inference correctly? A lazy cloud provider might use a simpler but less accurate model to reduce its own computational load, or worse, maliciously modify the inference results sent to the client. We propose SafetyNets, a framework that enables an untrusted server (the cloud) to provide a client with a short mathematical proof of the correctness of inference tasks that they perform on behalf of the client. Specifically, SafetyNets develops and implements a specialized interactive proof (IP) protocol for verifiable execution of a class of deep neural networks, i.e., those that can be represented as arithmetic circuits. Our empirical results on three- and four-layer deep neural networks demonstrate the run-time costs of SafetyNets for both the client and server are low. SafetyNets detects any incorrect computations of the neural network by the untrusted server with high probability, while achieving state-of-the-art accuracy on the MNIST digit recognition (99.4%) and TIMIT speech recognition tasks (75.22%).
1 Introduction
SafetyNets addresses the integrity risks of outsourcing neural-network inference by using interactive proofs to verify computation on an untrusted cloud. Its evaluations indicate low verification and proof-generation costs, strong detection of incorrect computations, and high task accuracy.
- Motivation: Outsourcing neural-network training and inference reduces client computational demands but creates concerns about cloud computation integrity and data privacy.The paper focuses specifically on integrity: whether the cloud performed inference correctly.
- Threat model: A lazy or compromised cloud could substitute a simpler model or maliciously alter results returned to the client.Examples include systematic digit misclassification and unauthorized access decisions in face-recognition authentication.
- Approach: Interactive proofs let a prover provide a mathematical correctness proof, enabling a verifier to reject incorrect results with high probability while accepting correct ones.The verifier sends inputs, receives a purported output, and checks responses across n randomly challenged rounds.
- Contribution: SafetyNets composes specialized activation-layer and matrix-multiplication IP protocols for end-to-end neural-network verification while reducing bandwidth relative to verifying layers separately.The framework targets networks representable as arithmetic circuits over finite fields.
- Results: 8×-80× lower client execution time, less than 5% server proof-generation overhead, and less than 8 KBytes exchanged demonstrate low-cost verification.These empirical results were obtained on MNIST and TIMIT tasks.
- Results: 99.4% MNIST accuracy and 75.22% TIMIT accuracy accompany detection of incorrect server computations with probability vanishingly close to 1.The security guarantee concerns incorrect computations by the server, not errors inherent in the model.
2 Background
SafetyNets builds on interactive proofs and sum-check protocols to verify arithmetic-circuit computations, while restricting neural-network layers to operations representable over finite fields. Its mathematical model covers batched fully connected and convolutional networks with supported activations and pooling.
- Interactive Proof Systems: Interactive-proof systems use sum-check protocols to verify claims about computations, with the verifier progressively checking randomized polynomial assertions.The final claim is checked by evaluating the polynomial directly; incorrect claims are rejected with high probability.
- Interactive Proof Systems: GKR organizes arithmetic-circuit nodes into layers and reduces output assertions backward until the verifier checks an assertion about the circuit inputs.Arithmetic circuits use addition and multiplication over a finite field Fp.
- Neural Networks as Arithmetic Circuits: SafetyNets requires activation functions to be polynomials over Fp, using quadratic activations in hidden layers while excluding ReLU, sigmoid, and softmax except at the output.The paper notes prior work finding quadratic activations have representation power comparable to threshold activations.
- Neural Networks as Arithmetic Circuits: SafetyNets supports sum pooling but not max or stochastic pooling because max and division operations are not easily represented as arithmetic circuits.These restrictions arise from the arithmetic-circuit representation used by the protocol.
- Neural Networks as Arithmetic Circuits: Inference inputs, weights, and intermediate values must lie in a finite-field range, with large primes used because quadratic activations and sum pooling can increase values.Training may still use floating-point inputs and weights before rescaling and quantization for inference.
- Mathematical Model: The model represents each layer using a weight matrix, bias vector, and quadratic or output activation, and it covers fully connected and convolutional layers.Convolutional layers are represented with sparse weight matrices, while successive linear transformations can be combined.
- Mathematical Model: SafetyNets amortizes prover and verifier costs over input batches, rejecting an entire batch if any corresponding output is incorrectly computed.The protocol’s goal is to verify the final network output yL computed by the server.
3 SafetyNets
SafetyNets verifies neural-network inference through a specialized interactive proof protocol for arithmetic-circuit networks, reducing each layer’s computations to checks over multilinear extensions and sum-check protocols. Its finite-field quantization and protocol design target accurate, efficient verification with low communication and strong soundness guarantees.
- Protocol foundation: SafetyNets represents supported neural networks as arithmetic circuits over finite fields and uses multilinear extensions of inputs, weights, and intermediate values.The inference inputs, weights, and intermediate values are converted to finite-field elements; biases are assumed zero for exposition, with incorporation described separately.
- Protocol overview: The verifier checks the final output by receiving zL−1, the input to the final activation, and computing the final activation locally.This avoids applying the interactive proof to the final activation layer, which is not amenable to the protocol because it does not use quadratic activations.
- Matrix multiplication: Matrix-multiplication checks use sum-check to verify ˜Zi(qi, ri) through assertions about the weight and preceding activation extensions.The verifier checks the weight extension locally and recursively verifies activation-layer assertions until reaching the network input.
- Efficiency and soundness: The prover’s matrix-multiplication protocol runtime is O(ni(ni−1 + b)), while the verifier’s runtime is O(nini−1) and communication is 4 log(ni) field elements per layer.For activation layers, prover and verifier runtimes are O(bni) and O(log(bni)), respectively, with 5 log(bni) field elements exchanged.
- Quadratic activation: Quadratic activation checks reduce assertions about ˜Yi(si, ri) to assertions about the preceding layer’s ˜Zi−1, which are then verified with the matrix-multiplication protocol.The reduction uses the multilinear extension of the identity matrix and completes the layer-by-layer verification chain.
- Efficiency and soundness: With p = 2^61 − 1, the soundness error is less than 1/2^30 for practical network parameters and batch sizes.Larger primes support larger intermediate values but increase modular-arithmetic costs, so SafetyNets balances field size against quantization accuracy and runtime.
4 Empirical Evaluation
SafetyNets is evaluated on digit and speech recognition tasks, with quadratic-activation networks remaining competitive with ReLU baselines while enabling low-cost verifiable inference. The evaluation reports accuracy, scaling constraints, verification performance, bandwidth, and a rough comparison with homomorphic-encryption-based inference.
- 4.1 Setup: SafetyNets is evaluated on MNIST, MNIST-Back-Rand, and TIMIT using convolutional and fully connected quadratic-activation networks.The MNIST networks use two convolutional layers, while the TIMIT network uses three hidden fully connected layers with quadratic activations.
- 4.2 Classification Accuracy of SafetyNets: Quadratic-activation networks are competitive with ReLU networks on all three tasks and appear to converge faster during training.The faster convergence may be related to larger gradients despite gradient clipping.
- 4.2 Classification Accuracy of SafetyNets: 4.67% test error is obtained on MNIST-Back-Rand with α = β = 16; corresponding test errors are 0.63% for MNIST and 25.7% for TIMIT.Larger scaling factors reduce quantization error but can exceed the representable range for p = 2^61 − 1.
- 4.3 Verifier and Prover Run-times: 8× to 82× faster verifier time is achieved than local FcNN-Quad-3 execution, while proof-generation overhead increases server execution time by only 5%.For batch size 2048, exchanged data is less than 8 KBytes and the soundness error is less than 1/2^30.
- 4.3 Verifier and Prover Run-times: SafetyNets has significantly lower bandwidth costs than separately verifying each neural-network layer with matrix-multiplication protocols.The evaluation also contrasts SafetyNets with CryptoNets, whose reported MNIST client runtime is about 600 seconds versus less than 10 seconds for SafetyNets at batch size 4096.
5 Conclusion
The paper concludes that SafetyNets enables low-cost, provable verification of deep-neural-network inference on untrusted clouds. Its arithmetic-circuit restrictions did not impact accuracy on the evaluated digit and speech recognition tasks.
- 5 Conclusion: SafetyNets provides provable correctness verification for deep-neural-network inference running on untrusted clouds.The framework uses a specialized interactive-proof protocol for networks representable as arithmetic circuits.
- 5 Conclusion: Arithmetic-circuit restrictions did not impact network accuracy on the evaluated digit and speech recognition tasks.The paper identifies applying SafetyNets to deeper networks and extending it to privacy as future work.
Proof of Lemma 3.1
Lemma 3.1 bounds the verifier’s probability of accepting an incorrect computation by aggregating soundness errors from the protocol’s components. The resulting bound is an upper bound on the total soundness error.
- The verifier rejects incorrect computations with probability greater than 1 − ϵ, where ϵ is the protocol’s soundness error.
- The total soundness error combines contributions from multilinear-extension sampling, sum-check, matrix multiplication, and quadratic-activation protocols.
- The summed component errors produce an upper bound on the final soundness error.
Handling Bias Variables
The bias-handling step corrects the zero-bias simplification by incorporating bias variables into the matrix-multiplication assertion. Sum-check then separates the locally checked bias assertion from the assertion passed onward.
- The general layer computation includes a bias term, changing the relation from bmzi = wi.yi to bmzi = wi.yi + bi1T.
- The proof converts an assertion on ˜Zi(qi, ri) into an assertion on the bias-aware extension ˜Z′i.
- Sum-check yields a locally checked assertion on ˜Bi while forwarding ˜Z′i to the matrix-multiplication IP protocol.