Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

9-2024

Abstract

Quantization plays an important role in deploying neural networks on embedded, real-time systems with limited computing and storage resources (e.g., edge devices). It significantly reduces the model storage cost and improves inference efficiency by using fewer bits to represent the parameters. However, it was recently shown that critical properties may be broken after quantization, such as robustness and backdoor-freeness. In this work, we introduce the first method for synthesizing quantization strategies that verifiably maintain desired properties after quantization, leveraging a key insight that quantization leads to a data distribution shift in each layer. We propose to compute the preimage for each layer based on which the preceding layer is quantized, ensuring that the quantized reachable region of the preceding layer remains within the preimage. To tackle the challenge of computing the exact preimage, we propose an MILP-based method to compute its under-approximation. We implement our method into a tool Quadapter and demonstrate its effectiveness and efficiency by providing certified quantization that successfully preserves model robustness and backdoor-freeness.

Discipline

Databases and Information Systems | Numerical Analysis and Scientific Computing

Research Areas

Intelligent Systems and Optimization

Publication

Formal Methods: 26th International Symposium FM 2024, Milan, September 9-13: Proceedings

Volume

14933

First Page

343

Last Page

362

ISBN

9783031711619

Identifier

10.1007/978-3-031-71162-6_18

Publisher

Springer

City or Country

Cham

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-031-71162-6_18

Download

Share

COinS