CEG4N: Counter-Example Guided Neural Network Quantization Refinement

Abstract

Neural networks are essential components of learning-based software systems. However, deploying neural networks in low-resource domains is challenging because of their high computing, memory, and power requirements. For this reason, neural networks are often quantized before deployment, but existing quantization techniques tend to degrade network accuracy. We propose Counter-Example Guided Neural Network Quantization Refinement (CEG4N). This technique combines search-based quantization and equivalence verification: the former minimizes the computational requirements, while the latter guarantees that the network’s output does not change after quantization. We evaluate CEG4N on a diverse set of benchmarks, including large and small networks. Our technique successfully quantizes the networks in our evaluation while producing models with up to 72% better accuracy than state-of-the-art techniques.

A Appendices

1.1 A.1 Implementation of NNs in Python.

The NNs were built and trained using the Pytorch library [29]. Weights of the trained models were then exported to the ONNX [4] format, which can be interpreted by Pytorch and used to run predictions without any compromise in the NNs performance.

1.2 A.2 Implementation of NNs abstract models in C.

In the present work, we use the C language to implement the abstract representation of the NNs. It allows us to explicitly model the NN operations in their original and quantized forms and apply existing software verification tools (e.g., ESBMC [14]). The operational C-abstraction models perform double-precision arithmetic. Although, we must notice that the original and quantized only diverge on the precision of the weight and bias vectors that are embedded in the abstractions code.

1.3 A.3 Encoding of Equivalence Properties

Suppose, a NN  F, for which $x\in \mathcal {H}$ is a safe input and $y \in \mathcal {G}$ is the expected output of f the input. We now show how one can specify the equivalence properties. For this example, consider that the function f can produce the outputs of F in floating-point arithmetic, while fq produces the outputs of F in fixed-point arithmetic (i.e. quantization). First, the concrete NN  input x is replaced by a non-deterministic one, which is achieved using the command nondet_float from the ESBMC.

1.4 A.4 Genetic Algorithm Parameters Definition

In Table 3, we report a summary of experiments conducted to tune the parameters of the Genetic Algorithm, more precisely, the number of generations. For example, a NN with 2 layers would require a brute force algorithm to search for $52^2$ combinations of bits widths for the quantization. Similarly, a NN with 7 layers would require a brute force algorithm to search for $52^7$ combinations of bits widths. We conducted a set of experiments where we ran the GA one hundred times with a different number of generations options ranging from 50 to 1000. In addition, we fixed the population size to 5. From our findings, the GA needs about 100 to 110 generations per layer to find the optimal bit width solution for each run.

Table 3. Summary of experiments for tuning Genetic Algorithm Parameters.