Towards Efficient Verification of Quantized Neural Networks. Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., & Barrett, C. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, pages 21152–21160, February, 2024. Paper abstract bibtex 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.
@inproceedings{HWY+24,
url = "https://arxiv.org/abs/2312.12679",
author = "Huang, Pei and Wu, Haoze and Yang, Yuting and Daukantas, Ieva and Wu, Min and Zhang, Yedi and Barrett, Clark",
title = "Towards Efficient Verification of Quantized Neural Networks",
booktitle = "Proceedings of the AAAI Conference on Artificial Intelligence",
volume = 38,
number = 19,
pages = "21152--21160",
month = feb,
year = 2024,
category = "Conference Publications",
abstract = "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."
}
Downloads: 0
{"_id":"PrejXty3wBrfZrZ6S","bibbaseid":"huang-wu-yang-daukantas-wu-zhang-barrett-towardsefficientverificationofquantizedneuralnetworks-2024","author_short":["Huang, P.","Wu, H.","Yang, Y.","Daukantas, I.","Wu, M.","Zhang, Y.","Barrett, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","url":"https://arxiv.org/abs/2312.12679","author":[{"propositions":[],"lastnames":["Huang"],"firstnames":["Pei"],"suffixes":[]},{"propositions":[],"lastnames":["Wu"],"firstnames":["Haoze"],"suffixes":[]},{"propositions":[],"lastnames":["Yang"],"firstnames":["Yuting"],"suffixes":[]},{"propositions":[],"lastnames":["Daukantas"],"firstnames":["Ieva"],"suffixes":[]},{"propositions":[],"lastnames":["Wu"],"firstnames":["Min"],"suffixes":[]},{"propositions":[],"lastnames":["Zhang"],"firstnames":["Yedi"],"suffixes":[]},{"propositions":[],"lastnames":["Barrett"],"firstnames":["Clark"],"suffixes":[]}],"title":"Towards Efficient Verification of Quantized Neural Networks","booktitle":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":"38","number":"19","pages":"21152–21160","month":"February","year":"2024","category":"Conference Publications","abstract":"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.","bibtex":"@inproceedings{HWY+24,\n url = \"https://arxiv.org/abs/2312.12679\",\n author = \"Huang, Pei and Wu, Haoze and Yang, Yuting and Daukantas, Ieva and Wu, Min and Zhang, Yedi and Barrett, Clark\",\n title = \"Towards Efficient Verification of Quantized Neural Networks\",\n booktitle = \"Proceedings of the AAAI Conference on Artificial Intelligence\",\n volume = 38,\n number = 19,\n pages = \"21152--21160\",\n month = feb,\n year = 2024,\n category = \"Conference Publications\",\n abstract = \"Quantization replaces floating point arithmetic with integer\n arithmetic in deep neural network models, providing more\n efficient on-device inference with less power and memory. In\n this work, we propose a framework for formally verifying\n properties of quantized neural networks. Our baseline\n technique is based on integer linear programming which\n guarantees both soundness and completeness. We then show how\n efficiency can be improved by utilizing gradient-based\n heuristic search methods and also bound-propagation\n techniques. We evaluate our approach on perception networks\n quantized with PyTorch. Our results show that we can verify\n quantized networks with better scalability and efficiency\n than the previous state of the art.\"\n}\n\n\n","author_short":["Huang, P.","Wu, H.","Yang, Y.","Daukantas, I.","Wu, M.","Zhang, Y.","Barrett, C."],"key":"HWY+24","id":"HWY+24","bibbaseid":"huang-wu-yang-daukantas-wu-zhang-barrett-towardsefficientverificationofquantizedneuralnetworks-2024","role":"author","urls":{"Paper":"https://arxiv.org/abs/2312.12679"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://aisafety.stanford.edu/bib/all-pubs.bib","dataSources":["Q5m4eREZKA5kKSYST"],"keywords":[],"search_terms":["towards","efficient","verification","quantized","neural","networks","huang","wu","yang","daukantas","wu","zhang","barrett"],"title":"Towards Efficient Verification of Quantized Neural Networks","year":2024}