{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:19:13Z","timestamp":1743052753447,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031651113"},{"type":"electronic","value":"9783031651120"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-65112-0_4","type":"book-chapter","created":{"date-parts":[[2024,7,16]],"date-time":"2024-07-16T20:21:48Z","timestamp":1721161308000},"page":"78-99","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parallel Verification for\u00a0$$\\delta $$-Equivalence of\u00a0Neural Network Quantization"],"prefix":"10.1007","author":[{"given":"Pei","family":"Huang","sequence":"first","affiliation":[]},{"given":"Yuting","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Haoze","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Ieva","family":"Daukantas","sequence":"additional","affiliation":[]},{"given":"Min","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Fuqi","family":"Jia","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,17]]},"reference":[{"key":"4_CR1","unstructured":"FSD chip-tesla (2022). https:\/\/en.wikichip.org\/wiki\/tesla_(car_company)\/fsd_chip"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Bunda, S., Spreeuwers, L.J., Zeinstra, C.G.: Sub-byte quantization of mobile face recognition convolutional neural networks. In: Br\u00f6mme, A., et al. (eds.) Proceedings of the 21st International Conference of the Biometrics Special Interest Group, BIOSIG 2022, Darmstadt, Germany, 14\u201316 September 2022. LNI, vol. P-329, pp. 229\u2013236. IEEE \/ Gesellschaft f\u00fcr Informatik e.V. (2022)","DOI":"10.1109\/BIOSIG55365.2022.9897025"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-68167-2_18","volume-title":"Automated Technology for Verification and Analysis","author":"C-H Cheng","year":"2017","unstructured":"Cheng, C.-H., N\u00fchrenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 251\u2013268. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_18"},{"key":"4_CR4","unstructured":"Ciresan, D.C., Giusti, A., Gambardella, L.M., Schmidhuber, J.: Deep neural networks segment neuronal membranes in electron microscopy images. In: Advances in Neural Information Processing Systems 25: 26th Annual Conference on Neural Information Processing Systems 2012. Proceedings of a meeting held 3\u20136 December 2012, Lake Tahoe, Nevada, United States, pp. 2852\u20132860 (2012)"},{"key":"4_CR5","unstructured":"Devlin, J., Chang, M., Lee, K., Toutanova, K.: BERT: pre-training of deep bidirectional transformers for language understanding. In: Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, Minneapolis, MN, USA, 2\u20137 June 2019, vol. 1. pp. 4171\u20134186. Association for Computational Linguistics (2019)"},{"key":"4_CR6","unstructured":"Dosovitskiy, A., et al.: An image is worth 16$$\\,\\times \\,$$16 words: transformers for image recognition at scale. In: 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, 3\u20137 May 2021. OpenReview.net (2021)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"NASA Formal Methods","author":"S Dutta","year":"2018","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 121\u2013138. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_9"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","volume-title":"Automated Technology for Verification and Analysis","author":"R Ehlers","year":"2017","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269\u2013286. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19"},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/s10601-018-9285-6","volume":"23","author":"M Fischetti","year":"2018","unstructured":"Fischetti, M., Jo, J.: Deep neural networks and mixed integer linear optimization. Constraints Int. J. 23(3), 296\u2013309 (2018)","journal-title":"Constraints Int. J."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"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: 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA, pp. 3\u201318. IEEE Computer Society (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"4_CR11","unstructured":"Goodfellow, I.J., Bengio, Y., Courville, A.C.: Deep Learning. MIT Press, Adaptive computation and machine learning (2016)"},{"key":"4_CR12","unstructured":"Gurobi: A most powerful mathematical optimization solver (2018)"},{"key":"4_CR13","unstructured":"Han, S., Mao, H., Dally, W.J.: Deep compression: Compressing deep neural network with pruning, trained quantization and Huffman coding. In: 4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, 2\u20134 May 2016, Conference Track Proceedings (2016)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Lechner, M., \u017dikeli\u0107, D.: Scalable verification of quantized neural networks. In: Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, pp. 3787\u20133795. AAAI Press (2021)","DOI":"10.1609\/aaai.v35i5.16496"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and Conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Huang, P., Liu, M., Ge, C., Ma, F., Zhang, J.: Investigating the existence of orthogonal golf designs via satisfiability testing. In: Davenport, J.H., Wang, D., Kauers, M., Bradford, R.J. (eds.) Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, ISSAC 2019, Beijing, China, July 15-18, 2019, pp. 203\u2013210. ACM (2019)","DOI":"10.1145\/3326229.3326232"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-94205-6_24","volume-title":"Automated Reasoning","author":"P Huang","year":"2018","unstructured":"Huang, P., Ma, F., Ge, C., Zhang, J., Zhang, H.: Investigating the existence of large sets of idempotent quasigroups via satisfiability testing. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 354\u2013369. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_24"},{"key":"4_CR19","unstructured":"Huang, P., et al.: Towards efficient verification of quantized neural networks. arXiv preprint arXiv:2312.12679 (2023)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Jacob, B., et al.: Quantization and training of neural networks for efficient integer-arithmetic-only inference. In: 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, 18\u201322 June 2018, pp. 2704\u20132713. Computer Vision Foundation\/IEEE Computer Society (2018)","DOI":"10.1109\/CVPR.2018.00286"},{"key":"4_CR22","unstructured":"Jia, K., Rinard, M.C.: Efficient exact verification of binarized neural networks. In: Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, 6\u201312 December 2020, virtual (2020)"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Kulkarni, U., M, M.S., Gurlahosur, S.V., Bhogar, G.: Quantization friendly MobileNet (QF-MobileNet) architecture for vision based applications on embedded platforms. Neural Networks 136, 28\u201339 (2021)","DOI":"10.1016\/j.neunet.2020.12.022"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278\u20132324 (1998). https:\/\/doi.org\/10.1109\/5.726791","DOI":"10.1109\/5.726791"},{"key":"4_CR27","unstructured":"Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, 10\u201315 July 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 3575\u20133583. PMLR (2018)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Mistry, S., Saha, I., Biswas, S.: An MILP encoding for efficient verification of quantized deep neural networks. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4445\u20134456 (2022)","DOI":"10.1109\/TCAD.2022.3197697"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, C.: ReluDiff: differential verification of deep neural networks. In: Rothermel, G., Bae, D. (eds.) ICSE \u201920: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June\u201319 July, 2020, pp. 714\u2013726. ACM (2020)","DOI":"10.1145\/3377811.3380337"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, J., Wang, C.: NEURODIFF: scalable differential verification of neural networks using fine-grained approximation. In: 35th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, 21\u201325 September 2020, pp. 784\u2013796. IEEE (2020)","DOI":"10.1145\/3324884.3416560"},{"key":"4_CR31","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 10900\u201310910 (2018)"},{"key":"4_CR32","unstructured":"Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. In: 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, 7\u20139 May 2015, Conference Track Proceedings (2015)"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 41:1\u201341:30 (2019)","DOI":"10.1145\/3290354"},{"key":"4_CR34","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 6369\u20136379 (2018)"},{"key":"4_CR35","unstructured":"Weng, T., et al.: Towards fast computation of certified robustness for ReLU networks. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, 10\u201315 July 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5273\u20135282. PMLR (2018)"},{"key":"4_CR36","unstructured":"Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, 10\u201315 July 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5283\u20135292. PMLR (2018)"},{"key":"4_CR37","unstructured":"Wu, H., et al.: Parallelization techniques for verifying neural networks. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21\u201324 September 2020, pp. 128\u2013137. IEEE (2020)"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Xu, H., Gao, Y., Yu, F., Darrell, T.: End-to-end learning of driving models from large-scale video datasets. In: 2017 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2017, Honolulu, HI, USA, 21\u201326 July 2017, pp. 3530\u20133538. IEEE Computer Society (2017)","DOI":"10.1109\/CVPR.2017.376"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Yang, Y., Lei, W., Huang, P., Cao, J., Li, J., Chua, T.: A dual prompt learning framework for few-shot dialogue state tracking. In: Ding, Y., Tang, J., Sequeda, J.F., Aroyo, L., Castillo, C., Houben, G. (eds.) Proceedings of the ACM Web Conference 2023, WWW 2023, Austin, TX, USA, 30 April 2023\u20134 May 2023, pp. 1468\u20131477. ACM (2023)","DOI":"10.1145\/3543507.3583238"},{"key":"4_CR40","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 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 4944\u20134953 (2018)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Song, F., Sun, J.: QEBVerif: Quantization error bound verification of neural networks. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 413\u2013437. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_20"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Zhang, Y., et al.: QVIP: an ILP-based formal verification approach for quantized neural networks. In: 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, 10\u201314 October 2022, pp. 82:1\u201382:13. ACM (2022)","DOI":"10.1145\/3551349.3556916"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65112-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,16]],"date-time":"2024-07-16T20:22:30Z","timestamp":1721161350000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65112-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031651113","9783031651120"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65112-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"17 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.aiverification.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}