mlsanityData to 7 Oct 2026

Towards Efficient Verification of Quantized Neural Networks

arXiv 2312.12679 ↗First posted 20 Dec 2023cs.LG cs.AI cs.LOcited by 10

Not on the map. Why?

Abstract (arXiv)

Quantization replaces floating point arithmetic with integer arithmetic in deep neural network models, providing more efficient on-device inference with less power and memory. In this work, we propose a framework for formally verifying properties of quantized neural networks. Our baseline technique is based on integer linear programming which guarantees both soundness and completeness. We then show how efficiency can be improved by utilizing gradient-based heuristic search methods and also bound-propagation techniques. We evaluate our approach on perception networks quantized with PyTorch. Our results show that we can verify quantized networks with better scalability and efficiency than the previous state of the art.

Key facts. Cited by 10 papers in the map (data through 7 Oct 2026). Builds on 18 of its 30 references that are in the map. First posted on arXiv 20 Dec 2023.

Builds on

18 of 30 references.

References · 18

  1. 2014Very Deep Convolutional Networks for Large-Scale Image Recognitioncited by 15,267
  2. 2014Explaining and Harnessing Adversarial Examplescited by 7,287
  3. 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,326
  4. 2015Deep Compression: Compressing Deep Neural Networks with Pruning, Trained Quantization and Huffman Codingcited by 2,291
  5. 2017Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inferencecited by 1,548
  6. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
  7. 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 564
  8. 2016Safety Verification of Deep Neural Networkscited by 262
  9. 2018Towards Fast Computation of Certified Robustness for ReLU Networkscited by 254
  10. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
  11. 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 178
  12. 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
6 more
  1. 2016End-to-end Learning of Driving Models from Large-scale Video Datasetscited by 147
  2. 2020Efficient Exact Verification of Binarized Neural Networkscited by 33
  3. 2021Boosting Transferability of Targeted Adversarial Examples via Hierarchical Generative Networkscited by 31
  4. 2020Scalable Verification of Quantized Neural Networks (Technical Report)cited by 28
  5. 2021Stability Verification in Stochastic Control Systems via Neural Network Supermartingalescited by 24
  6. 2022Quantifying Robustness to Adversarial Word Substitutionscited by 2

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 1; 2025: 6; 2026: 3.

10 papers.

  1. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  2. 2025Neural Network Verification is a Programming Language Challengecited by 12
  3. 2025Verifying Quantized Graph Neural Networks is PSPACE-completecited by 2
  4. 2025Verification of Bit-Flip Attacks against Quantized Neural Networkscited by 2
  5. 2025Floating-Point Neural Network Verification at the Software Levelcited by 2
  6. 2026VNN-LIB 2.0: Rigorous Foundations for Neural Network Verificationcited by 1
  7. 2025S2A: A Unified Framework for Parameter and Memory Efficient Transfer Learningcited by 0
  8. 2025Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precisioncited by 0
  9. 2026Neural Network Verification using Partial Multi-Neuron Relaxationcited by 0
  10. 2026Mining Verdict Boundaries for Neural Network Verificationcited by 0