Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks

With the increasing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become very important in safety-critical and legal compliance settings. However, model parameters are often commercial secrets that cannot be disclosed to auditors or end users. To this end, we present PANDA, a scalable system that uses Zero-Knowledge Proofs (ZKPs) to prove robustness and fairness properties of a model without revealing private model parameters. PANDA is built on top of CROWN an efficient robustness certification framework that is used in many state-of-the-art formal verification tools for neural networks. The core contribution of PANDA is a novel algorithm for proving linear relaxation bounds on non-linear activation layers, achieving simple and lightweight proofs. Remarkably, our system can generate proofs of local robustness for neural networks with more than 2.9M parameters in about 4 minutes, and can verify them in under 7.5 seconds. Prior ZKP-based robustness systems are based on exponential-time algorithms that cannot scale to nontrivial networks. In contrast, PANDA scales polynomially with the number of neurons in a network, allowing us to support neural networks 3 to 4 orders of magnitude larger than prior works with significantly reduced prover overhead.