DiffRNN: differential verification of recurrent neural networks. (English) Zbl 07498004

Mohammadinejad, Sara; Paulsen, Brandon; Deshmukh, Jyotirmoy V.; Wang, Chao

Dima, Catalin (ed.) et al., Formal modeling and analysis of timed systems. 19th international conference, FORMATS 2021, Paris, France, August 24–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12860, 117-134 (2021).

Summary: Recurrent neural networks (RNNs) such as Long Short Term Memory (LSTM) networks have become popular in a variety of applications such as image processing, data classification, speech recognition, and as controllers in autonomous systems. In practical settings, there is often a need to deploy such RNNs on resource-constrained platforms such as mobile phones or embedded devices. As the memory footprint and energy consumption of such components become a bottleneck, there is interest in compressing and optimizing such networks using a range of heuristic techniques. However, these techniques do not guarantee the safety of the optimized network, e.g., against adversarial inputs, or equivalence of the optimized and original networks. To address this problem, we propose DiffRNN, the first differential verification method for RNNs to certify the equivalence of two structurally similar neural networks. Existing work on differential verification for ReLU-based feed-forward neural networks does not apply to RNNs where nonlinear activation functions such as Sigmoid and Tanh cannot be avoided. RNNs also pose unique challenges such as handling sequential inputs, complex feedback structures, and interactions between the gates and states. In DiffRNN, we overcome these challenges by bounding nonlinear activation functions with linear constraints and then solving constrained optimization problems to compute tight bounding boxes on non-linear surfaces in a high-dimensional space. The soundness of these bounding boxes is then proved using the dReal SMT solver. We demonstrate the practical efficacy of our technique on a variety of benchmarks and show that DiffRNN outperforms state-of-the-art RNN verification tools such as Popqorn.
For the entire collection see [Zbl 1482.68018].

MSC:

68Qxx

Theory of computing

Keywords:

recurrent neural networks; resource-constrained platforms; compression techniques; differential verification

Software:

dReal; DeepFool; MNIST; DeepXplore; ReluDiff; NeuroDiff; TensorFuzz; POPQORN; DiffRNN; Reluplex; DeepGauge; Marabou; AI2; DL2

References:

[1]	Anguita, D., Ghio, A., Oneto, L., Parra, X., Reyes-Ortiz, J.L.: A public domain dataset for human activity recognition using smartphones. In: ESANN (2013)
[2]	Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V., Criminisi, A.: Measuring neural net robustness with constraints. In: Annual Conference on Neural Information Processing Systems, pp. 2613-2621 (2016)
[3]	Bojarski, M., et al.: End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)
[4]	Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks. In: IEEE Symposium on Security and Privacy, pp. 39-57 (2017)
[5]	Cheng, Y., Wang, D., Zhou, P., Zhang, T.: A survey of model compression and acceleration for deep neural networks. arXiv preprint arXiv:1710.09282 (2017)
[6]	Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238-252 (1977)
[7]	Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 84-96 (1978)
[8]	Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: International Conference on Uncertainty in Artificial Intelligence, pp. 550-559 (2018)
[9]	Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, 3-6 October 2017, Proceedings, pp. 269-286 (2017) · Zbl 1495.68131
[10]	Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.T.: DL2: training and querying neural networks with logic. In: International Conference on Machine Learning, pp. 1931-1941 (2019)
[11]	Gao, S.; Kong, S.; Clarke, EM; Bonacina, MP, dReal: an SMT solver for nonlinear theories over the reals, Automated Deduction - CADE-24, 208-214 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68268
[12]	Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: IEEE Symposium on Security and Privacy, pp. 3-18 (2018)
[13]	Ghorbal, K.; Goubault, E.; Putot, S.; Bouajjani, A.; Maler, O., The zonotope abstract domain Taylor1+, Computer Aided Verification, 627-633 (2009), Heidelberg: Springer, Heidelberg
[14]	Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: International Conference on Learning Representations (2015)
[15]	Gopinath, D., Katz, G., Pasareanu, C.S., Barrett, C.W.: DeepSafe: a data-driven approach for assessing robustness of neural networks. In: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, 7-10 October 2018, Proceedings, pp. 3-19 (2018)
[16]	Han, S., Mao, H., Dally, W.J.: Deep compression: compressing deep neural network with pruning, trained quantization and Huffman coding. In: International Conference on Learning Representations (2016)
[17]	Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: International Conference on Computer Aided Verification, pp. 3-29 (2017) · Zbl 1494.68166
[18]	Jia, R., Raghunathan, A., Göksel, K., Liang, P.: Certified robustness to adversarial word substitutions. arXiv preprint arXiv:1909.00986 (2019)
[19]	Julian, KD; Kochenderfer, MJ; Owen, MP, Deep neural network compression for aircraft collision avoidance systems, J. Guid. Control Dyn., 42, 3, 598-608 (2019)
[20]	Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: International Conference on Computer Aided Verification, pp. 97-117 (2017) · Zbl 1494.68167
[21]	Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: International Conference on Computer Aided Verification, pp. 443-452 (2019)
[22]	Ko, C.Y., Lyu, Z., Weng, T.W., Daniel, L., Wong, N., Lin, D.: Popqorn: quantifying robustness of recurrent neural networks. arXiv preprint arXiv:1905.07387 (2019)
[23]	Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial examples in the physical world. In: International Conference on Learning Representations (2017)
[24]	LeCun, Y., Cortes, C.: MNIST handwritten digit database (2010). http://yann.lecun.com/exdb/mnist/
[25]	Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: tightened neural network robustness certificates. arXiv preprint arXiv:1912.00574 (2019)
[26]	Ma, L., et al.: Deepgauge: multi-granularity testing criteria for deep learning systems. In: IEEE/ACM International Conference On Automated Software Engineering, pp. 120-131. ACM (2018)
[27]	Ma, S., Liu, Y., Lee, W., Zhang, X., Grama, A.: MODE: automated neural network model debugging via state differential analysis and input selection. In: Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, 04-09 November 2018, pp. 175-186 (2018)
[28]	Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: International Conference on Learning Representations (2018)
[29]	Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: International Conference on Machine Learning, pp. 3575-3583 (2018)
[30]	Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis, vol. 110. SIAM (2009) · Zbl 1168.65002
[31]	Moosavi-Dezfooli, S., Fawzi, A., Frossard, P.: DeepFool: a simple and accurate method to fool deep neural networks. In: IEEE Conference on Computer Vision and Pattern Recognition, pp. 2574-2582 (2016)
[32]	Nguyen, A.M., Yosinski, J., Clune, J.: Deep neural networks are easily fooled: high confidence predictions for unrecognizable images. In: IEEE Conference on Computer Vision and Pattern Recognition, pp. 427-436 (2015)
[33]	Odena, A., Goodfellow, I.: Tensorfuzz: debugging neural networks with coverage-guided fuzzing. arXiv preprint arXiv:1807.10875 (2018)
[34]	Paulsen, B., Wang, J., Wang, C.: Reludiff: differential verification of deep neural networks. arXiv preprint arXiv:2001.03662 (2020)
[35]	Paulsen, B., Wang, J., Wang, J., Wang, C.: Neurodiff: scalable differential verification of neural networks using fine-grained approximation. arXiv preprint arXiv:2009.09943 (2020)
[36]	Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: automated whitebox testing of deep learning systems. In: ACM Symposium on Operating Systems Principles, pp. 1-18 (2017)
[37]	Price, KV; Storn, RM; Lampinen, JA, Differential Evolution: A Practical Approach to Global Optimization (2005), Heidelberg: Springer, Heidelberg · Zbl 1186.90004
[38]	Raghunathan, A., Steinhardt, J., Liang, P.: Certified defenses against adversarial examples. In: International Conference on Learning Representations (2018)
[39]	Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: International Joint Conference on Artificial Intelligence, pp. 2651-2659 (2018)
[40]	Shi, Z., Zhang, H., Chang, K.W., Huang, M., Hsieh, C.J.: Robustness verification for transformers. arXiv preprint arXiv:2002.06622 (2020)
[41]	Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 41:1-41:30 (2019)
[42]	Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: Boosting robustness certification of neural networks. In: International Conference on Learning Representations (2019)
[43]	Stérin, T.; Farrugia, N.; Gripon, V., An intrinsic difference between vanilla RNNs and GRU models, COGNTIVE, 2017, 84 (2017)
[44]	Sun, Y., Wu, M., Ruan, W., Huang, X., Kwiatkowska, M., Kroening, D.: Concolic testing for deep neural networks. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3-7 September 2018, pp. 109-119 (2018)
[45]	Szegedy, C., et al.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)
[46]	Tian, Y., Pei, K., Jana, S., Ray, B.: Deeptest: automated testing of deep-neural-network-driven autonomous cars. In: International Conference on Software Engineering, pp. 303-314 (2018)
[47]	Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Annual Conference on Neural Information Processing Systems, pp. 6369-6379 (2018)
[48]	Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: USENIX Security Symposium, pp. 1599-1614 (2018)
[49]	Weng, T., et al.: Towards fast computation of certified robustness for relu networks. In: International Conference on Machine Learning, pp. 5273-5282 (2018)
[50]	Wicker, M., Huang, X., Kwiatkowska, M.: Feature-guided black-box safety testing of deep neural networks. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 408-426 (2018)
[51]	Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: International Conference on Machine Learning, pp. 5283-5292 (2018)
[52]	Xie, X., et al.: Deephunter: a coverage-guided fuzz testing framework for deep neural networks. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 146-157 (2019)
[53]	Xie, X., Ma, L., Wang, H., Li, Y., Liu, Y., Li, X.: Diffchaser: detecting disagreements for deep neural networks. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence, pp. 5772-5778. AAAI Press (2019)
[54]	Xu, W., Qi, Y., Evans, D.: Automatically evading classifiers: a case study on PDF malware classifiers. In: Network and Distributed System Security Symposium (2016)
[55]	Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Annual Conference on Neural Information Processing Systems, pp. 4939-4948 (2018)