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
cs.LG, cs.CR, cs.LO
2026-08-18
Yale-led PANDA wraps the CROWN robustness certifier in zero-knowledge proofs: 2.9M-parameter networks prove local robustness in 5.5 minutes and verify in 14 seconds, four orders of magnitude beyond prior ZK systems, with weights never revealed.
Regulators and commercial customers increasingly demand formal robustness guarantees: small perturbations of the input must not flip the prediction. Formal verification tools need the model weights to run, and weights are exactly what model owners cannot hand over: trade secrets, and a conduit for white-box attacks that recover training data (a direct HIPAA problem in healthcare). The prior escape route, zero-knowledge robustness proofs in the FairProof line, enumerates neuron activation combinations and scales exponentially, capping out around 100-parameter toy networks in practice.
The tension is specific: verification tools demand weights, and owners cannot disclose them. This paper lets a model owner prove to anyone, without revealing weights, that a model is robust within a given perturbation radius, with a proof that is publicly verifiable and archivable.
PANDA builds on CROWN, the 2018 linear bound-propagation certification framework that sits inside state-of-the-art verifiers such as α-CROWN. CROWN finds linear upper and lower bounds sandwiching each activation function, propagates them backward layer by layer, and maximizes the resulting linear bound over the perturbation ball. If the output gap's upper bound stays below zero, robustness is certified. It runs in polynomial time but is incomplete: it over-approximates, so it can confirm robustness but not refute it.
The expensive step to move into a ZKP is line selection. Vanilla CROWN solves an equation iteratively to find optimal tangent lines, and running that search inside a circuit is prohibitive. PANDA's governing principle is "compute in the clear, verify in the circuit": the prover runs full CROWN outside the ZKP, commits to the chosen relaxation coefficients as a witness, and the circuit checks only a reduced constraint system. Verifying that a linear relaxation holds over a continuous interval naively means checking infinitely many points; the Four-Point Relaxation Gadget reduces it to four inequalities per neuron. For S-shaped activations like sigmoid, tanh, and arctan, checking the two interval endpoints and the two tangency points suffices. The criteria are deliberately case-free, because branching on whether a tangency point falls inside the interval would leak information about the weights.
Three pieces of engineering round it out. All real arithmetic is quantized into finite-field integers (14 bits, following zkML convention), with rounding remainers proved inside the circuit. Instead of a general-purpose ZKP backend, PANDA assembles three primitives (Hyrax polynomial commitments, Thaler's matrix-multiplication proof, and LogUp-GKR lookups) and routes each operation type to the cheapest fit. ReLU networks get a cheaper dedicated check (the secant line plus a line through the origin, two points). Prover time stays polynomial in the neuron count, inheriting CROWN's O(m²n³).
On MNIST 4×[1024] (four layers of 1024 neurons, 2.9M parameters): proving takes 5.5 minutes, verification 14 seconds, proof size 31-32 MB. The previous ceiling for ZK robustness proofs was roughly 100 parameters, so this is four orders of magnitude larger.
| Model | Activation | Prove (s) | Verify (s) | Proof (MB) |
| 2×[20] | ReLU | 22.8 | 0.97 | 3 |
| 3×[1024] | ReLU | 101.6 | 4.6 | 9 |
| 4×[1024] | Sigmoid | 327.5 | 14.1 | 31 |
| 4×[1024] | Tanh | 333.9 | 14.3 | 32 |
For calibration: proving costs roughly 100-1,000× plain CROWN (verification 20-50×), which is the price of privacy; sigmoid/tanh networks cost 1.5-2.6× ReLU. Against FairProof on the only benchmark both can run (the Adult two-layer 8/2-neuron network), PANDA proves in 34.89 s versus FairProof's 66.0 s end to end; FairProof times out (>1 hour) on four of five tests at MNIST 2×[20] and runs out of memory (>512 GiB) on the fifth. On quantization drift, PANDA verifies every claim CROWN certifies, with drift up to 12.6% on that tiny Adult network and within 0.5% on the large MNIST models.
AI regulation is turning provable robustness into an entry requirement for high-stakes settings, and hospitals, automakers, and risk teams need to convince third parties without surrendering weights. PANDA is the first system to make both possible at a practical scale: 2.9M parameters is a real MNIST-class classifier, though far from LLMs. For audit-platform builders the transferable idea is the compute-verify split: run the verifier outside the circuit, check constraints inside. That principle applies to any team ZK-ifying an existing verifier.
The incremental part should be stated plainly: no new verification algorithm here. Certification power is inherited from CROWN; the contribution is the ZK translation.
The authors list three: only quantized models can be proved, not general floating-point ones; the architecture, layer dimensions, and activation type are disclosed, with only weights hidden (dummy layers can mask dimensions at a cost); and CROWN's incompleteness carries over, so it cannot falsify robustness and certifies fewer claims than complete verifiers. Reading beyond the self-report: the implementation uses non-zero-knowledge variants of the three underlying protocols, and the claim that zero-knowledge variants would add only a small constant factor is an estimate, not a measurement. The FairProof comparison rests on the authors' reimplementation, since FairProof's offline phase was never released. Most importantly, the scale ceiling is unbroken: 2.9M parameters is a fully connected network, and convnets, Transformers, and LLMs are untouched. The zkML inference-verification line (DeepProve, zkGPT) tackles a different problem, and whether this method transfers there is not discussed.