Research map / Adversarial robustness and security / Certified and empirical robustness
VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees
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 VNN, a post-training layer-wise sparsification method that solves an L1-relaxed linear program to make trained DNNs (FNNs and CNNs) more amenable to formal robustness verification while keeping accuracy.
Problem
Formal verification of DNN robustness suffers from scalability and precision limits because over-approximation accumulates through the forward pass, leaving many samples unverified.
Approach
Post-training, layer-by-layer optimization that minimizes the L1 norm of weights and biases (a convex relaxation of L0) under linear constraints that keep each neuron's ReLU activation state, output-perturbation bound epsilon, and predicted class on a validation set, yielding sparser networks that verifiers can certify more often.
Key results
- On MNIST 2x50 FNN with ERAN at delta=0.03, verified robustness rises from 22.5% (original) to 75.5% (VNN), and VNNs verify up to 76 times more samples overall.
- On CHB-MIT and MIT-BIH, VNNs verify up to 24 and 34 times more samples than the original CNNs, with accuracy of 82.5% vs 85.7% on CHB-MIT and 92.0% vs 91.5% on MIT-BIH.
- Versus MBP and SOP, VNNs are up to 46, 19, and 27 times more verification-friendly than MBP on MNIST, CHB-MIT, and MIT-BIH, and up to 51 times more than SOP on MNIST.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Optimize the FNN into a VNN | MNIST FNN, 2×50 · MNIST, δ=0.03, ERAN | verified robustness (%): 22.5 -> 75.5 | Helped |
| Optimize the FNN into a VNN | MNIST FNN, 2×50 · MNIST, δ=0.03, SafeDeep | verified robustness (%): 41 -> 79.5 | Helped |
| Optimize the FNN into a VNN | MNIST FNNs · MNIST | average processing time | Mixed |
| Optimize the CNN into a VNN | CHB-MIT CNN · CHB-MIT | accuracy: 85.7% ± 3.8% -> 82.5% ± 4.2% | Hurt |
| Optimize the CNN into a VNN | CHB-MIT CNN · CHB-MIT, ERAN | verified robustness: up to 9 times | Helped |
| Optimize the CNN into a VNN | CHB-MIT CNN · CHB-MIT, SafeDeep | verified robustness: up to 24 times | Helped |
| Set the 10% smallest weights and biases to zero | CHB-MIT CNN · CHB-MIT | accuracy: 85.7% ± 3.8% -> 84.1% ± 4.1% | Hurt |
| Match VNN sparsity using MBP pruning | CHB-MIT CNN · CHB-MIT | accuracy: 68.4% ± 4.3% | Hurt |
| Optimize the CNN into a VNN | MIT-BIH CNN · MIT-BIH | accuracy: 91.5% ± 3.1% -> 92.0% ± 3.0% | Helped |
| Optimize the CNN into a VNN | MIT-BIH CNN · MIT-BIH, ERAN | verified robustness: up to 34 times | Helped |
| Optimize the CNN into a VNN | MIT-BIH CNN · MIT-BIH, SafeDeep | verified robustness: up to 30 times | Helped |
| Increase ε to 0.3 (ablation) | FNN, 9×200 · MNIST | accuracy: above 90% -> 80% | Hurt |
Surprising findings
- Pruned FNNs (MBP, 7x200 from prior work) with high accuracy did not show higher verification-friendliness than the original network.
- Larger validation sets improve prediction performance of VNNs, while small validation sets relative to model size cause accuracy drops.
Limitations
- Exact verification (Marabou) does not scale; only the 2x50 FNN was evaluated with it and over 75% of larger-network cases timed out.
- Accuracy can degrade when the validation set is small relative to model size, especially with larger epsilon.
- Framework is developed for ReLU piecewise-linear activations; extension to other activations is claimed but not evaluated.
Experimental setup
Datasets: MNIST CHB-MIT Scalp EEG MIT-BIH Arrhythmia
Benchmarks: MNIST CHB-MIT MIT-BIH
Metrics: verified robustness (%) average verification time (s) clean accuracy number of verified samples
Baselines: magnitude-based pruning (MBP) SOP original DNNs PGD adversarial training
Builds on: ERAN / DeepPoly SafeDeep Marabou magnitude-based pruning sparsity-optimized pruning
Closest papers by meaning
- Interpreting Robustness Proofs of Deep Neural Networks (ICLR 2024 · similarity 0.90)
- Towards Trustworthy Deep Learning (AAAI 2024 · similarity 0.89)
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.89)
- Tightening Robustness Verification of MaxPool-based Neural Networks via Minimizing the Over-Approximation Zone (CVPR 2025 · similarity 0.88)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.88)
- Towards General Robustness Verification of MaxPool-based Convolutional Neural Networks via Tightening Linear Approximation (CVPR 2024 · similarity 0.88)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.