Research map / Architectures and efficiency / Quantization
Towards Efficient Verification of Quantized Neural Networks
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 EQV, a verifier for PyTorch-style quantized neural networks combining exact ILP encoding, interval bound propagation (via Marabou) and gradient-based PGD counterexample search with a rewritten round operation.
Problem
Formal robustness verification of quantized neural networks (QNNs) under the real quantization schemes used in deep learning frameworks such as PyTorch, which prior work did not model and which scale poorly.
Approach
Exact ILP encoding of the full PyTorch quantization pipeline (round, clip, zero-point, scale), with a clip-as-two-ReLUs trick to enable abstract interpretation bounds, and a straight-through style rewrite y=Round(x)+x-x.detach() so gradient-based attacks can find counterexamples quickly before invoking the solver.
Key results
- On FC1-100 at r=4, EQV takes 104.09 s versus 11751.16 s for QVIP (30 timeouts), and FC2-100 at r=4 takes 1465.46 s versus 30000 s (100 timeouts).
- At r=4 EQV gives an answer for about 88% of instances even on FC2-512 within a 30-minute limit (11% unknown).
- Across FC2-256, FC2-512, FC3-100, CNN1 and CNN2 at r=4, EQV is faster than pure ILP, e.g. CNN1 205.48 s vs 28235.35 s.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, FC2-256, r=4 | total execution time (s): 4456.76 -> 4019.10 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, FC2-512, r=4 | total execution time (s): 8013.00 -> 7637.05 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, FC3-100, r=4 | total execution time (s): 3347.88 -> 2421.66 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, CNN1, r=4 | total execution time (s): 221.64 -> 205.48 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, CNN2, r=4 | total execution time (s): 1041.85 -> 723.13 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, FC2-256, r=8 | total execution time (s): 22543.68 -> 19918.79 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, FC2-512, r=8 | total execution time (s): 29891.39 -> 29179.91 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, FC3-100, r=8 | total execution time (s): 24330.21 -> 22616.44 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, CNN1, r=8 | total execution time (s): 2503.19 -> 1850.32 | Helped |
| Use EQV instead of ILP+In | QNN robustness verification · MNIST test, CNN2, r=8 | total execution time (s): 3715.99 -> 1499.73 | Helped |
| Add interval analysis to ILP (ablation) | ILP QNN verification · MNIST test, FC1-100, r=4 | total execution time (s): 332.48 -> 93.52 | Helped |
| Add interval analysis to ILP (ablation) | ILP QNN verification · MNIST test, FC2-100, r=4 | total execution time (s): 4039.38 (7) -> 1581.41 (3) | Helped |
Surprising findings
- Quantization does not always reduce robustness: below a radius threshold real-valued networks are more robust, while above it QNNs show better robustness.
- Parallelizing the ILP and abstract interpretation with 20 threads improves efficiency by less than 10%.
Limitations
- Scalability still limited on larger networks near the maximum safe radius, with many timeouts for FC2-512 and FC3-100 at r=8 and above.
- Evaluated only on MNIST-trained fully connected and small convolutional networks.
- Comparison to QVIP is only for reference since QVIP uses a simplified quantization scheme.
Experimental setup
Datasets: MNIST
Benchmarks: MNIST
Metrics: solving time (s) number of timeouts percentage robust / unsafe / unknown
Baselines: QVIP ILP ILP+In
Builds on: QVIP Marabou PGD big-M encoding
Closest papers by meaning
- Scalable Verification of Quantized Neural Networks (AAAI 2021 · similarity 0.92)
- Training Quantized Nets: A Deeper Understanding (NeurIPS 2017 · similarity 0.89)
- Fully Quantized Network for Object Detection (CVPR 2019 · similarity 0.87)
- Linear Symmetric Quantization of Neural Networks for Low-precision Integer Hardware (ICLR 2020 · similarity 0.87)
- On the Universal Approximability and Complexity Bounds of Quantized ReLU Neural Networks (ICLR 2019 · similarity 0.87)
- Degree-Quant: Quantization-Aware Training for Graph Neural Networks (ICLR 2021 · similarity 0.87)
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.