PaperlayerView exact revision on arXiv

Source-linked AI summary

Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees

Youwei Zhong, Ben Merbaum, Timos Antonopoulos, Ning Luo, Charalampos Papamanthou, Katerina Sotiraki, Ruzica Piskac

arXiv:2608.17070v1cs.LGcs.CRcs.LO

TL;DR

Formal robustness guarantees are increasingly needed for deployed neural networks, but proprietary parameters cannot always be disclosed to auditors or users. PANDA combines zero-knowledge proofs with CROWN to certify private models, supporting networks with up to 2.9 million parameters in five minutes and verification in ten seconds.

  • Problem

    Scalable formal robustness certification is needed for neural networks whose proprietary parameters cannot be disclosed to users or auditors.

  • Method

    PANDA combines zero-knowledge proofs with CROWN and verifies linear activation relaxations using a lightweight four-point constraint gadget.

  • Results

    2.9 million parameters are supported with 5 minutes of proving and 10 seconds of verification, exceeding prior approaches by more than 4 orders of magnitude.

  • Takeaways & Limitations

    PANDA enables publicly verifiable robustness proofs for private neural networks without revealing their model parameters.

  • Takeaways & Limitations

    PANDA proves robustness only for quantized models and publicly discloses the architecture, layer dimensions, and activation function.

Abstract

from arXiv · show

With the growing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become increasingly 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 the robustness and fairness properties of a model without revealing its private 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 for non-linear activation layers, yielding simple, lightweight proofs. Remarkably, our system can generate proofs of local robustness for neural networks with more than 2.9M parameters in 5 minutes, and can verify them in 10 seconds. Prior ZKP-based robustness system rely on exponential-time algorithms that cannot scale to nontrivial networks. In contrast, PANDA scales polynomially in the number of neurons in a network, allowing us to support neural networks 4 orders of magnitude larger than previous approaches with significantly reduced prover overhead.

1 Introduction

PANDA combines zero-knowledge proofs with CROWN to certify local robustness of private neural networks, addressing the tension between verifiability and model confidentiality. It scales to networks with 2.9 million parameters while supporting transcendental activations through lightweight, ZK-friendly verification methods.

  • Motivation: Proprietary model parameters can expose intellectual property, enable white-box attacks, and leak training data, complicating formal robustness verification.These confidentiality concerns are especially relevant as ML systems are deployed in safety-critical settings and regulators or customers demand formal guarantees.
  • PANDA: PANDA combines ZKPs with CROWN to produce publicly verifiable proofs of local robustness without revealing private model parameters.CROWN is an efficient linear bound propagation method underlying many state-of-the-art neural-network verification systems.
  • Scalability: 2.9 million parameters: PANDA supports networks at this scale, exceeding prior approaches by more than 4 orders of magnitude, with 5 minutes proving and 10 seconds verification.The prover runtime is polynomial in the number of neurons, enabling practical certification for substantially larger networks.
  • Novelty: PANDA is the first privacy-preserving local robustness certification system to support transcendental activations such as sigmoid and tanh.Its method verifies linear relaxations over continuous intervals by checking four pointwise inequalities.
  • Technical highlights: PANDA improves efficiency by performing CROWN’s costly bound-selection search outside the ZKP and verifying its correctness without replaying the entire computation trace.A customized backend uses different cryptographic primitives for different operations, improving prover efficiency and scalability.

2 Preliminaries

This section defines zero-knowledge proofs and commit-and-prove systems for certifying public statements using private witnesses, then introduces PANDA’s cryptographic components and quantized finite-field computation. It also explains how polynomial commitments, matrix arithmetic, and lookup arguments support the system’s proofs.

  • Zero-knowledge proofs: A ZKP lets a prover convince a verifier that a public statement is true without revealing the private witness explaining why.For PANDA, the statement may assert local robustness, while the witness contains private model weights and auxiliary computation values.
  • Commit-and-prove ZKPs: Commit-and-prove ZKPs bind a hiding commitment to the witness and prove that the committed witness is valid for the public statement.The commitment reveals nothing about the witness, while binding prevents the prover from substituting a different witness.
  • PANDA primitives: PANDA combines polynomial commitments, matrix-arithmetic proofs, and lookup arguments to prove committed polynomial evaluations, matrix relations, and table membership.Matrix and vector data can be encoded as polynomials, while lookup arguments can establish range constraints and nonlinear function evaluations.
  • Lookup arguments: ΠLOOKUP proves range constraints by using an interval as its table and proves nonlinear evaluations by tabulating pairs (z, f(z)) over the possible domain.One-sided range proofs use a table beginning at 0, with the upper bound determined by quantization.
  • Quantization: Quantization translates real-valued neural-network computations into finite-field arithmetic by representing each real x with a Q-bit integer qx satisfying x · Sx ≈ qx.Addition requires rescaling operands to a common factor, multiplication sets the product scale to SxSy, and rescaling computes qz = ⌊Szqx/Sx⌋.

3 CROWN Algorithm

CROWN certifies neural-network statements by computing layerwise linear bounds and checking the resulting output bound against the target constraint. Its procedure combines an outer forward pass, inner backward passes through activation relaxations and linear maps, and final concretization over the perturbation region.

  • Network model: CROWN models an m-layer feed-forward network with weight matrices, biases, coordinatewise activations, and class scores given by output neurons.The predicted class is the output index maximizing its score on input x0.
  • Certification goal: CROWN certifies constraints C · f(x) ≤ u by computing u′ from linear bounds and checking u′ ≤ u entry-wise.For local robustness, the certified region is an ℓ∞ ball around x0.
  • Forward and backward passes: CROWN builds bounds layer by layer in an outer forward pass, while each layer’s bounds require an inner backward pass to the input.A concretization step then converts the linear bounds into scalar bounds used to derive u′.
  • Final layer: In the final layer, CROWN initializes the backward pass with C · W(m) and C · b(m), bounding C · z(m) rather than z(m).This modification supports the target claim C f(x) ≤ u before final concretization.
  • Backward-pass invariants: The backward pass propagates affine bounds through linear maps and activation relaxations while maintaining invariants over all inputs in B(x0, ε).The lower-bound case is symmetric to the described upper-bound procedure.
  • Concretization: After each layer’s backward pass, concretization obtains L(k) and U(k) by minimizing and maximizing the affine bounds over x ∈ B(x0, ε).These vectors provide the layerwise bounds used by subsequent recursive calls.

4 PANDA Framework

PANDA is a commit-and-prove zero-knowledge protocol that certifies local neural-network robustness while keeping model parameters and the CROWN transcript private. It combines arithmetic and lookup proofs with a Four-Point Relaxation Gadget, and retains polynomial runtime in network size.

  • Protocol overview: PANDA certifies local robustness in zero knowledge through a commit-and-prove protocol.The prover convinces the verifier of a local robustness claim without revealing the committed witness.
  • Protocol overview: The private witness contains model parameters and the CROWN transcript, while the public statement contains commitments, the robustness claim, and model architecture.The robustness claim is specified by (x0, ε, C, u).
  • Proof components: PANDA uses ΠARITH for matrix arithmetic and ΠLOOKUP for table lookups during quantized CROWN verification.ΠARITH proves equations (8), (9), (11), (12), and (13); ΠLOOKUP proves equations (10) and (14).
  • Proof components: The Four-Point Relaxation Gadget proves activation relaxation equations over real-valued intervals, where pointwise lookup checks lack between-point soundness.It addresses the insufficiency of ΠARITH and ΠLOOKUP for equation (7).
  • Asymptotic runtime: O(m2n3) is CROWN’s runtime for an m-layer network with n neurons per layer, and PANDA inherits this polynomial runtime.This follows from instantiating the protocol with ZKP systems and a commitment scheme requiring linear prover time.

5 The Four-Point Relaxation Gadget

The Four-Point Relaxation Gadget reduces validity checks for S-shaped activation relaxations to at most four points per neuron and removes case-specific analysis from the ZKP encoding. It also provides specialized validity proofs for ReLU relaxations selected by CROWN.

  • S-shaped activations: Four points per neuron suffice to check linear relaxation validity for S-shaped activations, independent of interval width.The points are the interval endpoints l and u and up to two tangency points.
  • Case-free soundness: Theorem 5.1 gives case-free sufficient criteria for proving upper-bound validity without revealing which tangency-point case applies.This avoids leaking private interval endpoints derived from model parameters.
  • Case-free soundness: CROWN’s selected linear relaxations satisfy the case-free soundness criteria.The theorem has a symmetric lower-bound statement provided in Appendix H.
  • ZKP algorithm: The ZKP algorithm encodes the soundness criteria using ΠARITH and ΠLOOKUP, with the prover supplying private intervals, bounds, tangency points, and activation evaluations.The verifier checks all resulting proofs using lookup tables Tσ and Tσ′.
  • ReLU: For ReLU, the gadget proves upper-bound validity by checking endpoint equalities and lower-bound validity by proving a ∈{0, 1} with intercept b = 0.These conditions are proven with ΠARITH; ΠLOOKUP supports selecting a within [0, 1] for α-CROWN.

6 Implementation and Evaluations

PANDA’s evaluations cover scalability, activation support, fidelity, privacy overhead, and comparison with prior work. It proves robustness for million-parameter networks, preserves CROWN’s certified claims, and substantially outscales the only suitable prior ZKP comparison.

  • Q1: Scalability: Under six minutes, PANDA proves local robustness for 4 × [1024] MNIST networks with 2.9 million parameters.This is the largest evaluated MNIST network.
  • Q2: Support of activation functions: Relative to ReLU, sigmoid/tanh increases proving time by 1.5–2.6×, with verification time and proof size growing similarly.PANDA therefore supports non-ReLU activations with comparable overhead scaling.
  • Q3: Fidelity: PANDA verifies all claims that CROWN verifies, although quantization introduces errors through lossy rounding and lookup-table discretization.The evaluation measures drift between PANDA and CROWN and compares their certification results.
  • Q4: Comparison with CROWN: 100–1,000× prover overhead and 20–50× verifier overhead are PANDA’s privacy costs over CROWN on 1024-neuron models.The verifier overhead rises to 106× only on toy networks where CROWN runs in microseconds and ZKP fixed costs dominate.
  • Q5: Comparison with previous work: FairProof cannot run on even the smallest MNIST network, while PANDA requires about half its prover time on FairProof Adult and has a 1.21s verifier cost.FairProof is identified as the only suitable direct comparison and the only known ZKP system certifying local robustness.

7 Known Limitations

PANDA’s guarantees are limited to quantized models and reveal architectural details, while quantization precision affects lookup-table accuracy and rounding lossiness. As an incomplete verifier inherited from CROWN, PANDA can certify many but not all robustness claims and cannot falsify them.

  • Quantization and privacy limits: PANDA proves robustness only for quantized models, whose precision affects lookup-table accuracy and rounding lossiness.It does not support general floating-point models.
  • Quantization and privacy limits: PANDA publicly discloses the model architecture, layer dimensions, and activation function, hiding only weights and biases.Dummy layers and weights can pad DNNs to conceal exact dimensions.
  • Verification limits: PANDA inherits CROWN’s incompleteness: it can verify many but not all robustness claims and cannot falsify a claim.Complete local-robustness verification for DNNs is NP-hard, whereas CROWN over-approximates bounds in polynomial time.

8 Related Work

Prior work addresses fairness and robustness certification with either zero-knowledge proofs or non-cryptographic verification, while concurrent Secure-CROWN uses secure two-party computation for private local-robustness claims. PANDA differs by supporting zero-knowledge certification without revealing model parameters.

  • Proof of fairness: FairProof verifies local fairness and robustness with ZKPs but supports only ReLU activations and incurs prover time exponential in network size.Its preprocessing enumerates all possible neuron activations.
  • Non-cryptographic certification approaches: Non-cryptographic certification methods verify local robustness but require the verifier to access model parameters.PANDA certifies these properties in zero knowledge without revealing the parameters.
  • Concurrent work: Secure-CROWN uses secure two-party computation to jointly compute CROWN while hiding the query point, perturbation radius, and model from the respective parties.Its computation trace is not publicly verifiable, and the construction is in the hone…

9 Conclusion … B Details of PANDA

PANDA confidentially proves and verifies linear model-output properties such as fairness and robustness, improving prover performance and scalability while keeping model data private. The appendices detail CROWN’s relaxation procedure and PANDA’s proof algorithms and lookup-based gadgets.

  • 9 Conclusion: PANDA enables model owners to share verifiable robustness proofs publicly without revealing model data.The system was evaluated on leading benchmarks, with improvements in prover time and scalability.
  • A Details of CROWN: CROWN computes neural-network bounds through an outer forward pass and an inner backward pass that repeatedly applies activation relaxation, linear substitution, and concretization.The full procedure is given in Algorithm 1.
  • A.1 The CROWN Algorithm: O(m^2n^3) is CROWN’s time complexity for a network with m layers, n neurons per layer, and n output neurons.The complexity arises from two nested layer loops and O(n^3) matrix multiplications at each layer.
  • A.2 The Relaxation Algorithm: RELAX produces per-neuron linear relaxations that PANDA verifies using the Four-Point Relaxation Gadget.For S-shaped activations, the procedure selects an upper bound using tangent or secant lines according to the non-trivial root τ.
  • A.2 The Relaxation Algorithm: For S-shaped activations, RELAX selects the tangent or secant upper bound based on where τ lies relative to the interval endpoints.When τ ≤ l, it outputs a midpoint tangent; when τ ≥ u, it outputs the endpoint secant.
  • B Details of PANDA: PANDA’s full algorithms include the Four-Point Relaxation Gadget prover, the PANDA prover, and the verifier.Appendix F describes an optimization that eliminates the Tσ′ lookup table.
  • B Details of PANDA: ΠLOOKUP uses public tables for ReLU values, activation values, and activation derivatives over the quantization domain D.The same lookup mechanism also performs range proofs.
  • B Details of PANDA: The Four-Point Relaxation Gadget prover proves endpoint and tangency conditions using activation lookups, ordering checks, and arithmetic equalities.Its witness contains (l, u, a, b, z1, z2), and it returns all generated proofs.

C Comparison with FairProof · D Complete Evaluation · E Prover Breakdown

PANDA is compared directly with FairProof on shared robustness benchmarks and evaluated across model families under a defined testing protocol. Its prover-time breakdown identifies lookup arguments as the largest component while all components scale polynomially with network size.

  • C Comparison with FairProof: FairProof is the only suitable direct comparison because it is the only known ZKP system certifying local robustness.The comparison uses FairProof’s Adult model and PANDA’s smallest MNIST models on the first five properties PANDA proves.
  • C Comparison with FairProof: The FairProof offline phase was reimplemented and validated against its released example using one core and the same CPUs as PANDA’s evaluation.This establishes the basis for the head-to-head comparison despite FairProof’s unreleased offline phase.
  • C Comparison with FairProof: 34.89s is PANDA’s prover time on FairProof Adult, versus 66.0s for FairProof, while FairProof cannot scale to larger MNIST models.PANDA therefore requires about half of FairProof’s prover time where both systems run; PANDA verification remains on the order of seconds.
  • D Complete Evaluation: The complete evaluation runs 100 tests per model, except for FairProof, which receives one test, and MNIST, which tests only correctly classified images.Reported prove and verify times are mean ± standard deviation over the verified subset, and N counts both evaluated benchmarks and CROWN-certified properties.
  • E Prover Breakdown: Table 4 reports component-wise prover times for three MNIST 3 × [20] and three MNIST 3 × [1024] models, averaged over PANDA’s first five properties.The breakdown compares prover components across these two network-size groups.
  • E Prover Breakdown: Lookup arguments are the largest prover-time component, while every component scales polynomially with network size.This observed scaling aligns with the theoretical guarantees of the underlying cryptographic protocols.

F Optimization: Finite Differences · G Proof of Lemma 5.1

PANDA replaces derivative-table lookup proofs with finite-difference conditions using only the activation table, under strict monotonicity and quantized spacing assumptions. The resulting theorem characterizes convex and concave cases, while Lemma 5.1 establishes derivative preimages across the activation’s range.

  • F Optimization: Finite Differences: Finite differences eliminate the derivative table Tσ′, reducing memory demands and avoiding brittle equality checks in quantized settings.The optimization requires σ to be strictly increasing and uses lookup tables only for σ.
  • F Optimization: Finite Differences: The method finds a quantized witness z0 near z whose finite differences certify σ′(z) = α up to quantization error δ.The witness lies within a δ-neighborhood and conditions depend only on σ, not σ′.
  • F Optimization: Finite Differences: Algorithm 2 can encode these finite-difference conditions using only σ lookups, selecting z0 as a δ-approximation even when σ is neither locally convex nor concave.For non-convex, non-concave neighborhoods, the construction uses z0 = 0 as a δ-approximation.
  • F Optimization: Finite Differences: Under convexity, finite differences at z0 bound δα from below and above: σ(z0) − σ(z0 − δ) ≤ δα and σ(z0 + δ) − σ(z0) ≥ δα.Theorem F.1 assumes uniformly spaced quantized points with spacing at most δ.
  • F Optimization: Finite Differences: Under concavity, the corresponding finite-difference inequalities reverse around z0.The bounds become σ(z0) − σ(z0 − δ) ≥ δα and σ(z0 + δ) − σ(z0) ≤ δα.
  • F Optimization: Finite Differences: A sign change between the two finite-difference deviations implies that some z within (z0 − δ, z0 + δ) satisfies σ′(z) = α.This converse follows by applying the Intermediate Value Theorem to σ′.
  • G Proof of Lemma 5.1: For every α ∈ (0, B), σ′ has one preimage on each side of zero; for α = B, the unique preimage is zero.This follows from continuity, boundedness, monotonicity on either side of zero, and σ′(0) = B.

H Proof of Theorem 5.1

Theorem 5.1 establishes a case-free four-point criterion that certifies candidate linear upper and lower bounds for nonlinear activations. It also proves that CROWN’s selected relaxations satisfy this criterion, yielding complete and sound bounds.

  • Theorem 5.1(a): The soundness proof reduces validity to checking nonnegativity at both interval endpoints and at each interior critical point of the difference function.The critical points are the two solutions identified by Lemma 5.1; endpoint and critical-point nonnegativity follows from conditions (i)–(iii).
  • Remark: For activations with even derivative σ′, the tangency points satisfy z1 = −z2, so Algorithm 2 needs only one tangency-point witness.The remark specifically names sigmoid, tanh, and arctan as examples.
  • Theorem 5.1(b): CROWN’s linear relaxations satisfy the criteria of Theorem 5.1(a), proving the four-point construction is complete.The proof verifies conditions (i), (ii), and (iii) for each of the three cases in the upper-bound selection procedure; the lower-bound argument is analogous.
  • Theorem 5.1(b): The completeness proof handles three selection cases: an interior tangent-secant point, a midpoint tangent when τ ≤ l, and an endpoint secant when τ ≥ u.The cases use concavity or secant-slope properties to establish the required endpoint and tangency inequalities.
Loading 2608.17070v1…