We present the first end-to-end verifier of audio classifiers. Compared to existing methods, our approach enables analysis of both, the entire audio processing stage as well as recurrent neural network architectures (e.g., LSTM). The audio processing is verified using novel convex relaxations tailored to feature extraction operations used in audio (e.g., Fast Fourier Transform) while recurrent architectures are certified via a novel binary relaxation for the recurrent unit update. We show the verifier scales to large networks while computing significantly tighter bounds than existing methods for common audio classification benchmarks: on the challenging Google Speech Commands dataset we certify 95% more inputs than the interval approximation (only prior scalable method), for a perturbation of -90dB. Recent advances in deep learning have enabled replacement of traditional voice recognition systems with a single neural network trained from data (Graves et al., 2013; Hannun et al., 2014; Amodei et al., 2016) . Wide adoption of these networks in consumer devices poses a threat to their safety when exposed to a malicious adversary. Indeed, it was recently shown that an adversary can inject noise unrecognizable to a human and force the network to misclassify (Szegedy et al., 2013; Goodfellow et al., 2014; Zhang et al., 2017; Carlini & Wagner, 2018; Carlini et al., 2016; Qin et al., 2019; Neekhara et al., 2019; Yang et al., 2019; Esmaeilpour et al., 2019) , exposing a serious security flaw. Ideally, when deploying an automated speech recognition system we would like to guarantee that the system is robust against noise injected by an adversary. There has been substantial recent work on certifying robustness of computer vision models (Katz et al., 2017; Ehlers, 2017; Ruan et al., 2018; Tjeng et al., 2019; Anderson et al., 2018; Wong et al., 2018; Raghunathan et al., 2018; Dvijotham et al., 2019; Weng et al., 2018; Zhang et al., 2018; Salman et al., 2019; Gehr et al., 2018; Singh et al., 2018; 2019a; Wang et al., 2018; Singh et al., 2019b) . However, the audio domain poses unique challenges not addressed by prior certification work for vision. Differences between audio and vision models Concretely, while an input to a vision model is a raw image, audio models typically come with a complex preprocessing stage (that involves non-trivial non-linear operations such as logarithm) which extracts relevant features from the signal. Additionally, audio systems typically use recurrent architectures (Chiu et al., 2017) which computer vision verifiers do not handle as they focus on fully-connected, convolutional and residual architectures. This work We address both of these challenges and propose an end-to-end verification method for neural network based audio classifiers and an implementation of this method in a system called DAC (Deep Audio Certifier). Our threat model assumes an attacker can introduce a noise-based perturbation to the raw audio input signal. The goal then is to certify that, for any signal that the attacker can produce, the neural network classifies the signal to the correct label. We perform verification of this property using the framework of abstract interpretation (Gehr et al., 2018) . At a high level, the idea is to maintain an abstraction capturing all possible behaviors of both the audio processing stage and the neural network. The flow of DAC is shown in Fig. 1 where all abstractions are dark blue shapes. Here, all possible signals an attacker can obtain are captured using an abstraction s (i) (a convex relaxation). This abstraction is then propagated through the audio processing stage (shown in green boxes). The key components of this step are abstract transformers. For each audio processing operation (e.g. FFT) we create an abstract transformer which receives an abstraction representing an approximation of all possible inputs to the operation and outputs a new abstraction which approximates all possible outputs of the operation. The result of the audio processing stage is the abstraction x (i) . The shape x (i) is then used as input to the recurrent LSTM unit (light blue) which maintains an abstraction of a hidden state h (i−1) . LSTM consists of multiple operations and we create a custom abstract transformer for each of those. The result of the transformers in LSTM is a new hidden state h (i) . If this was the last frame in the signal (meaning i = T ), then hidden state h (T ) is passed through the fully connected layer of the neural network and, again using the abstract transformer, the final abstract shape a is obtained at the output (at the right of Fig. 1 ). Finally, to certify the property we check if each concrete output in the abstraction a classifies to the correct label (this is typically easy). If this is true, the output of the network is correct for all inputs that the attacker can create. Related work on RNN certification The work of (Ko et al., 2019) proposes the POPQORN verifier for recurrent neural networks (RNN). We note that POPQORN does not handle the audio preprocessing pipeline. Even though POPQORN cannot directly verify audio classifiers, their approximations for LSTM non-linearities can be integrated in DAC. This results in ≈ 200× slowdown with small decrease in the volume of the approximation. The massive slowdown makes their approximations unsuitable for certifying audio classifiers. In contrast, using our custom abstract transformers for LSTM non-linearities, DAC can precisely certify end-to-end robustness of challenging audio classifiers in few minutes. Our main contributions are: 1. A novel and efficient method to certify robustness of neural network audio classifiers to noise-based perturbations. The method is based on new abstract transformers which handle non-linear operations used in both audio processing and recurrent architectures. 2. An implementation of both verification and provably robust training in a system called DAC. We evaluated DAC on common audio classification benchmarks, showing it scales to realistic networks and is far more precise (97% to 2%) than the next best scalable method. We presented the first verifier for certifying audio classifiers. The key idea was to create abstract transformers for non-linear operations used in the audio processing stage and the recurrent network. These transformers compute an optimal (area-wise) approximation under assumptions representable in the underlying convex relaxation and enable sound handling of the entire pipeline. Our evaluation shows that DAC is practically effective and achieves high verification rates on different datasets. by the smaller volume under the each plane. Then for any x, y, f (x, y 1 ) < f (x, y 2 ) and f (x 1 , y) < f (x 2 , y). Thus, since z u x is independent to y, it is sufficient to show z We can easily know that f (x, u y ) is concave at x ≥ 0 and convex at x ≤ 0 by the second derivation of f . (a) Consider the case of u x > 0. Let x 0 be the x coordinate of the crossing of f (x, u y ) and . Again, by convexity of . Again, by convexity of With analogous steps, z l y can be shown to lie under the curve. Choosing the plane with larger volume underneath it allows to minimize the expected difference between the true curve and the lower bound plane under the randomly chosen domain. The proof of upper bounds will follow the same steps with the first case. z u x in this case is exactly same as before, but since f (x, y) goes below 0 when y < 0, z u y has to anchor at (l x , l y ) instead of (u x , l y ) since f (l x , l y ) ≥ f (u x , l y ) and convexity of f in the region. The proof steps do not differ much from the previous proofs. Again, the proof for lower bound is similar as before, but note that z l x needs to choose maximum between the two slopes. This is due to the sign of the values. Since f (u x , l y ) < 0 is the minimum in the region and it grows along x gets smaller, both D i f (u x , l y ) and f (ux,ly)−f (lx,ly) ux−lx are less than zero.
We present the first approach to certify robustness of neural networks against noise-based perturbations in the audio domain.
{"src": "scitldr-AIC_train", "paper_id": "HJxkvlBtwH"}