{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:12:12Z","timestamp":1775880732256,"version":"3.50.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Adversarial noise attacks present a significant threat to quantum machine learning (QML) models, similar to their classical counterparts. This is especially true in the current Noisy Intermediate-Scale Quantum era, where noise is unavoidable. Therefore, it is essential to ensure the robustness of QML models before their deployment. To address this challenge, we introduce <jats:italic>VeriQR<\/jats:italic>, the first tool designed specifically for formally verifying and improving the robustness of QML models, to the best of our knowledge. This tool mimics real-world quantum hardware\u2019s noisy impacts by incorporating random noise to formally validate a QML model\u2019s robustness. <jats:italic>VeriQR<\/jats:italic> supports exact (sound and complete) algorithms for both local and global robustness verification. For enhanced efficiency, it implements an under-approximate (complete) algorithm and a tensor network-based algorithm to verify local and global robustness, respectively. As a formal verification tool, <jats:italic>VeriQR<\/jats:italic> can detect adversarial examples and utilize them for further analysis and to enhance the local robustness through adversarial training, as demonstrated by experiments on real-world quantum machine learning models. Moreover, it permits users to incorporate customized noise. Based on this feature, we assess <jats:italic>VeriQR<\/jats:italic> using various real-world examples, and experimental outcomes confirm that the addition of specific quantum noise can enhance the global robustness of QML models. These processes are made accessible through a user-friendly graphical interface provided by <jats:italic>VeriQR<\/jats:italic>, catering to general users without requiring a deep understanding of the counter-intuitive probabilistic nature of quantum computing.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_21","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"403-421","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A obustness fication Tool for\u00a0 uantum Machine Learning Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-5492-3752","authenticated-orcid":false,"given":"Yanling","family":"Lin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3490-0029","authenticated-orcid":false,"given":"Ji","family":"Guan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7628-1185","authenticated-orcid":false,"given":"Wang","family":"Fang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0021-225X","authenticated-orcid":false,"given":"Zhaofeng","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., et\u00a0al.: Introduction to neural network verification. Found. Trends\u00ae Programm. Lang. 7(1\u20132), 1\u2013157 (2021)","DOI":"10.1561\/2500000051"},{"key":"21_CR2","unstructured":"Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.: Certifying geometric robustness of neural networks. In: Advances in Neural Information Processing Systems, vol. 32 (2019)"},{"key":"21_CR3","unstructured":"Becker, B., Kohavi, R.: Adult. UCI Machine Learning Repository (1996)"},{"issue":"7671","key":"21_CR4","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1038\/nature23474","volume":"549","author":"J Biamonte","year":"2017","unstructured":"Biamonte, J., Wittek, P., Pancotti, N., Rebentrost, P., Wiebe, N., Lloyd, S.: Quantum machine learning. Nature 549(7671), 195\u2013202 (2017)","journal-title":"Nature"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Biggio, B., Roli, F.: Wild Patterns: ten years after the rise of adversarial machine learning. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 2154\u20132156 (2018)","DOI":"10.1145\/3243734.3264418"},{"key":"21_CR6","unstructured":"Blanchette, J., Summerfield, M.: C++ GUI programming with Qt 4. Prentice Hall Professional (2006)"},{"key":"21_CR7","unstructured":"Broughton, M., et\u00a0al.: TensorFlow Quantum: a software framework for quantum machine learning. arXiv preprint arXiv:2003.02989 (2020)"},{"issue":"1","key":"21_CR8","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1049\/cit2.12028","volume":"6","author":"A Chakraborty","year":"2021","unstructured":"Chakraborty, A., Alam, M., Dey, V., Chattopadhyay, A., Mukhopadhyay, D.: A survey on adversarial attacks and defences. CAAI Trans. Intell. Technol. 6(1), 25\u201345 (2021)","journal-title":"CAAI Trans. Intell. Technol."},{"key":"21_CR9","unstructured":"Chen, K., et al.: VeriQBench: a benchmark for multiple types of quantum circuits. arXiv preprint arXiv:2206.10880 (2022)"},{"key":"21_CR10","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-031-37709-9_7","volume-title":"Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part III","author":"Y-F Chen","year":"2023","unstructured":"Chen, Y.-F., Chung, K.-M., Leng\u00e1l, O., Lin, J.-A., Tsai, W.-L.: AutoQ: An Automata-Based Quantum Circuit Verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part III, pp. 139\u2013153. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_7"},{"key":"21_CR11","unstructured":"Cross, A.W., Bishop, L.S., Smolin, J.A., Gambetta, J.M.: Open quantum assembly language. arXiv preprint arXiv:1707.03429 (2017)"},{"issue":"6","key":"21_CR12","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/MSP.2012.2211477","volume":"29","author":"L Deng","year":"2012","unstructured":"Deng, L.: The mnist database of handwritten digit images for machine learning research. IEEE Signal Process. Mag. 29(6), 141\u2013142 (2012)","journal-title":"IEEE Signal Process. Mag."},{"key":"21_CR13","unstructured":"Developers, C.: Cirq. https:\/\/quantumai.google\/cirq"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Dreossi, T., et al.: VERIFAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In: International Conference on Computer Aided Verification, pp. 432\u2013442. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_25","DOI":"10.1007\/978-3-030-25540-4_25"},{"issue":"2","key":"21_CR15","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevResearch.3.023153","volume":"3","author":"Y Du","year":"2021","unstructured":"Du, Y., Hsieh, M.H., Liu, T., Tao, D., Liu, N.: Quantum noise protects quantum classifiers against adversaries. Phys. Rev. Res. 3(2), 023153 (2021)","journal-title":"Phys. Rev. Res."},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-319-19249-9_17","volume-title":"FM 2015: Formal Methods","author":"Y Feng","year":"2015","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Zhang, L.: QPMC: a model checker for quantum programs and protocols. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 265\u2013272. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_17"},{"key":"21_CR17","unstructured":"Fisher, R.A.: Iris. UCI Machine Learning Repository (1988)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"21_CR19","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-81685-8_7","volume-title":"Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part I","author":"J Guan","year":"2021","unstructured":"Guan, J., Fang, W., Ying, M.: Robustness verification of quantum classifiers. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part I, pp. 151\u2013174. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_7"},{"key":"21_CR20","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-031-13188-2_20","volume-title":"Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part II","author":"J Guan","year":"2022","unstructured":"Guan, J., Fang, W., Ying, M.: Verifying fairness in\u00a0quantum machine learning. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part II, pp. 408\u2013429. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_20"},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-031-65633-0_24","volume-title":"Computer Aided Verification: 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24\u201327, 2024, Proceedings, Part III","author":"J Guan","year":"2024","unstructured":"Guan, J., Feng, Y., Turrini, A., Ying, M.: Measurement-based verification of\u00a0quantum Markov chains. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification: 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24\u201327, 2024, Proceedings, Part III, pp. 533\u2013554. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_24"},{"issue":"3","key":"21_CR22","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1038\/s41567-020-01105-y","volume":"17","author":"MP Harrigan","year":"2021","unstructured":"Harrigan, M.P., et al.: Quantum approximate optimization of non-planar graph problems on a planar superconducting processor. Nat. Phys. 17(3), 332\u2013336 (2021). https:\/\/doi.org\/10.1038\/s41567-020-01105-y","journal-title":"Nat. Phys."},{"issue":"3","key":"21_CR23","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/S0019-9958(67)90302-6","volume":"10","author":"CW Helstrom","year":"1967","unstructured":"Helstrom, C.W.: Detection theory and quantum mechanics. Inf. Control 10(3), 254\u2013291 (1967)","journal-title":"Inf. Control"},{"key":"21_CR24","unstructured":"Hofmann, H.: Statlog (German Credit Data). UCI Machine Learning Repository (1994)"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Huang, J.C., et al.: Certified robustness of quantum classifiers against adversarial examples through quantum noise. In: ICASSP 2023-2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pp.\u00a01\u20135. IEEE (2023)","DOI":"10.1109\/ICASSP49357.2023.10095030"},{"key":"21_CR26","unstructured":"IBM: Learn quantum computation using Qiskit. https:\/\/qiskit.org\/textbook\/preface.html (Accessed 2021)"},{"key":"21_CR27","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":"21_CR28","doi-asserted-by":"crossref","unstructured":"Li, R., et al.: PRODeep: a platform for robustness verification of deep neural networks. In: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1630\u20131634 (2020)","DOI":"10.1145\/3368089.3417918"},{"key":"21_CR29","unstructured":"Lin, Y., Guan, J., Fang, W., Ying, M., Su, Z.: Artifact for veriQR (2024). https:\/\/doi.org\/10.5281\/zenodo.12526235"},{"issue":"6","key":"21_CR30","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.101.062331","volume":"101","author":"N Liu","year":"2020","unstructured":"Liu, N., Wittek, P.: Vulnerability of quantum classification to adversarial perturbations. Phys. Rev. A 101(6), 062331 (2020)","journal-title":"Phys. Rev. A"},{"issue":"3","key":"21_CR31","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevResearch.2.033212","volume":"2","author":"S Lu","year":"2020","unstructured":"Lu, S., Duan, L.M., Deng, D.L.: Quantum adversarial machine learning. Phys. Rev. Res. 2(3), 033212 (2020)","journal-title":"Phys. Rev. Res."},{"issue":"2","key":"21_CR32","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1063\/1.1359716","volume":"54","author":"MA Nielsen","year":"2001","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum computation and quantum information. Phys. Today 54(2), 60 (2001)","journal-title":"Phys. Today"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-70545-1_51","volume-title":"Computer Aided Verification","author":"SJ Gay","year":"2008","unstructured":"Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: a model checker for quantum systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 543\u2013547. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_51"},{"key":"21_CR34","doi-asserted-by":"publisher","first-page":"79","DOI":"10.22331\/q-2018-08-06-79","volume":"2","author":"J Preskill","year":"2018","unstructured":"Preskill, J.: Quantum computing in the NISQ era and beyond. Quantum 2, 79 (2018)","journal-title":"Quantum"},{"issue":"6507","key":"21_CR35","doi-asserted-by":"publisher","first-page":"1084","DOI":"10.1126\/science.abb9811","volume":"369","author":"GA Quantum","year":"2020","unstructured":"Quantum, G.A., et al.: Hartree-Fock on a superconducting qubit quantum computer. Science 369(6507), 1084\u20131089 (2020)","journal-title":"Science"},{"key":"21_CR36","unstructured":"Roberts, C., et al.: TensorNetwork: a library for physics and machine learning (2019). https:\/\/tensornetwork.readthedocs.io\/en\/latest\/index.html"},{"key":"21_CR37","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014)"},{"key":"21_CR38","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-81685-8_12","volume-title":"Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part I","author":"H-D Tran","year":"2021","unstructured":"Tran, H.-D., et al.: Robustness verification of semantic segmentation neural networks using relaxed reachability. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part I, pp. 263\u2013286. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_12"},{"key":"21_CR39","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Proceedings, Part I","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Proceedings, Part I, pp. 3\u201317. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"21_CR40","unstructured":"ULB, M.L.G.: Credit card fraud detection. https:\/\/www.kaggle.com\/datasets\/mlg-ulb\/creditcardfraud"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Weber, M., Liu, N., Li, B., Zhang, C., Zhao, Z.: Optimal provable robustness of quantum classification via quantum hypothesis testing. NPJ Quant. Inf. 7(1), 76 (2021)","DOI":"10.1038\/s41534-021-00410-5"},{"key":"21_CR42","unstructured":"Xiao, H., Rasul, K., Vollgraf, R.: Fashion-MNIST: a novel image dataset for benchmarking machine learning algorithms. arXiv preprint arXiv:1708.07747 (2017)"},{"key":"21_CR43","unstructured":"Xu, X., et\u00a0al.: MindSpore Quantum: a user-friendly, high-performance, and AI-compatible quantum computing framework. arXiv preprint arXiv:2406.17248 (2024)"},{"issue":"2","key":"21_CR44","doi-asserted-by":"publisher","first-page":"287","DOI":"10.3390\/e25020287","volume":"25","author":"A Zeguendry","year":"2023","unstructured":"Zeguendry, A., Jarir, Z., Quafafou, M.: Quantum machine learning: a review and case studies. Entropy 25(2), 287 (2023)","journal-title":"Entropy"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: CoqQ: foundational verification of quantum programs. In: Proceedings of the ACM on Programming Languages, vol. 7(POPL), pp. 833\u2013865 (2023)","DOI":"10.1145\/3571222"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:06:44Z","timestamp":1725934004000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}