Research map / Learning theory and algorithms / Combinatorial and search optimization

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

NeurIPS 2026 · Learning theory and algorithms › Combinatorial and search optimization · approach: Semidefinite relaxations for verification

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes PANDA, a commit-and-prove ZKP system that certifies CROWN-based local robustness and fairness of private neural networks, using a Four-Point Relaxation Gadget to verify activation linear relaxations in polynomial time.

Problem

Proving local robustness of neural networks in zero knowledge (hiding model weights) is infeasible for large networks: prior ZKP robustness/fairness systems (FairProof) enumerate neuron activations exponentially and handle only tiny models.

Approach

Run CROWN outside the ZKP to find linear relaxations of activations, then certify them inside the ZKP via a case-free four-point check (endpoints and two tangency points) using lookup and matrix-arithmetic arguments, yielding polynomial prover time.

Key results

• Generates local robustness proofs for 4x1024 MNIST networks (2.9M parameters) in about 5 minutes (226 s ReLU) and verifies in about 10 s (9.6 s).
• On FairProof Adult, PANDA prover takes 34.89 s versus FairProof's 66.0 s total, while FairProof cannot run on even the smallest MNIST model.
• Sigmoid/tanh increase proving time by 1.5-2.6x over ReLU; quantization drift on MNIST stays within small relative differences (up to 6.33%).

Surprising findings

• FairProof times out (>12h) even on the 3x[20] MNIST model, while PANDA proves 4x[1024] networks.
• Quantization drift for tanh 4x1024 reaches 6.33% relative to CROWN, larger than for ReLU.

Limitations

• Only quantized models can be proven; quantization affects accuracy and drift relative to CROWN.
• Model architecture, layer dimensions and activation functions are public; only weights and biases are hidden.
• As an incomplete verifier based on CROWN, it cannot falsify claims or verify all true robustness properties.

Experimental setup

Datasets: MNIST SafeNLP LunarLander FairProof Adult

Benchmarks: MNIST SafeNLP LunarLander FairProof Adult

Metrics: prove time verify time proof size CROWN time drift (%) number of certified properties

Baselines: FairProof CROWN

Builds on: CROWN FairProof Hyrax LogUp-GKR alpha-CROWN

Closest papers by meaning

• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.88)
• FairProof : Confidential and Certifiable Fairness for Neural Networks (ICML 2024 · similarity 0.88)
• Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.88)
• Probably Approximately Global Robustness Certification (ICML 2025 · similarity 0.88)
• Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization (ICLR 2025 · similarity 0.86)
• Halt Fast! Early Stopping for Certified Robustness (NeurIPS 2026 · similarity 0.86)