{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:08Z","timestamp":1784232968381,"version":"3.55.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a scalable and precise verifier for recurrent neural networks, called<jats:sc>Prover<\/jats:sc>based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and non-linear recurrent update functions by combining sampling, optimization, and Fermat\u2019s theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using<jats:sc>Prover<\/jats:sc>, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that<jats:sc>Prover<\/jats:sc>successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_10","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"225-248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["Scalable Polyhedral Verification of Recurrent Neural Networks"],"prefix":"10.1007","author":[{"given":"Wonryong","family":"Ryou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jiayu","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mislav","family":"Balunovic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gagandeep","family":"Singh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Dan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"10_CR1","unstructured":"Fermat\u2019s theorem. https:\/\/planetmath.org\/fermatstheoremstationarypoints"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Akintunde, M.E., Kevorchian, A., Lomuscio, A., Pirovano, E.: Verification of RNN-based neural agent-environment systems. In: Proceedings of the AAAI Conference on Artificial Intelligence (2019)","DOI":"10.1609\/aaai.v33i01.33016006"},{"issue":"2","key":"10_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"10_CR4","unstructured":"Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.: Certifying geometric robustness of neural networks. In: Advances in Neural Information Processing Systems (2019)"},{"key":"10_CR5","unstructured":"Balunovic, M., Vechev, M.: Adversarial training and provable defenses: Bridging the gap. In: International Conference on Learning Representations (2020)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Biggio, B., et al.: Evasion attacks against machine learning at test time. In: Joint European Conference on Machine Learning and Knowledge Discovery in Databases (2013)","DOI":"10.1007\/978-3-642-40994-3_25"},{"key":"10_CR7","unstructured":"Carlini, N., et al.: Hidden voice commands. In: 25th $$\\{$$USENIX$$\\}$$ Security Symposium ($$\\{$$USENIX$$\\}$$ Security 16), pp. 513\u2013530 (2016)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Carlini, N., Wagner, D.: Audio adversarial examples: Targeted attacks on speech-to-text. In: 2018 IEEE Security and Privacy Workshops (SPW) (2018)","DOI":"10.1109\/SPW.2018.00009"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Cho, K., et al.: Learning phrase representations using RNN encoder-decoder for statistical machine translation. In: EMNLP, pp. 1724\u20131734 (2014)","DOI":"10.3115\/v1\/D14-1179"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of Principles of Programming Languages, ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"9","key":"10_CR11","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1109\/MCOM.2018.1701270","volume":"56","author":"A Diro","year":"2018","unstructured":"Diro, A., Chilamkurti, N.: Leveraging LSTM networks for attack detection in fog-to-things communications. IEEE Commun. Mag. 56(9), 124\u2013130 (2018)","journal-title":"IEEE Commun. Mag."},{"key":"10_CR12","unstructured":"Dvijotham, K., et al.: Training verified learners with learned verifiers. arXiv:1805.10265 (2018)"},{"key":"10_CR13","unstructured":"Fischer, M., Baader, M., Vechev, M.: Certification of semantic perturbations via randomized smoothing. arXiv:2002.12463 (2020)"},{"key":"10_CR14","unstructured":"Hannun, A., et al.: Deep speech: Scaling up end-to-end speech recognition. arXiv:1412.5567 (2014)"},{"issue":"8","key":"10_CR15","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735\u20131780 (1997)","journal-title":"Neural Comput."},{"key":"10_CR16","unstructured":"Hu, W., Tan, Y.: Black-box attacks against RNN based malware detection algorithms. arXiv:1705.08131 (2017)"},{"key":"10_CR17","unstructured":"Jackson, Z.: Free spoken digit dataset (2020). https:\/\/github.com\/Jakobovski\/free-spoken-digit-dataset"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Jacoby, Y., Barrett, C., Katz, G.: Verifying recurrent neural networks using invariant inference. arXiv:2004.02462 (2020)","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"10_CR19","unstructured":"Khmelnitsky, I., et al.: Property-directed verification of recurrent neural networks. arXiv:2009.10610 (2020)"},{"key":"10_CR20","unstructured":"Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. arXiv:1412.6980 (2014)"},{"key":"10_CR21","unstructured":"Ko, C., Lyu, Z., Weng, T., Daniel, L., Wong, N., Lin, D.: Popqorn: Certifying robustness of recurrent neural networks. In: International Conference on Machine Learning (ICML) (2019)"},{"key":"10_CR22","unstructured":"Li, J., Qu, S., Li, X., Szurley, J., Kolter, J.Z., Metze, F.: Adversarial music: real world audio adversary against wake-word detection system. In: Advances in Neural Information Processing Systems, pp. 11908\u201311918 (2019)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: Tightened neural network robustness certificates. arXiv:1912.00574 (2019)","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Proceedings of Programs As Data Objects (PADO), pp. 155\u2013172 (2001)","DOI":"10.1007\/3-540-44978-7_10"},{"issue":"1","key":"10_CR25","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symbolic Comput."},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Neekhara, P., Hussain, S., Pandey, P., Dubnov, S., McAuley, J., Koushanfar, F.: Universal adversarial perturbations for speech recognition systems. arXiv:1905.03828 (2019)","DOI":"10.21437\/Interspeech.2019-1353"},{"key":"10_CR27","unstructured":"Pachocki, J., et al.: Openai five. https:\/\/blog.openai.com\/openai-five (2018)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Swami, A., Harang, R.: Crafting adversarial input sequences for recurrent neural networks. In: MILCOM 2016\u20132016 IEEE Military Communications Conference, pp. 49\u201354. IEEE (2016)","DOI":"10.1109\/MILCOM.2016.7795300"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Pascual, S., Bonafonte, A., Serra, J.: Segan: Speech enhancement generative adversarial network. arXiv:1703.09452 (2017)","DOI":"10.21437\/Interspeech.2017-1428"},{"key":"10_CR30","unstructured":"Paszke, A., et al.: Automatic differentiation in pytorch (2017)"},{"key":"10_CR31","unstructured":"Qin, Y., Carlini, N., Goodfellow, I., Cottrell, G., Raffel, C.: Imperceptible, robust, and targeted adversarial examples for automatic speech recognition. In: International Conference on Machine Learning (ICML) (2019)"},{"key":"10_CR32","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.S.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Advances in Neural Information Processing Systems (NeurIPS), pp. 10877\u201310887 (2018)"},{"key":"10_CR33","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1016\/j.neucom.2015.07.085","volume":"171","author":"JL Reyes-Ortiz","year":"2016","unstructured":"Reyes-Ortiz, J.L., Oneto, L., Sam\u00e0, A., Parra, X., Anguita, D.: Transition-aware human activity recognition using smartphones. Neurocomputing 171, 754\u2013767 (2016)","journal-title":"Neurocomputing"},{"key":"10_CR34","unstructured":"Sabour, S., Frosst, N., Hinton, G.E.: Dynamic routing between capsules. In: Proceedings of Neural Information Processing Systems (NIPS), pp. 3856\u20133866 (2017)"},{"issue":"4","key":"10_CR35","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/j.specom.2011.11.004","volume":"54","author":"M Sahidullah","year":"2012","unstructured":"Sahidullah, M., Saha, G.: Design, analysis and experimental evaluation of block based transformation in MFCC computation for speaker recognition. Speech Commun. 54(4), 543\u2013565 (2012)","journal-title":"Speech Commun."},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Sainath, T.N., Weiss, R.J., Senior, A., Wilson, K.W., Vinyals, O.: Learning the speech front-end with raw waveform CLDNNs. In: Sixteenth Annual Conference of the International Speech Communication Association (2015)","DOI":"10.21437\/Interspeech.2015-1"},{"key":"10_CR37","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: Advances in Neural Information Processing Systems (2019)"},{"key":"10_CR38","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems (2018)"},{"key":"10_CR39","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. In: Proceedings of Principles of Programming Languages (POPL) (2019)","DOI":"10.1145\/3290354"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of Principles of Programming Languages (POPL), pp. 46\u201359 (2017)","DOI":"10.1145\/3093333.3009885"},{"key":"10_CR41","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. arXiv:1312.6199 (2013)"},{"key":"10_CR42","unstructured":"Vaswani, A., et al.: Attention is all you need. In: Proceedings of Neural Information Processing Systems (NIPS) (2017)"},{"key":"10_CR43","unstructured":"Vinyals, O., et al.: Alphastar: Mastering the real-time strategy game starcraft ii. DeepMind blog p. 2 (2019)"},{"key":"10_CR44","unstructured":"Warden, P.: Speech commands: A dataset for limited-vocabulary speech recognition. arXiv:1804.03209 (2018)"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"Wu, M., Kwiatkowska, M.: Robustness guarantees for deep neural networks on videos. arXiv:1907.00098 (2019)","DOI":"10.1109\/CVPR42600.2020.00039"},{"key":"10_CR46","unstructured":"Yang, Z., Li, B., Chen, P.Y., Song, D.: Characterizing audio adversarial examples using temporal dependency (2019)"},{"key":"10_CR47","unstructured":"Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems, (NeurIPS) (2018)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T18:45:23Z","timestamp":1672857923000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}