Certifying Neural Network Audio Classifiers
Authors: Wonryong Ryou
Mislav Balunovic
Gagandeep Singh
Martin Vechev
Venue:  (2020)
Keywords: Adversarial Examples
Audio Classifier
Speech Recognition
Certified Robustness
Deep Learning

Abstract: 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.

Under review as a conference paper at ICLR 2020
CERTIFYING NEURAL NETWORK AUDIO CLASSIFIERS
Anonymous authors
Paper under double-blind review
ABSTRACT
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 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.
INTRODUCTION
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. 20144] Ammodii al. 2016). Wide adoption of these networks in consumer devices poses threat to their safety when exposed to a malicious adversary. Indeed, it was recently shown that an adversary can inject noise unrecognizable
human and force the network misclassify (Szegedy et al.) 2013 Goodfellow
ct al. 2014 Zhang et al. 2017 Carlini & Wagner 2018, Carlini et al. 2016 Qin et al. 2019
Neekhara et al. 2019 Yang et
2019
Esmaeilpour al. 2019). exposing a serious security flaw.
Ideally, when deploying an automated speech recognition system we would like to guarantee that the system 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 Bunel et al. 2018 Ruan et al. 20188] Tieng et al. 2019 Anderson et al.) 2018 Wong et al.) 2018 Dvijotham et al. 2018 Raghunathan et al. 2018: Dvijothav et al. [019 Weng et al. 2018 Zhhan 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 noise-based per- turbation 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 high level, the idea 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. T where all abstractions dark blue shapes.
A 1--3
A
ATT-L
A
ReLU
ReLU
MyMM
800
Figure 1: End-to-End Audio Certifica- tion Flow using DAC.

---

Under review as a conference paper at ICLR 2020
Here, all possible signals an attacker obtain are captured using abstraction s (a convex relax- ation). This abstraction is then propagated through the audio processing stage (shown in green boxes). The key components of this step 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+))
The shape a:()) is then used as input to the recurrent LSTM unit (light blue) which maintains an abstraction of a hidden state h (5-1), LSTM consists of multiple operations and we create custom abstract transformer for each of those. The result of the transformers in LSTM is new hidden state (()), If this was the last frame in the signal (meaning i = T), then hidden state (T)) is passed through the fully connected layer of the neural network and, again using the abstract transformer, the final abstract shape is obtained at the output (at the right of Fig. [ Finally, to certify the property we check if each concrete output 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 preprocess- ing pipeline. Even though POPQORN cannot directly verify audio classifiers, their approximations for LSTM non-linearities
be integrated in DAC. This results in = 200 slowdown with small decrease in the volume of the approximation. The massive slowdown makes their approximations un- suitable 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 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.
2 BACKGROUND
We first define a threat model that we work with and then present all operations that are part of the verification procedure, including audio processing (MFCC) and LSTM updates. We also discuss the type of verification method we employ.
Threat model We follow the same attacker threat model as Carlini & Wagner (0088). The assumption that the attacker can add noise to the original signal s so obtain a perturbed signal s' + The measure of signal distortion are decibels (dB) defined as:
dB(s) max logio((ss)) do. dB( dBBss)
Note that the quieter the noise is, the smaller the decibel of perturbation (8, (it is usually negative value as it is quieter than the signal). We assume the attacker can generate noise ò such that (5) < c where is a constant defined by the threat model. Our goal is to verify whether the neural network classifies s' correctly for each small perturbation 5 (as constrained above).
Mel-Frequency Cepstral Coefficients (MFCC) Though there have been number of works which operate directly on the raw signal (Pascual et al.) 2017 Sainath et al. 2015), Mel-Frequency Cepstrum (MFC) traditionally preferred for audio preprocessing in speech recognition systems e.g., Deep- Speech (Hannun al. 2014). The idea of MFC is to model non-linear human acoustic perception as power spectrum filters based on certain frequencies, called Mel-frequencies. The final result of the transformation is vector of coefficients whose elements contain log-scaled values of filtered spectra, one for every Mel-frequency. This resulting vector is a feature representation of the original signal and can now be used in a downstream task such as audio classification.
Sahidullah & Saha 22012) presented an approach to represent MFCC computation using several matrix operations which integrate with our verification framework. Given T' frames of audio signals of
2

---

Under review as a conference paper at ICLR 2020
the length N 2 represented matrix S = [s(1) s(T) RTXN (tr for transpose), audio preprocessing with MFCC calculated using the following steps:
1. Pre-emphasizing and Windowing: Y = S(IN cpe N H
Transform the signal with the pre-emphasizing and applying the Hamming window. Here, IN RNXN is the shifted diagonal identity matrix (12)) +f =. otherwise 0),
H E RTN is the Hamming window, and Ope is the pre-emphasizing constant.
2. Power Spectrum of Fast Fourier Transform (FFT): @ (YW) @ (YW)
Perform FFT on the windowed data and square it to get the real-value spectrum. We can denote FFT on discrete domain (DFT) with the multiplication of Y and W E CNx//22
3. Filter Bank Log Energy: V log( (A)
Apply the Mel frequency filter bank to the power spectrum and get the log value of them.
A E N/2xp is the filter bank given the number of filters p, and log is applied entry-wise.
4. Dis(Dise Cosine Transformation): X DD
Perform DCT on the previous result. Again, this can be formulated using matrix multiplica- tion. We use the resulting X
(1) ... (T)) as the input for the neural network.
Long-Short Term Memory (LSTMM) LSTM architectures (Hochreiter & Schmidhuber 1997) are a key part in modern state-of-the-art speech recognition systems (Hannun al., [2014] Amodei et al. 2016 In our work, we consider the following definitions of updates in the LSTM unit.
fet (1) h W by
o (s) [xx(1) ht W. + b.
(4) (1) h (t- IW + b:
d [x( h (1-1)
We + ba
( (f o (t--1) + to(i
@ tanh (c))
(*)) = (ob))) o (*))
where [ is the horizontal concatenation two row vectors, W. and b. kernel and bias of the cell, respectively. At timestep 1, vectors {(() :0) % ((!) represent pre-activations of the forget, input, and output gate, respectively, and the pre-calculation of cell state. Cell state c(9) and hidden state (+) computed at timestep t are propagated to the LSTM unit at the next timestep, thus allowing it to maintain states. This recurrent architecture allows inputs with arbitrary length, making it especially suited for audio inputs.
Robustness certification In this work, our goal will be certify the robustness of audio classifi- cation pipeline (including the LSTM) to noise perturbations of the input. To build such a verifier, leverage the general method of abstract interpretation suggested by Cousot & Cousot (977). successfully employed by some of the most recent state-of-the-ar verifiers of neural networks (Gehr al. 2018 Singh et al. 2019a). The basic idea here will be to propagate the possible perturbations (captured by a convex region) through the operations of the entire audio pipeline and to then use the final output region certify the robustness property. The most challenging step of this approach is defining efficient yet precise approximations of the non-linear operations (called abstract transformers) used in the audio pipeline. In this work, we will introduce a number such new abstract transformers that handle the non-linear operations used in audio processing. Specifically, our over-approximation will be expressed in the recent DEEPPOLY abstraction (Singh et al. 2019a) (a restricted form of convex polyhedra) which aims to balance efficiency and precision. That is, the abstract transformer of a non- non-linear function will take as input a convex polyhedra element expressible in DEEPPOLY and output another polyhedra which over-approximates the behavior of the non-linear operation when invoked with any concrete point inside the original polyhedra.
3 OVERVIEW OF VERIFICATION PROCESS
We now explain the workings of our verifier on a (toy) example from the point where sound enters the processing stage where the output of the classifier is certified robust under any allowed perturbation of the threat model. Our goal is to provide an intuitive understanding, formal details are provided later.
Audio preprocessing Unlike in standard computer vision tasks where the input is fed directly to the neural network, audio models typically first perform MFCC preprocessing to extract useful features
3

---

Under review as a conference paper at ICLR 2020
PFT
[0)
(1)
42
310 20
+ +/
11
v1
(1)
10
+
ReLU
41
I1 A +.224
FB
(6)
2
W
of
+ 30f
4
(8)
12 x2
g(9)
(y/ y
10(0 (ng())))))
LSTM
4v1 (1)
2 0.07%1
200 0.86
4 2 0.185 +0000
0.33
(9) 51
0 4v (3)
$ 0. 0.058
+ 1.92
40 s (0.165
+ 0.390 0.86
2 S
(0)
5
0
622
0.010
1.85
4 0.088f 0.08
5/ S 0.0333
2.50
440 S <u.14e) + 0.45
Figure 2: Robustness verification illustrated on toy example. Each box shows the constraints computed by the verifier after processing given operation (shown on edges). Green color denotes elements of the MFCC audio processing stage: the Fast Fourier Transform (FFT), the Filterbank Transform (FB), and the Discrete Cosine Transform (DCT). Blue color denotes components of the network: ReLU layer, LSTM and Fully Connected layer. Approximations computed with this work are shown the bottom row. The operations which the abstract transformers handle are shown next. to the downward edges. Edges without labels represent affine transforms.
from the signal. We represent all preprocessing operations green boxes in Fig. 2 The calculation follows steps described formally in Section 2
using the same notation for resulting vectors.
Fast Fourier transform The first operation is Fast Fourier Transform (FFT) of the pre-emphasized input signal. It is a two-step process shown in dashed boxes in Fig. 2 We decompose it into affine and square operations which transform signal (4) into an intermediate representation ((), Using our novel and optimal abstract transformer for the square operation, formally defined in Section and
visualized in Fig. 3b, we obtain linear bounds on (())
Filterbank transform The next operation is Filterbank transform (FB) which consists of affine and logarithm operations, shown in solid boxes in Fig. Note that if the approximations from the square transformer allows negative values, then the entire analysis will fail as the logarithm operation is undefined for negative inputs. Our transformers are carefully designed to avoid this scenario. To obtain bounds on the output of the logarithm we apply our novel and optimal logarithm transformer, also formally described in Section 4 and visualized Fig. 3al and obtain linear upper and lower bounds on the log energy of the filtered power spectrum, tb(*) Logarithm operation is followed by Discrete Cosine Transform (DCT) resulting in vector a which is then used as an input to the fully connected layer of the neural network followed by a ReLU. Our analysis (detailed calculation in Appendix
C produces a E [0.87, 5.56]. (!)) E [0.17, 12.8). Since all the values are positive, the following ReL.U has no effect on its input and thus we set (1) (i() Using the back-substitution
technique we describe later, we derive z²{t) E [0.87, 5.56), n:(() E [0.17, 12.83). In the next paragraph we describe bound propagation through LSTM in more detail.
LSTM bound propagation Here we provide technical overview of our LSTM transformer, for- malized in Section and visualized in Fig. 4 by calculating the result of the transformation on the first neuron of the I.STM hidden layer. We provide detailed mathematical basis of this process in
Appendix D For our toy example, let the gates be updated as f(() x1() /4, input gate z5²) = 2h (t-1),
output gate of) 1: (c(11) and cell state z(t) (t-1) _1(() /4. Also, assume the previous states
are bounded by: 11(1-1), .n (t-1) o (1-1) of (t-1) o (x) y transformers to get bounds of the cell state ef = a - of ((-1)) + oii(() tanh()(").
E [0.90, 1.00). We now apply our o(x) tanh(y) and
0.18f + 0.45 - a(((() ) (t-1) < 0.16f(() - 0.58
0.032 (1) 0.78 < (((1t) tanh (c(1) < 0.39c(") + 0.28
Summing up the inequalities above results in a (-0.36, 1.46]. For the hidden state x0 (of()) (an)) we again apply our abstract transformer and obtain
0.48c(") - 0.08 < ()) tanh(c(") - 0.14g( 0.45
4

---

Under review as a conference paper at ICLR 2020
12
2x
log Mattle
+la
V" (uz + 12)x x
ugle
l
Al2x 412
U
3' log Lx
+
log
dx To
(a) Log abstract transformer.
(b) Square abstract transformer.
Figure 3: Our DeepPoly approximations of (a) the natural logarithm and (b) the square function. Blue lines represent the valid (in case of square, non-negative) upper and lower bounds which minimize the area between the planes under the given domain (a, uz]- The red bound on (b) grants smaller area, but contains the negative value, which occurs the analysis failure in the audio processing pipeline.
i.e. 111h) (-0.25, 0.65]. An analogous computation is performed for 12 For this example, we assume the computation results in l/2 = 0.
Robustness certification using DeepPoly The hidden states in the LSTM at the final timestep are passed through a fully connected layer without activation. In our example we assume that logits after the layer are obtained with the following formula: 1 1, + 0.24 and 12 h.g". These are shown in the final box of Fig. 2 To certify that the neural network classifies the input to class 1, we need to prove that 1 l2 > O. We now apply the back-substitution technique in Singh et al. (019a) upto the input to the LSTM:
4 12 = 11 A/t + 0.24 0.48(0.18f)) + 0.00af 0.33) 0.08 + 0.24
= -0009f + 0.01
( + 0.01 = 0.09(x("/4)) 0.01 -2 // + 0.01 2 0.006
As this value is greater than 0, robustness is established. The process above, of replacing variable with its constraints, is called buck-substitution. Here, we replaced I with 1,(") + 0.24, then 1,(0) with 0.18 0.185( + 0.03z(() 0.33 and so on. In Appendix C we show more detailed calculations to obtain tighter bound 0.0375 by also socssuubtituuiing in the preprocessing pipeline. For our experiments in Section we tune the number of fack-substitution steps to achieve good tradeoff between speed and precision. Note that robustness cannot be proved if one concretizes the expression above to an interval, instead of performing back-substitufe
of linear bounds. For instance, if we concretize 11(1) to 1-0.25, 0.65], we obtain 4 - l22 2 h h + 0.24 > -0.01 which is imprecise and fails to certify robustness. Note that if is not the last timestep. the hidden state and the cell state are passed to the next analysis timestep instead of computing the final output.
AUDIO PROCESSING TRANSFORMERS
As illustrated earlier, the first part of the verification process involves handling of the audio processing stage (performed using MFCC). Here, most matrix multiplication parts can be captured exactly by our abstraction, but MFCC also includes the square operation in the FFT and the logarithm operation in the computation of energy from filterbanks. Thus, to handle these non-linear operations, we need to create new abstract transformers, which we present next. To ensure minimal loss of precision, our abstract transformers minimize the area between the lower and upper bounds in the input-output plane. This approach of minimizing the area has been used before for other transformers and has been shown to be practically effective in (Singh et al. (2018) 2019a).
We denote the set of all variables in the analysis X. For element E X. denote the functions corresponding to its linear lower and upper bound as x' and x", respectively. These are scalar functions defined on R where & is the number of other variables used to compute z. For every element, we also maintain interval bounds, x E [Zz; ug] For ease explanation, we introduce the log transformer followed by the square transformer.
5

---

observe Under review as a conference paper at ICLR 2020
Log abstract transformer The logarithm operation is assignment y := log(z) where x, X.. The output of this operation cannot be captured exactly and we need to carefully introduce an approximation. Here, we first compute the minimum by = log(4z) and the maximum U (,)( which we use interval approximation. We define linear lower and upper bound functions y² ,²"" R - R. Using concavity the logarithm on any subset of the domain, the lower bound function is a line connecting the points (lz, log(())) and (uz, (wz). The upper bound function is chosen the langent line to the function minimizing the area between the lower and the upper bound. As result, we obtain the following bounds as depicted in Fig.
3a
(()) = =logl U2 - 1
l
log
Ur 12
y y²(x)
2r
log
M2 + 1
Ug + L1
Note that if l < 0, y (x) = -o0 since the function is not defined on that domain. We make an exception when ug 4g 10 to use interval bound for y' for avoiding the unstable floating point calculation caused by large denominator of x coefficient.
Square abstract transformer The square operation is an assignment y := x² where x, E X. Similar to logarithm, this operation is non-linear and cannot be captured exactly in the abstraction. We first compute the interval bounds of the output ly and My. and set the minimum value ly to 0 when 0 E [L,,, Uay] and min((", v otherwise. The maximum value My simply max(l", u²))
Next, define linear lower and upper bound functions y" y" IR - R. Using the convexity of the square function, we set the upper bound function y to the linear function connecting (l,, 12) and (u,, ) For the lower bound function y', we have be delicate: since x² : R22 our y should also be greater or equal than 0 within any domain. With the principle of minimizing the area between the bounds, we obtain the following bounds for cases as shown in Fig. 3b
F 412
0 < L1 < U2/3
4 4u
0 2 3uz > l
(x(x)
(x) = (ux + la)x - unlz
0
4. S 0 S U
(ur + 1x)x (lux + L2)
otherwise
LSTM TRANSFORMERS
Most prior work on verification of neural networks focuses on feed-forward or convolutional ar- chitectures whose operations consist of sequence of affine transforms and activation functions. However, to perform verification of recurrent architectures, one needs to handle the updates of the recurrent unit. Following the equations updating the LSTM presented in Section 2 that pre-activations of gates are affine transforms which can be captured exactly in our abstraction. However, the operations updating the cell and hidden states are non-linear and require approximation.
Overall, we have three elementwise products - two are between a sigmoid and a tanh and one between sigmoid and the identity. A straightforward approach to handling such transforms would be to concretize the polyhedra DeepPoly element to an interval and perform the multiplication using intervals. However, this approach would lose all relations between inputs and incur precision loss in future operations of the analysis. Instead, we design custom binary approximation transformers specifically tailored to handle the elementwise product in the update of the recurrent unit.
Sigmoid @ Tanh abstract transformer We define elementwise multiplication between sigmoid and tanh as an assignment == (z)) tanh(g), where z, y, X. As before, our aim is to construct linear bounds 2t_ z Unlike the previously defined DeepPoly transformers which take as input single abstract element, this transformer is the first which receives two abstract elements as operands. Hence, the bound functions have the form 2 z" 2 + IR
Let z = f(x, = (z) tanh(y). Our goal is to bound this function between two planes such that the volume between the planes is as small as possible (following first divide the computation into 3 cases based on the signs of ly and uy. To simplify notation, we introduce the variable assignment in Table I so that
previous heuristic). We
can reuse notation across all cases. We first define an anchor point a: a point in the box [L,, ug] x Iy, uyy where function f attains the max/min value defined upon the case. Also we need reference point whereas the plane would meet

---

Under review as a conference paper at ICLR 2020
Pi
min
min
min
min
by 2
Mars Myy
Myy Mly
leoty
lxy My
Max
121 Myy
min
max
miu
0.5
0
Up
Mas tly
Marg Bly
lxs My
br.4y
L..
1z, My
max
min
max
min
0.5
My <
a
lxs
la My
0
My. Mg.
4
Mys My
Table 1: Variable reference for the (x)) -tanh(y)) approximation.
Figure 4: Visualization of the bounding planes and (xx) tanh (y) curve.
first among the four corners it is tilted in given direction, other than the anchor. Our transformer computes candidates planes for the upper bound (z 25)) and two for the lower bound (z', 2/)) as:
(2"1²")= +b Dif(a), f(a) [(r))
(x -aa) + f(a)
0₂ rg
(="1z"), + Dzf(a)) f(a) [(r) ay Ty
(y any + f(a)
where D&f of Dyf= of and +, a, r are chosen from Table Finally, we choose bounds from two candidates which minimize the volume between the planes. Fig. $ the visualization of this result. We note that Sigmoid @ Identity transformer is handled in the same manner (we can directly apply the same transformer by replacing fx, y) with (x)) -g).
dr
.g
Theorem 1. Our Sigmoid @ Tanh transformer is optimal (it minimizes the volume between the lower and upper plane) under the assumptions: (I) bounding planes are tangent to the curve at the respective anchor points, (2) bounding planes are parallel to either or y axis. Planes computed using our transformer result in a volume strictly smaller than those computed using interval analysis.
We show the proof in Appendix B Our assumptions based on the following reasoning. The first assumption is need so that our transformer produces bounds strictly better than interval analysis. Unless 2 passes through the point (Ug, uy). the concrete upper bound would be larger than (uz)) tanh(uy). making it worse than an interval bound(analogoushy for the lower bound). The second assumption enables computation of optimal planes in O(1) while without this assumption one needs to solve non-convex optimization problem which is not feasible at the scale of networks we consider.
6 EXPERIMENTS
We now evaluate the effectiveness of DAC on several datasets and neural architectures. All our transformers are implemented in C (for performance) and exposed to the verifier using Python interface. We will publicly release the datasets, trained networks and source code of DAC. Verification performed on Intel(R) Core(TM) 19-9900K CPU 3. 3.60GHz using 6 cores for each instance.
Experimental setup We evaluate on audio classification benchmarks: Free Spoken Digit Dataset (FSDD) (Jackson/ 2019) and Google Speech Commands (GSC) (Warden 2018). FSDD contains 2,000 samples of spoken digits while GSC is more complex dataset containing 65,000 utterances of 30 short words spoken by thousands different people. State-of-thh--ar accuracy on GSC 96.9% by de Andrade et al. (2018) using attention RNN, while our verified model achieves 89%.
Robustness evaluation Following Singh et al. (2019b), we define success rate verification as the ratio between certified samples and correctly predicted ones. We randomly shuffled the test data and then, for every experiment, inferred labels one by one until the number of correctly classified samples provability.
reached 100. We report the number of provably correct samples out of these 100 As a baseline, we consider a verification method based on interval analysis, which only derives neuronwise lower and upper bounds using the previous layer's bounds. We used networks with
7

---

Under review as a conference paper at ICLR 2020
Verified rohustmess($)) (
Verified mhbsstness(S)
Verilied rohustness
100
DAC INTERVAL
100
100
60
40
40-
DAC INTERVAL
70
20-
-100
1221
-1.0
-50
-00
-180
120
100
-50
-00
-0
-101
-121
-100
-10
-00
noise (log scale)
dB
(log scale)
noise (log scale)
(a) undefended FSDD, 98%
(b) defended FSDD, 95%
(c) undefended GSC, 89%.
Figure 5: Robustness evaluation FSDD and GSC datasets, using DAC and Interval analysis.
40 hidden neurons and = 10 filters for both FSDD and GSC, Our results are shown Fig. 5
They suggest that DAC substantially outperforms interval analysis due to better approximations of key functions in both audio preprocessing and neural network stages.
Effect of back-substitution depth In this experiment, vary the depth of back-substitution used in DAC and study its effect our performance. We this experiment on an FSDD network and report the results in Table 2 We observe that increasing the back-substitution depth increases the provability. This is due to the fact that we benefit from cancellation of common terms in the propagated expressions, as demonstrated in our example in Section 3 However, this comes at a cost of exponential increase runtime. Thus, we choose to use depth 3 in order to get high verification rate while still having reasonable verification speed.
Depth
Provability($))
Run Time(s)
0
27
8.33
35
18.95
37
40.83
39
87.92
40
166.19
41
328.92
Table 2: Effect of sack-substitution
depth on the performance.
Provable defense for audio classitiers We also for the first time trained audio classifiers to be provably robust against noise- perturbations. Our training follows Mirman Mormmn al. (2018); Gowal et al. (2018) we perturb the input signal and propagate interval bounds through the audio processing and LSTM stages. To train, we combine standard loss with the worst case loss obtained using interval propagation. The resulting network shown in Fig. Sbhheeeeess 80% of provability for -80 dB even with the imprecise intervals, outperforming the undefended network. Even though this network was specifically trained be verifiable using intervals, DAC still outperforms intervals and proves significantly more robustness properties. Also note that defended network has lower accuracy of 95%, compared to the 98% accuracy of the baseline.
Experimental comparison with prior work POPQORN Ko et al. 2019) also proposes a method to certify recurrent neural networks by propagating linear bounds. One of the key differences with our work is the approximation of (zx - tanh(y) using linear bounds. We found that, in practice, optimization approach used by POPQORN produces approximations of slightly smaller volume than our LSTM transformer (although non-comparable).. However, this smaller volume comes at a high cost in runtime. We tried to integrate POPQORN bounds into our verification framework, however we found it not feasible for audio tasks it increased our end-to-end runtime 200 one of the smaller networks. In contrast, DAC takes only 1-2 minutes on average to verify a single example containing multiple frames. Indeed, observation is consistent with the evaluation of POPQORN in the paper where takes hours on a GPU for verifying NLP and vision tasks only for a single frame.
7 CONCLUSION
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 different datasets.
8

---

Under review as a conference paper at ICLR 2020
REFERENCES
Dario Amodei, Sundaram Ananthanarayanan, Rishita Anubhai, Jingliang Bai, Eric Battenberg, Carl Case, Jared Casper, Bryan Catanzaro, Qiang Cheng, Guoliang Chen, al. Deep speech 2: End-to- end speech recognition in english and mandarin. In International conference on machine learning, pp. 182, 2016.
Ross Anderson, Joey Huchette, Will Ma, Christian Tjand raatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. arXiv e-prints, pp. ar 1.01988, 2018.
Rudy Bunel, Ilker Turkaslan, Philip H.S. Torr Pushmeet Kohli, and M. Pawan Kumar. A unified view of piecewise linear neural network verification. In Proc. Advances in Neural Information Processing Systems (NeurIPS), pp. 4795-4804 2018.
Nicholas Carlini and David Wagner. Audio adversarial examples: Targeted attacks on speech-to-teks In 2018 IEEE Security and Privacy Workshops (SPW), pp. 1-7. IEEE, 2018.
Nicholas Carlini, Pratyush Mishra, Tavish Vaidya, Yuankai Zhang, Micah Sherr, Clay Shields, David Wagner, and Wenchao Zhou. Hidden voice commands. In 25th {USENIX} Security Symposium ({USENIX) Security 16), pp. 513-530, 2016.
Chung-Cheng Chiu, Tara N. Sainath, Yonghui Wu, Rohit Prabhavalkar, Patrick Nguyen, Zhifeng Chen, Anjuli Kannan, Ron J. Weiss, Kanishka Rao, Katya Gonina, Navdeep Jaitly, Bo Li, Jan Chorowski, and Michiel Bacchiani. State-of-the-art speech recognition with seeuunce----- models. CoRR, abs/ abs/1712.01769 2017. URL http:: wwtp://wwww.xpp///////222... 017669
Patrick Cousot and Radhia Cousot. Abstract interpretation: unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238 200-25524442 ACM, 1977.
Douglas Coimbra de Andrade, Sabato Leo, Martin Loesener Da Silva Viana, and Christoph Bernkopf. A neural attention model for speech command recognition. arXiv preprint (80.:18888009999 2018.
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. Proc. Uncertainty Artificial Intelligence ( (UAI). pp. 162-171, 2018.
Krishnamurthy (Dj) Dvijotham, Robert Stanforth, Sven Gowal, Chongli Qin, Soham De, and Push- meet Kohli. Efficient neural network verification with exactness characterization, In Proc. Uncer- tainty in Artificial Intelligence, UAI, pp. 164, 2019.
Rüdiger Ehlers. Formal verification of piece- wise linear feed-forward neural networks. In Automated Technology for Verification and Analysis (ATVA), 2017.
Mohammad Esmaeilpour, Patrick Cardinal, and Alessandro Lameiras Koerich. A robust approach for securing audio classification against adversarial attacks. arXiv preprint arXiv: 10990, 2019.
Timon Gehr, Matthew Mirman, Dana Trachsler-Cohen Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3-18. IEEE, 2018.
Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. arXiv preprint
2014.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ucsato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint 1rXiv:1810.12715. 2018.
Alex Graves, Abdel-rahman Mohamed, and Geoffrey Hinton. Speech recognition with deep recurrent neural networks. In 2013 JEEE international conference on acoustics, speech and signal processing, pp. 6645-6649. IEBE, 2013.

---

Under review as a conference paper at ICLR 2020
Awni Hannun, Carl Case, Jared Casper, Bryan Catanzaro, Greg Diamos. Erich Elsen, Ryan Prenger, Sanjeev Satheesh, Shubho Sengupta, Adam Coates, et al. Deep speech: Scaling up end-to-end speech recognition. arXiv preprint arXiv: 2014.
Sepp Hochreiter and Jürgen Schmidhuber: Long short-term memory. Neural Comput., 98): URL htt:///d
1780, November 1997. ISSN 0899-7667. doi: 10.1 10.1162/neco.1919
foi.org/10 www11166eenco. 1997.9.99.... 87135
Zohar Jackson. Free spoken digit dataset. Etee-sooken-dicit-otttess 2019.
Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97- Springer, 2017.
CY Ko, Z. Lyu, TW Weng, I. Daniel, N Wong, and D Lin. Popqor:: Certifying robustness of recurrent neural networks. In International Conference on Machine Learning (ICML), 2019.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning, pp. 3575-3583, 2018.
Paarth Neekhara, Shehzeen Hussain, Prakhar Pandey, Shlomo Dubnov, Julian McAuley, and Farinaz Koushanfar. Universal adversarial perturbations for speech recognition systems. arXiv preprint arXiv:1905.03888, 2019.
Santiago Pascual, Antonio Bonafonte, and Joan Serra. Segan: Speech enhancement generative adversarial network. arXiv preprint vrxivv1703.094522 2017.
Yao Qin, Nicholas Carlini, Ian Goodfellow, Garrison Cottrell, and Colin Raffel. Imperceptible, robust, and targeted adversarial examples for automatic speech recognition. In International Conference on Machine Learning (ICML), 2019.
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems (NeurIPS), pp. 10877-10887. 2018.
Wenjie Ruan, Xiaowei Huang, and Marta Kwiatkowska. Reachability analysis of deep neural networks with provable guarantees. In Proc. International Joint Conference Artificial Intelligence, IJCAI, pp. 2651-2659, 2018.
Md Sahidullah and Goutam Saha. Design, analysis and experimental evaluation of block based transformation in mfce computation for speaker recognition. Speech Communication, 54(4): 543-565, 2012.
Tara N Sainath, Ron J Weiss, Andrew Senior, Kevin W Wilson, and Oriol Vinyals. Learning the speech front-end with raw waveform cldnns. In Sixteenth Annual Conference of the International Speech Communication Association, 2015.
Hadi Salman, Greg Yang. Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. CoRR, abs//192..0872. 2019.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems, pp. 10802-10813, 2018
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POL))41, 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations, 2019b.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint 132.v 2013.
10

---

Under review as a conference paper at ICLR 2020
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, (ICLR), 2019.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks, In Advances in Neural Information Processing Systems, pp. 6367- 6377, 2018.
Pete Warden. Speech commands: A dataset for limited-vocabulary speech recognition. arXiv preprint 0r04. 03209, 2018.
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song. Cho-Jui Hsich, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks. In Proc. International Conference on Machine Learning (ICML), volume 80, pp. 5276-5285, 2018.
Eric Wong, Frank R. Schmidt, Jan Hendrik Metzen, and J. Zico Kolter. Scaling provable adversarial defenses. In Proc. Neural Information Processing Systems (NeurIPS), pp. 8410-8419, 2018.
Zhuolin Yang, Bo Li, Pin-Yu Chen, and Dawn Song. Characterizing audio adversarial examples using temporal dependency. 2019.
Guoming Zhang, Chen Yan, Xiaoyu Ji, Tianchen Zhang, Taimin Zhang, and Wenyuan Xu. Dolphi- nattack: Inaudible voice commands. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp- 103- 117. ACM, 2017.
Huan Zhang, Tsui-Wei Weng, Pin-Ye Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems, pp. 4939-49444 2018.

---

Under review as a conference paper at ICLR 2020
A SOUNDNESS PROOF OF SIGMOID C TANH ABSTRACT TRANSFORMER
Suppose x and are the abstract variable bounded by [4,, Uz], 14y1 Uy] respectively. This suggested transformer finds the bounding planes of the function fxz y) ozx tanh(y). Let D&f Oz
of and
81 D₃S 04
1. 1 2
Choose the upper bound of the function between 2/x² and 2y. where
2 (x, y) min (Dff uy), I (uz Uy) [1(1,, Uv) (x -ux) f(ux, Uy)
Ux - 11
*,, v) min Dzs(uz, uy); f(uz, Uy) - -fuus My ly
(y (uy) [(un Uy)
by the smaller volume under the each plane.
Claim 1: (2, y) 2 f(z, y) in (x, y) E [lz, ugl x Bly Uy).
Let x1 < z2 E [l uz] and y1 < y22 E Iyy unl. Then for any x, y, f(z, < f(x, y2)
and f(1 y) < f()2, Thus, since 2 is independent to y, it is sufficient to show
(2, ) 2 f(r
We can easily know that [xx uy) is concave at x 2 0 and convex at S 0 by the second derivation of f.
(a) Consider the case of u2 > Let Tn be the x coordinate of the crossing of f(x, (y) and g(x) = (uf( My (x uxx)) - [(uz, uy). From the convexity of f (ar, Myy in x < O. g(0) > f(0, ug). and gx(x) > 0, there exists a single xo < O. If Le > To. the slope of (x, becomes Dif Uy). and 2 and g become identical. Hence, f(z, uy) S becomes
Then z and g shares point of un but 2 has smaller slope, so g(x) S 2 (I.-) in Un]. Also from flz, uy)) = 2 (Iz,-) and f(0, uy) < (0, -). f(, Uyy S 2 (z..). Thus, the claim holds when U > O.
g(x) = (z, If l I Zp, the slope of (x, becomes "yM..,))-((eed
(b) Another case of un < 0, x coefficient of z will always be ((ue,u))ffl2z0l Again, by convexity of fxz uyy) 2 (x, 2 f(z, uy).
Hence 2 (x, 2 f(x, 2 f(z v) holds in (I, E [l,, ug] x Byy uy]. Claim proved. With analogous steps, 2i can be shown to cover above the curve. Choosing the plane with smaller volume underneath it allows to minimize the expected difference between the true curve and the upper bound plane under the randomly chosen domain. For the lower bound, choose the upper bound of the function between 24 and z,,, where
(x, = min (Dis(
f(ln by) - f(uar (y)
)
(or (o- (u--1a) (a)) -a)))) 1x)-f((mm) f(las
1/ Ux
(x(,,) = min (Df((e.sh)) S1 ly) [1ass Wyy)
(3 - (b) - f(laslty
by My
by the larger volume under the each plane.
Claim 2: 21 (x, S f(x, v) in (I.1) E [1,, un] x Uog uy]. It is sufficient to show (2, .) 2 f(x, since f(r, v1) S f(x, y2) for y1 S y22
(a) Consider the case of l, < 0. Let ao be the coordinate of the crossing of [ax by)
and g(x) = Def(le, (x: - (z) - flz. 1g). From the concavity of f(z, ln) in x > O. g(0) < (0) and g/ (z) > 0, there exists single 20 O. If L. < 20, the slope of (x, -) becomes Dif(le, (y), and 2 and y become identical. Hence, f(z, (y) S g(z) = (x,)). 1f 2 zg. the slope of .x( becomes 1(.....) H(ndd)))) Then 2f and g shares point of le but of has smaller slope, so g(x) > 2 (z .) in ugl-
1. -
Also from f(u,, = 2 (ugs and f(0, 1n) > (0..). f(x, (n) 2 2 (2. Thus,
the claim holds when u 0.
12

---

Under review as a conference paper at ICLR 2020
(b) Another case of L2 2 0, coefficient of 2 will always be ((lad))-((ual Again, by convexity of f(2,4) 2 (z, :) I f(x, (y).
Hence 2/ (x, S fzz (,) 2 f(z, y) holds in (a. y) LL. 2,2 B Myl- Claim proved.
With analogous steps, 24 be shown to lie under the curve. Choosing the plane with larger volume underneath allows to minimize the expected difference between the true curve and the lower bound plane under the randomly chosen domain.
2. b 5 Uy
The proof of upper bounds will follow the same steps with the first case. 2 in this case is exactly same as before, but since [(r, y) goes below 0 when y/ < O, z has to anchor at (y) instead of (ur,ly) since [(...1g ln) 2 f(uz, and convexity of f the region. The proof steps do not differ much from the previous proofs.
Again, the proof for lower bound is similar before, but note that z needs to choose maximum between the two slopes. This is due to the sign of the values. Since I' [Uaz, by) < 0 is the minimum in the region and grows along æ gets smaller, both Dif by) and f(w, (,) f(ladd)) are less than zero.
3. 0 By
We will not provide the proof since this case is symmetric to the first case.
B PROOF OF THEOREM
Theorem 1. (copied) Our Sigmoid Tanh transformer is optimal (it minimizes the volume between the lower and upper plane) under the assumptions: (1) bounding planes are langent to the curve at the respective anchor points, (2) bounding planes are parallel to either x or y axis. Planes computed using our transformer result in a volume strictly smaller than those computed using interval analysis.
Proof. First note that =² 2g: 2/, "y are sound bounds by Appendix A Assume N. is chosen as the upper bound. W.l.o.g., suppose there exists another sound candidate upper bound C satisfying (I) and (2), with smaller volume underneath it than z.. Then & would have larger absolute slope x than 2 However, the slope of 2 is chosen as stiff as possible while remaining the soundness (Appendix to see in detail). Hence, C would not be sound anymore with larger absolute coefficient.
Contradict to the existence of sound Gr Other cases can be proved with similar logic as well.
C VERIFICATION BY EXAMPLE
We assume the last sound frame (() consists of two elements 8 and 82 such that: " E [0, 1] and
822 E [-2,, -1]. These constraints capture noise perturbation of the sound and are depicted the white box in the left part of Fig. 2
We describe analysis only at the last timestep (the same process
repeated for every timestep).
We note that the DeepPoly abstraction (which we build on in this work) maintains four constraints for every element: a lower and upper constraints which are linear in terms of the previous elements as well as two interval constraints. This abstraction is exact for affine transformations, however, to handle non-linear operations, one has to create new abstract transformers. In our work we introduce such transformers and formally describe their operation in the next sections. In what follows, show their effect on our running example. For the presentation below, our figure shows the linear constraints obtained by the verifier, but avoid visual clutter, we do not show the two interval constraints (however. we do list them in the text).
Fast Fourier Transform The first operation in the audio processing stage is the Fast Fourier Transform (FFT) of the pre-emphasized input signal. It is two-step process shown in dashed boxes Fig. 2 The preemphasis is in fact an affine transform so we perform it jointly with the affine transform in the FFT. As the composition of two affine transforms is again affine, this
13

---

Under review as a conference paper at ICLR 2020
amounts to single affine transform the input. In our example, the composed affine transform is v1
8
(e)
52 and y/
(t)
28. Affine transforms can be captured exactly and here we obtain e.g..
(0) (1)
(t) We also obtain the interval bounds y/ E [1,3] and (!) E [-4, 2].
$1 22
S D1
$2
The next step in the computation of FFT is elementwise square of y (t) We denote this operation as 0 (u) )² and 089 (222 )2 The square operation is non-linear and cannot be captured exactly which means that we need to decide how to lose precision. Here, we apply our new square abstract transformer (formally defined in Section 4) which provides an optimal linear lower and upper bounds of the square function in terms of area. After applying this transformer, we obtain the bounds:
1y1 -4
of S 4yi -3
-6y2 (t) - - 650 S <-6y
The interval bounds are calculated by:
0 2 401
4(s) - (1)) 42 2 4(0 - (-1)) -
8(0) S 401 (0) 3 4(51)) 53
(0) 3 < 4(1 - ((22) - 33
80 Z 682
(1) - 9 = -6(28) (1) 9 2 -6(2 (-1)) -9
0 < 682 - 8 = -6(2s - 8 < 66(2 (-2)) -8 = 16
(t)
Hence, 8 E [0. 9) and 0 E 3. 16). Note those bounds are not exact but sound; even yf E [1,3]
and 1/2 (2) [-4,--2 DAC calculates the concrete lower and upper bound with the expression to be consistent with other transformers, so the bounds might not be exact as [1, 9] and [4, 16]. In practice, FFT is followed by another affine transform which adds together the real and complex component of each element, but we omit this for clarity as is captured as before, without loss of precision.
Filterbanks Transform
computatinn of filter banks of the input, Our analysis continues with the computation
shown in solid boxes in Fig.
The first step is an affine transform and in our example we use: J0
20 + o and / 8
(0 Our abstraction is again exact here and additionally computes interval bounds w [3, 34] and 7(r) E [9, 57]. The final step in this transform is the elementwise
+
logarithm of the input. We denote the operation as w log(w5 ((0) and uh (og())))). As this is
again a non-linear operation, we apply our new log transformer so to obtain:
0.0783x7 (1) + 0.8637 S <w( < 0.0541 ((0 + 1.9178
0.0384 (1) 1.8511 2/2 < 0.0303 700) 2.4965
The interval bounds are calculated by:
3/ N 0.0783.310 700 + 0.8637 - + ( + 0.8637
0.0783(20() N 0.07) -4 + (-6y," 9)) + 0.8637
= 0.0783(2(4($)) - -/ 4) + (-6(2) - 9) + 0.8637
- 0.6264. - 1.566s - 0.4674 1.0986
9 < 0.0541 (00) + 1.9178 (20541(20()) + (b()) + 1.9178
< 0.0541 (0) - + (-6y) -8)) + 1.9178
0.0541(2(4(0 (t) 3/ (1) 3) (-6(2.))) - 8)) + 1.9178
- 0.4328s (4) 1.082s 82
(0) 1.1604 < 3.7572
14

---

Under review as a conference paper at ICLR 2020
11) 2 0.0384 1.8511 0.0384 +30 + 1.8511
2
2 0.0384((4v) - 44+ 99) + 1.8511
=
-))
9) + 1.8511
0. - +0.6666
0.6607 2.1967
9
S 0.0303 ((0) + 2.495 0.0303(0)) 230 + 2.4965
2
S 0.0303 (44) (1) - 3) + 3 - -8) + 2.4965
0.0303 (4 (0) ) - 3) + 3(226))) 8)) 2.4965
0.12128 1.21282
(0) 1.6784 < 4.2236
1919 4.2236]. Again, these bounds are sound since [log 3, log 34] 110986, 3.7572), [log 9, log 57] [2.1967, 4.2236].
In other words, v1 E
1. 11.0966.3 3.7572 and 202
Discrete Cosine Transform and ReLU After the Filterbanks Transform, the input is passed through the Discrete Cosine Transform (DCT) followed by Lifting operation. The analysis result of these steps is then provided as input
fully connected (FC) layer followed by ReLU activation. To ease presentation, in our example we combine DCT, Lifting and FC layer in a single
affine transform: x
ub - -bbb") + 4 and 2 4w11 (t) We show this transform in dotted box in Fig. 2 This again captured exactly in our abstraction along with interval bounds
i1 E [0.875, 5.5655.. 222 E [0.1708, 12.8321). The affine transform is followed by ReLU
=11)
activation x = max(0, (0, (()).. x2 = max(0, ). In general, we use the ReLU transformer
(t) defined in Singh al. 2019a), which for this example produces: z/() = (t)) and x2 =
LSTM analysis After the verifier completes the audio processing stage, its output is passed as input the LSTM cell. This cell also receives hidden state and cell state from the previ- ous timestep (shown as a blue box in Fig. D In our example, we assume these are given as: nn((1))
-i(-1),n _ ci ((-1) ((-1) E [0.9, 1]. We note that these elements usually have different interval bounds, but for simplicity in our example we use the same intervals. We focus on the first neuron in the LSTM and compute pre-activations in example for the forget gate f(() x²() /4, input gate
{(() = 2h (t-1)) output gate ( h (t-1) and cell state z(t) = h (1-1) x22 /4.
In order to update the cell state, need to compute: c/ o ( d'- t (il))) tanh (c()). The left and right summands are computed using our new binary abstract transformers for (x)) and or (x)) tanh(y) expressions, respectively. Applying our abstract transformers the summands produces the following bounds:
0.18915(" + 0.4576 {(S(()) of ((-1) < 0.1596f 0.5787
0.0341c - 0.7847 S <a(((o) tan)( < 0.3945c( + 0.2769
Summing up the above inequalities grants the upper and lower bounds of (tt) in terms of x1), h (t-1), and (tt-
d0 0.1891 + 0.03112 0.3271
(9 =01191 0.0341 - = /4) 0.3271
+
2 -03644
d0 0.1596 (() + +..9455a + 0.8556
0. 0.1596(2
(1) (2) + 0.3945(1) (t-1) - -z -/////// /4) + 0.8556
< 1.4551
and get of E [-.36444, 1.4551]. We omit the back back-substitution steps since do not lose precision the affine transformations from (t) and note that this calculation is based the assumption
(t)
15

---

Under review as a conference paper at ICLR 2020
that the bounds of (()) and cl*-1) are given constant. In practice, we recursively apply the process for those vectors to express the bounds in terms of xx((), (x-(1),,.. ,''.
The next hidden state is computed ni - =o(f tanh(c)"). We apply our abstract transformer for the (z)) tanh(y) expression, we obtain:
4 z 0.4906c (0) 0.0764
0.4906(0.189151" + 0.0341ē 0.3271) 0.0764
-0.2551
& 0.1433c| 0.4477
0.1433) + 0.3945c 0.8556) 0.4471
0.6556
i.e., 11 E [--0.5551 256,,0.65666) An analogous computation is performed for (t) In this example we will assume h concretely.
Robustness certification using DeepPoly The hidden states in the LSTM at the final timestep are passed through a fully connected layer without activation. In our example assume that logits after the layer are obtained with the following formula: I ( + 0.24 and = n! These are shown in the final box of Fig. 2 To certify that the neural network classifies the input to class 1, we need to prove that 4 la > O. We now apply the same back-substitution technique as (Singh et al. (2019a):
41 - l/ n1 - 0.24
2 (.4906 0.0341c - 0.3271) 0.0764 + 0.24
0.00277/" 0.0031
-.020777//) (///4/ 0
((-
(1)
0.0231 (4) - [
0.0042.
0.0181
(applying concrete bound to A (t-1)
demomstration
0.0231
(L.231((/1))) (4)
+ + - 0.0042
1/2
(0) 0.0181
0.0063
(0) 0.01899 (0) + 0.1105
halt the computation and plug the bounds 2 0.0063 1.0986 0.0189 4.2236 + 0.1105
0.0375
For the purpose of demonstration, we stop here and plug previously obtained interval bounds for (b((), As this value greater than O, robustness is established.
D MATHEMATICAL DERIVATION OF LSTM TRANSFORMER
LSTM cell receives not only the resulting neurons from the pre-processing stage but hidden state and cell state from the previous timestep. To incorporate with all those incoming values, we extend the scope of the LSTM equations defined in Section 2 Let d be the dimension of the input and h be the dimension of states of the cell. To standardize the operations performed within the LSTM cell, append 0axd [0]axa and 022 [0], below each kernel and bias respectively express the formula as
f (x((),((1))) (1-1) ((-))) + b'r
0g [x) h (t-1) (c( W + +b
(1)
(1) (t), (t-1) (t-1) + b
C = [x) h (e-1) cle-l) W!
+ by
40
16

---

Under review as a conference paper at ICLR 2020
100
-2
88
y
Figure 6: (xx) tanh(y) boundings on [-30.7, 107] [-9.87, -0002.. Orange plane is obtained
from POPQORN and blue plane is from DAC.
Then the cell state and hidden state computations can be rewritten
e = (fo o (L-1) + o (1) (1)
@ (an)(a())
<(x t (1 1 + b,) @ ([x(") h (t1),, (000"100x(
+ [0x h (1-1) ((--1) W + by) o tanh((x!0) (1-1), ( (01-1/]// + bo2)
(2)
(0 a(ob (0) tanh(c
= ()x( (t-1)
W + bb) @ lanh(c!")
5 f(x, y) = ozx) tanh(y) and g(x, y) = oz() y can be bounded with two planes regarding the operands' lower and upper bounds. In other words, for any given two real values, v, y E IR, x E [L,, Mz], E (,y. My] our finding guarantees the planar bounds of f and y with the coefficients built by linear combination of las Uzy bys My. For single neuron oj (t)
As is described in detail in Section
in (!)) the upper bound can be expressed from Eq. 2
(e) = [0 (t-11), clt ( + (b/]l) (Ix(t)) A (0-11 clt 10 (m)):
fl.s
+(((x!))) (t-1), (t-1)) [ [b(], tanh(( (t-1) (1_1)) d + (b/li)
S (lx (t-1) c [W]) (b)1,) + B., ((x (t-11) (t 110 [Alia]] I") C.
+ (a h (t1)) "'""""[[".... + (b1,) + (ux (t-1), df dW"'s (bl)) + F
=x w. + h (1-1) un + ((--1)
where Ag. Fu are calculated real values by Section 5 and w. and are the simplified linear coefficients of each vector and bias term, respectively. We also can get the upper bound of n.50 by plugging Eq. in Eq. (3). and similarly for the lower bounds of those states.
Note these linear bounds makes possible to recursively apply this step to get desired bounds, and can be branched in any depth for the trade-off between the precision and the complexity.
E COMPARISON BETWEEN DAC AND POPQORN
In this subsection we provide in-depth comparison between our approach and POPQORN (Ko et al. 2019) which provides another way to bound a (x) tanh(y) and (xx) y non-linearities. Before the experiments, we discuss comparability between three methods to bound the non-linearitis interval, DAC and POPQORN. Then, we perform three different experiments. First, we compare volume of bounds produced by both POPQORN and DAC on set of synthetic test cases. As these test cases do not reflect the actual test cases which occur during the verification of audio benchmarks, in the second set of experiments Finally, in the third experiment we plug in POPQORN bounds into our framework and show its certification performance on the audio benchmarks.
compare the methods
set of test cases from one of our benchmarks.
17

---

Under review as a conference paper at ICLR 2020
DAC
POPQORN
0.2
0.4
0.6
0.8
Figure 7: Volume comparison with interval bounds with synthesized data. Excluded outliers.
-100BB certified
-80BB certified
-80dB uncertified
-60dB uncertified
0.2
0.4
0.6
0.8
1.2
1.4
Figure 8: Volume comparison with interval bounds with data from the working pipeline. Excluded outliers.
Comparability of different bounding methods We say that methods and are pairwise non- comparable if there exists an input for which method A produces tighter bound than method B, and vice versa. Given this definition, POPQORN is con-compaaable with our method. To demonstrate this, in Fig. 6 we show case where this behavior is manifested. Here, for y S -1 POPQORN (shown as orange plane) produces tighter bound than DAC (shown as blue plane). However, for other entire range of inputs where -10 I y S 2, POPQORN bounds substantially worse than our bounds. Further, those bounds are even worse than interval bounds and the overapproximation error is not bounded. Contrary POPQORN, our bounds always strictly better than interval bounds (this is proven in Theorem 1 and distance between the function and our planes is bounded.
Comparison on synthetic test cases In this experiment, we compare bounds produced by POPQORN and DAC on set of synthetic test cases, unrelated to the certification of audio classifiers. Both methods take 1,, uy and ly, Uy as bounds for the input to the sigmoid and tanh, respectively. We sample those inputs uniformly from [-2, 2] x [-2, 2] and compared the volume between the curve a (x)) Lanh(y) and bounding planes produced by both DAC and POPQORN. The volume was computed using 1000 Monde Carlo samples in the set [L. Uz]] [,y, My.] Since there two (xx) tanh(y) and one (xx) y calculation appearing in single LSTM cell, we run the experiment with such portion of data. In other words, in 67% of experiments
bound (x:) tanh(yy) and in 33% we bound (xx) y. We sampled 100 such inputs and compared the volumes obtained by POPQORN and DAC with the volume obtained using interval.
The distribution of volumes is shown in Fig. 7 Here, stands for the same volume as interval bounds and values less than I indicate performance better than intervals. We conclude that, for this experiment, POPQORN bounds produces smaller volume than our method - 0.2 compared to 0.37. In terms of runtime, POPQORN takes 14.37 seconds on average while the bound calculation of DAC finishes in few milliseconds.
Direct comparison on test cases from audio benchmarks The previous experiment may not reflect the actual performance audio benchmarks that consider in this work. We uniformly sampled the arguments Lz. uzz ly, Uy that our transformer for (x) tanh(y) and (zx) y was invoked corresponding to different perturbation ranges and then
with. We distinguish between test further split it into certified and uncertified samples. For each of the cases, Fig, g shows the box plot of the distributions of volumes produced by both POPQORN and DAC.
18

---

Under review as a conference paper at ICLR 2020
Verified robustness(())
Verified mhustness(Si)
100
DAC INTERVAL
100
DAC
INTERVAL
42
43
1000
-101
-01
-70
-10
-90
-100
-50
-00
-10
-00
-00
noise (log scale)
noise (log scale)
(a) undefended FSDD, 98%
(b) defended FSDD, 95%
Figure 9: Robustness evaluation FSDD with error bars.
We found that, while overall POPQORN bounds work well in practice, they frequently produce bounds less precise than interval bounds. The reason of this malfunctioning comes from the limitation of gradient descent approach employed by POPQORN. The gradient of the function, which POPQORN uses to search for the optimal bounds, is large when the inputs distributed near O. However, if the inputs are far from the origin or are too close to each other, the function curve becomes almost flat, gradients are close gradient descent is not guaranteed to find the bounds with minimum volume. Fig. [howsw one of the examples where POPQORN fails find lower planar bound which produces minimum volume. On the contrary. the resulting value of (xx) tanh(y) is within [-1.1] regardless of the magnitude of arguments which means that the error produced by intervals bounded. As our planar bounds are strictly better than intervals, regardless of input conditions, our error is also bounded.
and gradient descent has problems converging. Also, in other cases,
Plugging in POPQORN bounds into DAC We also experimented with using POPQORN bounds instead of our bounds in the pipeline and compared the final adversarial regions with those resulting from DAC. As POPQORN is relatively slow (108 minutes per sample), we performed this experiment only the first 10 inputs with - B perturbation. Using their bounds results in 0 verified samples, while DAC verifies samples. We believe the reason here is the existence of many pathological cases as described in the previous point where gradient descent used by POPQORN converges suboptimal solution which ends up being worse than interval bounds. These errors are further propagated through each frame and resulting output can not be certified.
F SENSITIVITY OF PROVABILITY METRIC
In our experiments, followed the convention of provability measurement from Singh al. (2119)). Here, we also provide the result with error bars from 10 independent repetitions with randomly permuted test set. For each repetition, we randomly permute the test set with the different seed and collect the first 100 samples with the correct prediction under zero perturbation from the ordered set. We then count the number of certified inputs from those samples represent the provability under the given constant e. Fig. [ shows that provabilities do not differ much from the reported results for multiple experiments.
G TRAINING WITH PROVABLE DEFENSE WITH IBP
Here give more details on training procedure for provably defended network which follows Mirman et al. 2011 8): Gowal et al. (2018). Let 2 (c) and B be the resulting lower and upper bounds for the final logit E Rdth under the perturbation size e, with the true label j E {0, -.. , 1}.
We define the worst-case logits (E) as
(c) i= (2)
2,(e)
i4j
which corresponds to the worst concrete logits under the given imput with the predefined perturbation amount. Recall that say the input is certified when this worst-case logits satisfy arg max, 2,
19

---

Under review as a conference paper at ICLR 2020
Verified robustness( (6))
100
DAC INTERVAL
-120
110
-100
-90
-60
-70
-80
50
dB noise (log scale)
Figure 10: defended GSC, 82%.
params
FSDD
GSC
Frame size N
256
512
Frame step 8
200
400
Number of filters p
10
10
Hidden neurons
40
40
Learning rate
0.001
0.001
Batch size
5
50
Table 3: Model parameters used in the experiments.
Training loss L is a linear combination of the standard cross-entropy loss ((z, e(i)) and the worst-case cross-entropy loss 1(2, e(i)) where e(i) is target one-hot vector, i.e..
L(t') <<t't((()))) (tt')((z, e (1 (()=K())((E(((())))))
Note that we set up the x and as the function of t'. As in Gowal et al. 2018). gradual in- crease/decrease of these parameters during the training was essential get desired performance. We set these functions with respect to the number of training epochs E as
[ I/E E/2 x(t)
11/2
otherwise
<(t) -0 (200 70)
Also, to track the training speed, we increase one by one t' only we are achieving 85% of standard accuracy and 80% provability at the current setting. The models were built under the 60.
We also attach the missing result of defended GSC with 82% concrete accuracy in Fig. 10
H MODEL PARAMETERS USED IN THE EXPERIMENTS
We perform the experiments with the same architecture with different model parameters for FSDD and GSC. Table 3 shows the parameters of the models we use. Both defended and undefended networks share the same parameters for each dataset.
20


Reviews:
[{"review_id": "rJlkTjrTFB", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper presents an end-to-end neural network verifier that is specially designed for audio signal processing to certify the robustness of a system when facing noise perturbation.  The approach is based on abstract transformers to deal with non-linearity in the audio signal processing pipeline and LSTM acoustic model. The authors implement the approach in a so-called \"deep audio certifier\" system and conduct experiments on various datasets and network architectures.  The results seem to be supportive.   The idea is good and the mathematical derivation is meticulous (although appears to be a bit tedious).  This is an interesting paper globally but I have some concerns. \n\n1.  There should be a more thorough introduction on how to verify the robustness of a neural network classifier for noise perturbation.  There should be some background summary such as what are the existing approaches and how to measure the robustness of a neural network classifier, etc..\n\n2. The so-called audio processing pipeline here is actually speech processing pipeline. I am not sure if \"audio\" is the right term in a strict sense. \n\n3.  This paper is closely related to the POPQORN paper. So it is good to see some in-depth discussion and comparison between the two.  One thing that is not clear to me is that the authors claim POPQORN is very time-consuming but DAC is much faster.  I wonder if the authors can elaborate a bit more on this issue.   What exactly makes POPQORN time-consuming in this case? \n\nP.S. rebuttal read.  I will stay with my score. ", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "S1lGzu0hYH", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 1, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proposes an approach for the certification of speech classification neural networks against adversarial perturbations. The network is based on a simple pipeline starting from MFCC to make an utterance level classifier via a last hidden state of an LSTM acoustic model. This approach can perform analysis through this pipeline. I feel that this paper is very difficult to follow because of the lack of background technique explanations based on neural network certification, and the lack of technical surveys of speech recognition and related areas. This paper requires such major restructuring and more surveys to make it in good shape.\n\nComments\n- The authors only list CTC related techniques as state-of-the-art ASR, but state-of-the-art ASR is still based on the HMM/DNN hybrid system or attention-based encoder-decoder/RNN transducer. They seriously lack the surveys o this area. Also several technical terminologies are not common in the speech recognition are (e.g., automated speech recognition --> automatic speech recognition)\n- \"Additionally, audio systems typically use recurrent architectures (Chiu et al., 2017)\": There are a lot of state-of-the-art ASR systems including TDNN (Kaldi), CNN, and transformer. Again the paper does not have enough surveys.\n- The font size of the characters in figure 1 is too small.\n- I cannot understand why the paper uses MFCC. The community was already moved from MFCC to log mel filterbank. We don't need final DCT.\n- Section 2. Threat model: what kind of noises are using?\n- Page 3, power operation: Either side must be a conjugate to get the power spectrum.\n\n\n\n", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I did not assess the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "BJeL0admqr", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "In this work, the authors study the task of building neural network classifiers for audio tasks which can be certified as being resistant to an adversarial attack. One of the contributions of this work is the development of abstract transformers which can be used for the data processing frontend used in typical audio applications. The work also proposes an abstract transformers for LSTMs which is stated to be much faster to use in practice than previous work. \n\nOverall, this work is interesting and I think it would be a great addition to the conference. The paper is generally well written in the initial sections, and the main ideas are very clearly presented. However, there are a number of missing details, particularly in the final sections which discuss the experimental validation. In its present form, I am rating this work as “weak reject”, but I would increase my scores if the authors can improve the final sections in the revised draft.\n\nMain Comments:\n1. While I found section 3 to be useful to get an intuition of the proposed method, I still feel that it could be condensed a bit to add in additional details. For example, the authors don’t describe “back-substitution” in the work, which I believe should be described in the main text.\n2. A clarification question: When computing provability, the authors state that “We randomly shuffled the test data and then, for every experiment, inferred labels one by one until the number of correctly classified samples reached 100. We report the number of provably correct samples out of these 100 as our provability.” How sensitive was the provability metric to the choice of these 100 test examples? Was the metric computed by repeatedly sampling 100 test cases, for example?\n3. The section on “Provable defense for audio classifiers” was not very clear to me. The authors state that “To train, we combine standard loss with the worst case loss obtained using interval propagation.” I was not clear on what the modified loss is. Could the authors please clarify this in the text, preferably a mathematical formulation? Also, I’m curious why these experiments are only conducted on the FSDD set, but not on the GSC set. \n4. Figure 5c. Why does the interval analysis technique perform so much worse on the GSC set relative to the FSDD set?  On a related note, it would also be useful to describe some more details about the model architectures for the two tasks.\n5. The section on “Experimental comparison with prior work” similarly left me with a number of questions. The authors mention that “We found that, in practice, optimization approach used by POPQORN produces approximations of slightly smaller volume than our LSTM transformer (although non-comparable).” Could these be quantified and reported in the paper. Also, why are the approximation volumes not comparable between the two systems. \n\nMinor comment: It is true that most works in audio classification and speech recognition use processed frontend features such as MFCCs. However, there is also a significant body of work which operates directly on the time-domain signal. Perhaps it would be better to clarify this in the text?\nFor example:\nPascual S, Bonafonte A, Serra J. SEGAN: Speech enhancement generative adversarial network. arXiv preprint arXiv:1703.09452. 2017 Mar 28.\nSainath TN, Weiss RJ, Senior A, Wilson KW, Vinyals O. Learning the speech front-end with raw waveform CLDNNs. In Sixteenth Annual Conference of the International Speech Communication Association 2015.\n", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper developed log abstract transformer, square abstract transformer and sigmoid-tanh abstract transformer to certifiy robustness of neural network models for audio. The work is interesting but the scope is limited. It presented a neural network certification methods for one particular type of audio classifiers that use MFCC as input features and LSTM as the neural network layers. This thus may have limited interest to the general readers. 

The paper targets to present an end-to-end solution to audio classifiers. Investigation on one particular type of audio classifier is far from sufficient. As the reviewers pointed out, there're large literature of work using raw waveform inputs systems. Also there're many state-of-the-art systems are HMM/DNN and attnetion based encoder-decoder models. In terms of neural network models, resent based models, transformer models etc are also important. A more thorough investigation/comparison would greatly enlarge the scope of this paper. 
Decision: Reject