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.LGAug 17, 2026

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

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

Organizations: Yale University · University of Illinois Urbana-Champaign

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: Linear relaxations of the ReLU (left) and $\tanh$ (right) activation functions over the interval $[l,u]$ (shaded). Each activation $\sigma(z)$ (black) is bounded by affine functions $h_{U}(z)$ (dashed green) and $h_{L}(z)$ (dashed red) over the interval $[l,u]$ .

Panel of Figure 2 — Figure 2: Case-free four-point soundness (Theorem 5.1 ) for the activation function $\sigma(z)=\tanh(z).$ The left image depicts $[l,u]=[-1.5,1.5]$ , $z_{2}\leq u$ , and $\sigma(z_{2})\leq h_{U}(z_{2})$ . The right image depicts $[l,u]=[-1.5,0.2]$ , $z_{2}>u$ , and $\sigma(z_{2})>h_{U}(z_{2}).$ Both cases therefore satisfy the criteria given by Theorem 5.1 without requiring case-specific analysis.

Dataset	Structure	Act.	Prove (s)	Verify (s)	Proof	CROWN	Drift
					(MB)	(s)	(%)
MNIST
	$2\times[20]$	ReLU	$22.81\pm 20$	$0.97\pm 1$	3	1.3e-4	0.02
	$3\times[1024]$	ReLU	$101.58\pm 375$	$4.60\pm 13$	9	0.22	0.03
	$4\times[1024]$	ReLU	$226.08\pm 1467$	$9.56\pm 48$	17	0.44	-0.01
	$4\times[1024]$	Sigmoid	$327.47\pm 1136$	$14.13\pm 46$	31	0.47	2.48

Table 1: Summary of results. Each row is one model. We denote an

m

-layer feed-forward network with

n

neurons per layer by

m\times[n].

Prove and verify times are reported as mean and standard deviation. FairProof Adult is a two-layer network with 8 and 2 neurons, denoted

[8,2]

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

Model	Offline prove (s)	Online prove (s)	Verify (s)	Proof (KB)
FairProof Adult	$9.2$	$56.8$	$0.02$	$19.1$
MNIST $2\times[20]$ ReLU	$1908.0^{\dagger}$	4/5 timeout ( $>$ 1h), 1/5 OOM ( $>$ 512GiB)	—	—
MNIST $3\times[20]$ ReLU	timeout ( $>$ 12h)	—	—	—
MNIST $2\times[1024]$ ReLU	timeout ( $>$ 12h)	—	—	—

Appendix

Table 2: FairProof’s performance on small benchmarks.

Dataset	Structure	Act.	Prove (s)	Verify (s)	Proof	CROWN	Drift	N
					(MB)	(s)	(%)
MNIST
	$2\times[20]$	ReLU	$22.81\pm 20$	$0.97\pm 1$	3	0.00013	0.02	97
	$2\times[20]$	Sigmoid	$58.35\pm 81$	$2.33\pm 3$	8	0.00014	0.19	94
	$2\times[20]$	Tanh	$58.77\pm 39$	$2.34\pm 3$	8	0.00014	0.16	97
	$3\times[20]$	ReLU	$42.64\pm 51$	$1.90\pm 3$	6	0.00018	0.04	95

Appendix

Table 3: Evaluation. Each row is one model. (adv.) denotes adversarially trained models. 100 tests are run for each model, except for FairProof (only one test is run) and MNIST (only images correctly classified by the model are tested). Prove/verify times show

\mu\pm\sigma

(mean and standard deviation) over the verified subset only. N is the number of benchmarks evaluated for each model, which is also the number of properties that CROWN certifies for that model.

			Cryptographic					Non-crypto
Structure	Act.	prove	commit	matmul	lookup	other	total	tangent	total
Absolute time (s); tangent in ms
$3\times[20]$	ReLU	45.08	0.93	0.35	43.59	0.21	45.07	0.000	0.01
$3\times[20]$	Sigmoid	92.34	0.86	0.33	90.25	0.89	92.33	0.009	0.01
$3\times[20]$	Tanh	116.45	0.94	0.36	113.27	1.87	116.44	0.013	0.01
$3\times[1024]$	ReLU	106.95	15.70	8.54	66.08	0.51	90.82	0.000	16.12

Appendix

Table 4: Component-wise breakdown of the prover time. commit = polynomial commitments to every witness (Hyrax [ 28 ] ); matmul = the matrix-multiplication verification ( [ 26 ] ); lookup = all lookup arguments (LogUp-GKR [ 21 ] ); other = other cryptographic computation; total in Cryptographic = the sum of the four preceding columns; total in Non-crypto = total non-cryptographic computation time of the prover (including the plaintext quantized-CROWN that generates witnesses); tangent = time for computing the tangent points used in linear relaxations of S-shaped activation functions, which is a part of total in . Upper panel: absolute times; lower panel: shares of prove . Note the unit change on tangent .

Certified Robustness

Certified robustness develops formal guarantees that model predictions remain reliable under specified input or system perturbations.

See all 84 papers

Jul 6, 2026

Privacy-Preserving Robustness Verification for Neural Networks

Neural network verification and data privacy are inherently in tension: verification demands full access to model parameters and input data, yet both are increasingly restricted by privacy regulations and intellectual property constraints. This tension has left robustness verification impractical in privacy-sensitive domains. In this work, we address this gap with SecureCROWN, the first framework for privacy-preserving neural network robustness verification. Built upon secure two-party computation (2PC), our framework enables a model owner and a data owner to jointly compute certified robustness bounds -- revealing only the final result while provably protecting both parties' private data under the semi-honest security model. A key challenge is securely computing the conditional operations in Linear Bound Propagation, where the data-dependent branching is incompatible with standard secure computation protocols. We eliminate branching by formulating conditional logic as continuous arithmetic operations. Additionally, we introduce a Newton--Raphson refinement method to improve numerical stability. Extensive analysis and experiments show that SecureCROWN strictly matches plaintext verification results, while completing in 0.1--200s across varied model sizes and communication settings (LAN/WAN), demonstrating the feasibility of privacy-preserving neural network verification.

Nianyun Song, Xiaokun Luan, Yu Guo +3

School of Artificial Intelligence, Beijing Key Laboratory of Artificial Intelligence for Education, Engineering Research Center of Intelligent Technology and Educational Application (Ministry of Education), Beijing Normal University, Beijing, China · School of Mathematical Sciences, Peking University, Beijing, China · School of Computer Science, University of Bristol, Bristol, UK

Secure Multi-Party Computation Neural Network Verification Neural Network Robustness Privacy-Preserving ML Certified Robustness

Ask PDF

Mar 17, 2026

NanoZK: Privacy-Preserving Verifiable Inference for Large Language Models via Layerwise Zero-Knowledge Proofs

We present NanoZK, a zero-knowledge proof system for verifiable LLM inference: clients and third-party auditors check that a provider executed the advertised model on a committed input without learning weights or activations. NanoZK introduces a layerwise proof framework that decomposes transformer inference into independently provable layers linked by a SHA-256 commitment chain, yielding constant-size sub-circuit proofs (3.5-3.7 KB; about 83 KB total at L=12), comparable in total size to and substantially more parallelizable than prior ZKML's monolithic 101-126 KB proofs. We prove compositional soundness and zero-knowledge under standard assumptions, design 16-bit lookup-table approximations for softmax, GELU, and normalization with measured perplexity degradation below 1e-4 across six model/dataset combinations, and add a Fisher-information-guided audit-budget triage as an efficiency tool (full soundness still requires verifying every layer). On CPU the MLP sub-circuit proves in about 6.3 s prove-only (about 43 s setup plus prove) with about 22 ms verification at any width; attention prove-only time scales from 0.9 s (d=16) to 184 s (d=256); full-block end-to-end proofs are measured to d=128, with a projected GPU time of about 68 s per block at d=768 from measured O(d^2) MSM scaling and a conservative 15-30x GPU-MSM speedup range based on Icicle's published 30x result for n >= 2^20 and extrapolated to the smaller-n regime. Privacy scope: NanoZK hides weights and activations from verifiers and auditors but does not hide the prompt from the prover; this is complementary to HE/MPC.

Zhaohui Wang

USC Viterbi School of Engineering, Los Angeles, CA, USA

Zero-Knowledge ML Privacy-Preserving ML Privacy-Preserving Language Models LLM Inference

Ask PDF

Jun 8, 2026

Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism

Formal neural network verification -- proving that a network satisfies safety properties for all inputs in a specified domain -- is bounded in practice by GPU memory: standard implementations of bound-propagation algorithms (IBP, CROWN,

α

-CROWN) require weight and relaxation-coefficient matrices to reside entirely on one accelerator. We adapt two parallelism techniques originally developed for large-scale model training to the auto_LiRPA /

α,β

-CROWN verification framework. Tensor Parallelism (TP) shards both weight and

A

-matrices across GPUs, achieving

{\approx}2\times

peak-memory reduction at

P{=}2

; soundness is confirmed on VNN-COMP 2022 MNIST-FC benchmarks, though bound tightness degrades with the number of sharded zones due to forced IBP substitution for intermediate bounds inside sharded zones. Fully Sharded Data Parallelism (FSDP) shards only weight matrices with a per-layer AllGather, producing bounds that are bitwise identical to the single-GPU baseline: baseline memory drops by 80--90%, peak memory by 34--39% on wide MLPs. FSDP integrates cleanly with complete verification (

β

-CROWN + Branch-and-Bound) and with convolutional layers (BoundConv); a complete unsat result is obtained for CIFAR-100 ResNet-large (VNN-COMP 2024) under FSDP. Across all experiments the memory bottleneck in

α

-CROWN+BaB mode proves to be per-neuron alpha tensors, not weight matrices, pointing to the key direction for future work.

Sergei Vorobyov, Eugene Ilyushin

Lomonosov Moscow State University · Central University

Neural Network Verification High-Performance Computing Tensor Parallelism

Ask PDF

Abstract

Certified Robustness

Explore similar work

Privacy-Preserving Robustness Verification for Neural Networks

NanoZK: Privacy-Preserving Verifiable Inference for Large Language Models via Layerwise Zero-Knowledge Proofs

Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism