QEBVerif: Quantization error bound verification of neural networks

To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power and storage space by quantizing the weights and/or activation tensors of a DNN in...

Full description

Saved in:
Bibliographic Details
Main Authors: ZHANG, Yedi, SONG, Fu, SUN, Jun
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2023
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/8119
https://ink.library.smu.edu.sg/context/sis_research/article/9122/viewcontent/Computer_Aided_Verification.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-9122
record_format dspace
spelling sg-smu-ink.sis_research-91222023-09-14T08:38:56Z QEBVerif: Quantization error bound verification of neural networks ZHANG, Yedi SONG, Fu SUN, Jun To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power and storage space by quantizing the weights and/or activation tensors of a DNN into lower bit-width fixed-point numbers, resulting in quantized neural networks (QNNs). While it has been empirically shown to introduce minor accuracy loss, critical verified properties of a DNN might become invalid once quantized. Existing verification methods focus on either individual neural networks (DNNs or QNNs) or quantization error bound for partial quantization. In this work, we propose a quantization error bound verification method, named QEBVerif, where both weights and activation tensors are quantized. QEBVerif consists of two parts, i.e., a differential reachability analysis (DRA) and a mixed-integer linear programming (MILP) based verification method. DRA performs difference analysis between the DNN and its quantized counterpart layer-by-layer to compute a tight quantization error interval efficiently. If DRA fails to prove the error bound, then we encode the verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Thus, QEBVerif is sound, complete, and reasonably efficient. We implement QEBVerif and conduct extensive experiments, showing its effectiveness and efficiency. 2023-07-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/8119 info:doi/10.1007/978-3-031-37703-7_20 https://ink.library.smu.edu.sg/context/sis_research/article/9122/viewcontent/Computer_Aided_Verification.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University OS and Networks Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic OS and Networks
Software Engineering
spellingShingle OS and Networks
Software Engineering
ZHANG, Yedi
SONG, Fu
SUN, Jun
QEBVerif: Quantization error bound verification of neural networks
description To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power and storage space by quantizing the weights and/or activation tensors of a DNN into lower bit-width fixed-point numbers, resulting in quantized neural networks (QNNs). While it has been empirically shown to introduce minor accuracy loss, critical verified properties of a DNN might become invalid once quantized. Existing verification methods focus on either individual neural networks (DNNs or QNNs) or quantization error bound for partial quantization. In this work, we propose a quantization error bound verification method, named QEBVerif, where both weights and activation tensors are quantized. QEBVerif consists of two parts, i.e., a differential reachability analysis (DRA) and a mixed-integer linear programming (MILP) based verification method. DRA performs difference analysis between the DNN and its quantized counterpart layer-by-layer to compute a tight quantization error interval efficiently. If DRA fails to prove the error bound, then we encode the verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Thus, QEBVerif is sound, complete, and reasonably efficient. We implement QEBVerif and conduct extensive experiments, showing its effectiveness and efficiency.
format text
author ZHANG, Yedi
SONG, Fu
SUN, Jun
author_facet ZHANG, Yedi
SONG, Fu
SUN, Jun
author_sort ZHANG, Yedi
title QEBVerif: Quantization error bound verification of neural networks
title_short QEBVerif: Quantization error bound verification of neural networks
title_full QEBVerif: Quantization error bound verification of neural networks
title_fullStr QEBVerif: Quantization error bound verification of neural networks
title_full_unstemmed QEBVerif: Quantization error bound verification of neural networks
title_sort qebverif: quantization error bound verification of neural networks
publisher Institutional Knowledge at Singapore Management University
publishDate 2023
url https://ink.library.smu.edu.sg/sis_research/8119
https://ink.library.smu.edu.sg/context/sis_research/article/9122/viewcontent/Computer_Aided_Verification.pdf
_version_ 1779157160507211776