{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:01:59Z","timestamp":1742965319072,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031460012"},{"type":"electronic","value":"9783031460029"}],"license":[{"start":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T00:00:00Z","timestamp":1702512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T00:00:00Z","timestamp":1702512000000},"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-46002-9_7","type":"book-chapter","created":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T16:02:36Z","timestamp":1702483356000},"page":"119-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal XAI via\u00a0Syntax-Guided Synthesis"],"prefix":"10.1007","author":[{"given":"Katrine","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel","family":"Judson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Filip","family":"Cano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Drew","family":"Goldman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nick","family":"Shoemaker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bettina","family":"K\u00f6nighofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,14]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"52138","DOI":"10.1109\/ACCESS.2018.2870052","volume":"6","author":"A Adadi","year":"2018","unstructured":"Adadi, A., Berrada, M.: Peeking inside the black-box: a survey on explainable artificial intelligence (XAI). IEEE Access 6, 52138\u201352160 (2018)","journal-title":"IEEE Access"},{"issue":"8","key":"7_CR2","doi-asserted-by":"publisher","first-page":"5031","DOI":"10.1109\/TII.2022.3146552","volume":"18","author":"I Ahmed","year":"2022","unstructured":"Ahmed, I., Jeon, G., Piccialli, F.: From artificial intelligence to explainable artificial intelligence in industry 4.0: a survey on what, how, and where. IEEE Trans. Ind. Inf. 18(8), 5031\u20135042 (2022)","journal-title":"IEEE Trans. Ind. Inf."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.inffus.2019.12.012","volume":"58","author":"AB Arrieta","year":"2020","unstructured":"Arrieta, A.B., et al.: Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf. Fusion 58, 82\u2013115 (2020)","journal-title":"Inf. Fusion"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-030-72013-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Ashok","year":"2021","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: TACAS 2021. LNCS, vol. 12652, pp. 326\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_17"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), pp. 415\u2013442 (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Bassan, S., Katz, G.: Towards formal XAI: formally approximate minimal explanations of neural networks. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 187\u2013207. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_10","DOI":"10.1007\/978-3-031-30823-9_10"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Cano C\u00f3rdoba, F., et al.: Analyzing intentional behavior in autonomous agents under uncertainty. In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, pp. 372\u2013381 (2023)","DOI":"10.24963\/ijcai.2023\/42"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1613\/jair.1.12963","volume":"72","author":"S Carr","year":"2021","unstructured":"Carr, S., Jansen, N., Topcu, U.: Task-aware verifiable rnn-based policies for partially observable markov decision processes. J. Artif. Intell. Res. (JAIR) 72, 819\u2013847 (2021)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"2","key":"7_CR10","doi-asserted-by":"publisher","first-page":"634","DOI":"10.3390\/s23020634","volume":"23","author":"A Chaddad","year":"2023","unstructured":"Chaddad, A., Peng, J., Xu, J., Bouridane, A.: Survey of explainable AI techniques in healthcare. Sensors 23(2), 634 (2023)","journal-title":"Sensors"},{"key":"7_CR11","unstructured":"Chollet, F.: Simple MNIST convnet (2015). https:\/\/keras.io\/examples\/vision\/mnist_convnet\/. Accessed 19 July 2023"},{"issue":"5","key":"7_CR12","doi-asserted-by":"publisher","first-page":"4765","DOI":"10.1007\/s10462-022-10275-5","volume":"56","author":"VG Costa","year":"2023","unstructured":"Costa, V.G., Pedreira, C.E.: Recent advances in decision trees: an updated survey. Artif. Intell. Rev. 56(5), 4765\u20134800 (2023)","journal-title":"Artif. Intell. Rev."},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-031-33170-1_7","volume-title":"NASA Formal Methods","author":"S Dierl","year":"2023","unstructured":"Dierl, S., et al.: Learning symbolic timed models from concrete timed data. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods, vol. 13903, pp. 104\u2013121. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_7"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Dwivedi, R., et al.: Explainable AI (XAI): core ideas, techniques, and solutions. ACM Comput. Surv. 55(9), 194:1\u2013194:33 (2023)","DOI":"10.1145\/3561048"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Fathi, E., Shoja, B.M.: Deep neural networks for natural language processing. In: Handbook of Statistics, vol. 38, pp. 229\u2013316. Elsevier (2018)","DOI":"10.1016\/bs.host.2018.07.006"},{"issue":"5","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3236009","volume":"51","author":"R Guidotti","year":"2018","unstructured":"Guidotti, R., Monreale, A., Ruggieri, S., Turini, F., Giannotti, F., Pedreschi, D.: A survey of methods for explaining black box models. ACM Comput. Surv. (CSUR) 51(5), 1\u201342 (2018)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"8","key":"7_CR17","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2240236.2240260","volume":"55","author":"S Gulwani","year":"2012","unstructured":"Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. Commun. ACM 55(8), 97\u2013105 (2012)","journal-title":"Commun. ACM"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Henderson, P., Islam, R., Bachman, P., Pineau, J., Precup, D., Meger, D.: Deep reinforcement learning that matters. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)","DOI":"10.1609\/aaai.v32i1.11694"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Ignatiev, A.: Towards trustable explainable AI. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pp. 5154\u20135158 (2020). https:\/\/www.ijcai.org\/","DOI":"10.24963\/ijcai.2020\/726"},{"key":"7_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2023.108939","volume":"159","author":"Y Izza","year":"2023","unstructured":"Izza, Y., Huang, X., Ignatiev, A., Narodytska, N., Cooper, M.C., Marques-Silva, J.: On computing probabilistic abductive explanations. Int. J. Approx. Reason. 159, 108939 (2023)","journal-title":"Int. J. Approx. Reason."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: 2010 ACM\/IEEE 32nd International Conference on Software Engineering (ICSE 2010), vol. 1, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"J\u00fcngermann, F., Kret\u00ednsk\u00fd, J., Weininger, M.: Algebraically explainable controllers: decision trees and support vector machines join forces. CoRR arXiv:2208.1280 (2022)","DOI":"10.1007\/s10009-023-00716-z"},{"key":"7_CR23","unstructured":"LeCun, Y., Cortes, C., Burges, C.J.: The MNIST database (1998). http:\/\/yann.lecun.com\/exdb\/mnist. Accessed 13 Aug 2022"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Li, M., Chan, N., Chandra, V., Muriki, K.: Cluster usage policy enforcement using slurm plugins and an HTTP API. In: Jacobs, G.A., Stewart, C.A. (eds.) PEARC 2020: Practice and Experience in Advanced Research Computing, Portland, OR, USA, 27\u201331 July 2020, pp. 232\u2013238. ACM (2020)","DOI":"10.1145\/3311790.3397341"},{"issue":"8","key":"7_CR25","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1038\/s42256-022-00516-1","volume":"4","author":"W Liang","year":"2022","unstructured":"Liang, W., et al.: Advances, challenges and opportunities in creating data for trustworthy AI. Nat. Mach. Intell. 4(8), 669\u2013677 (2022)","journal-title":"Nat. Mach. Intell."},{"key":"7_CR26","unstructured":"Lundberg, S.M., Lee, S.: A unified approach to interpreting model predictions. In: NIPS, pp. 4765\u20134774 (2017)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Ignatiev, A.: Delivering trustworthy AI through formal XAI. In: AAAI, pp. 12342\u201312350. AAAI Press (2022)","DOI":"10.1609\/aaai.v36i11.21499"},{"key":"7_CR28","unstructured":"Minh, D., Wang, H.X., Li, Y.F., Nguyen, T.N.: Explainable artificial intelligence: a comprehensive review. Artif. Intell. Rev., 1\u201366 (2022)"},{"issue":"1","key":"7_CR29","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1016\/j.fcij.2017.12.001","volume":"3","author":"H Mohsen","year":"2018","unstructured":"Mohsen, H., El-Dahshan, E.S.A., El-Horbaty, E.S.M., Salem, A.B.M.: Classification using deep learning neural networks for brain tumors. Future Comput. Inf. J. 3(1), 68\u201371 (2018)","journal-title":"Future Comput. Inf. J."},{"key":"7_CR30","unstructured":"Molnar, C.: Interpretable Machine Learning, 2 edn. (2022). https:\/\/christophm.github.io\/interpretable-ml-book"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Morton, K., Hallahan, W.T., Shum, E., Piskac, R., Santolucito, M.: Grammar filtering for syntax-guided synthesis. In: AAAI, pp. 1611\u20131618. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i02.5522"},{"key":"7_CR32","unstructured":"Neider, D., Ghosh, B.: Probably approximately correct explanations of machine learning models via syntax-guided synthesis. arXiv preprint arXiv:2009.08770 (2020)"},{"key":"7_CR33","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"Pedregosa, F., et al.: Scikit-learn: machine learning in python. J. Mach. Learn. Res. 12, 2825\u20132830 (2011)","journal-title":"J. Mach. Learn. Res."},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Ranjbar, N., Safabakhsh, R.: Using decision tree as local interpretable model in autoencoder-based LIME. In: CSICC, pp. 1\u20137. IEEE (2022)","DOI":"10.1109\/CSICC55295.2022.9780503"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: \u201cWhy Should I Trust You?\u201d explaining the predictions of any classifier. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD 2016), pp. 1135\u20131144 (2016)","DOI":"10.1145\/2939672.2939778"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Shih, A., Choi, A., Darwiche, A.: A symbolic approach to explaining bayesian network classifiers. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, Stockholm, Sweden, 13\u201319 July 2018, pp. 5103\u20135111 (2018). https:\/\/www.ijcai.org\/","DOI":"10.24963\/ijcai.2018\/708"},{"key":"7_CR37","unstructured":"Smith, J.W., Everhart, J.E., Dickson, W., Knowler, W.C., Johannes, R.S.: Using the ADAP learning algorithm to forecast the onset of diabetes mellitus. In: Proceedings of the Annual Symposium on Computer Application in Medical Care (1988)"},{"issue":"4\u20135","key":"7_CR38","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/s00165-021-00536-5","volume":"33","author":"M Tappler","year":"2021","unstructured":"Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: L$${}^{\\text{* }}$$-based learning of markov decision processes (extended version). Formal Aspects Comput. 33(4\u20135), 575\u2013615 (2021)","journal-title":"Formal Aspects Comput."},{"key":"7_CR39","unstructured":"Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: International Conference on Machine Learning (ICML), pp. 5045\u20135054. PMLR (2018)"},{"key":"7_CR40","first-page":"841","volume":"31","author":"S Wachter","year":"2017","unstructured":"Wachter, S., Mittelstadt, B., Russell, C.: Counterfactual explanations without opening the black box: automated decisions and the GDPR. Harvard J. Law Technol. 31, 841 (2017)","journal-title":"Harvard J. Law Technol."},{"key":"7_CR41","doi-asserted-by":"publisher","first-page":"108561","DOI":"10.1109\/ACCESS.2020.3000907","volume":"8","author":"F Wang","year":"2020","unstructured":"Wang, F., Cao, Z., Tan, L., Zong, H.: Survey on learning-based formal methods: taxonomy, applications and possible future directions. IEEE Access 8, 108561\u2013108578 (2020)","journal-title":"IEEE Access"}],"container-title":["Lecture Notes in Computer Science","Bridging the Gap Between AI and Reality"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-46002-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T16:03:56Z","timestamp":1702483436000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-46002-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,14]]},"ISBN":["9783031460012","9783031460029"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-46002-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,12,14]]},"assertion":[{"value":"14 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Bridging the Gap between AI and Reality","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2023","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":"aisola2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2023-aisola.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}