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.
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. 
Overall, 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.
Main Comments:
1. 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.
2. 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?
3. 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. 
4. 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.
5. 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. 
Minor 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?
For example:
Pascual S, Bonafonte A, Serra J. SEGAN: Speech enhancement generative adversarial network. arXiv preprint arXiv:1703.09452. 2017 Mar 28.
Sainath 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.