Abstract
In this paper, we propose a novel application of syntax-guided synthesis to find symbolic representations of a model’s decision-making process, designed for easy comprehension and validation by humans. Our approach takes input-output samples from complex machine learning models, such as deep neural networks, and automatically derives interpretable mimic programs. A mimic program precisely imitates the behavior of an opaque model over the provided data. We discuss various types of grammars that are well-suited for computing mimic programs for tabular and image input data.
Our experiments demonstrate the potential of the proposed method: we successfully synthesized mimic programs for neural networks trained on the MNIST and the Pima Indians diabetes data sets. All experiments were performed using the SMT-based \(\texttt{cvc5}\;\)synthesis tool.
K. Bjørner and S. Judson—Equal contribution.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Note that the mathematical expressions of the formula can easily be translated into a programming language such as Python.
- 2.
References
Adadi, A., Berrada, M.: Peeking inside the black-box: a survey on explainable artificial intelligence (XAI). IEEE Access 6, 52138–52160 (2018)
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–5042 (2022)
Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1–8. IEEE (2013)
Arrieta, A.B., et al.: Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf. Fusion 58, 82–115 (2020)
Ashok, P., Jackermeier, M., Křetínský, 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–345. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_17
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–442 (2022)
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–207. Springer, Heidelberg (2023). https://doi.org/10.1007/978-3-031-30823-9_10
Cano Córdoba, 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–381 (2023)
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–847 (2021)
Chaddad, A., Peng, J., Xu, J., Bouridane, A.: Survey of explainable AI techniques in healthcare. Sensors 23(2), 634 (2023)
Chollet, F.: Simple MNIST convnet (2015). https://keras.io/examples/vision/mnist_convnet/. Accessed 19 July 2023
Costa, V.G., Pedreira, C.E.: Recent advances in decision trees: an updated survey. Artif. Intell. Rev. 56(5), 4765–4800 (2023)
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–121. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33170-1_7
Dwivedi, R., et al.: Explainable AI (XAI): core ideas, techniques, and solutions. ACM Comput. Surv. 55(9), 194:1–194:33 (2023)
Fathi, E., Shoja, B.M.: Deep neural networks for natural language processing. In: Handbook of Statistics, vol. 38, pp. 229–316. Elsevier (2018)
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–42 (2018)
Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. Commun. ACM 55(8), 97–105 (2012)
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)
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–5158 (2020). https://www.ijcai.org/
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)
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–224 (2010)
Jüngermann, F., Kretínský, J., Weininger, M.: Algebraically explainable controllers: decision trees and support vector machines join forces. CoRR arXiv:2208.1280 (2022)
LeCun, Y., Cortes, C., Burges, C.J.: The MNIST database (1998). http://yann.lecun.com/exdb/mnist. Accessed 13 Aug 2022
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–31 July 2020, pp. 232–238. ACM (2020)
Liang, W., et al.: Advances, challenges and opportunities in creating data for trustworthy AI. Nat. Mach. Intell. 4(8), 669–677 (2022)
Lundberg, S.M., Lee, S.: A unified approach to interpreting model predictions. In: NIPS, pp. 4765–4774 (2017)
Marques-Silva, J., Ignatiev, A.: Delivering trustworthy AI through formal XAI. In: AAAI, pp. 12342–12350. AAAI Press (2022)
Minh, D., Wang, H.X., Li, Y.F., Nguyen, T.N.: Explainable artificial intelligence: a comprehensive review. Artif. Intell. Rev., 1–66 (2022)
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–71 (2018)
Molnar, C.: Interpretable Machine Learning, 2 edn. (2022). https://christophm.github.io/interpretable-ml-book
Morton, K., Hallahan, W.T., Shum, E., Piskac, R., Santolucito, M.: Grammar filtering for syntax-guided synthesis. In: AAAI, pp. 1611–1618. AAAI Press (2020)
Neider, D., Ghosh, B.: Probably approximately correct explanations of machine learning models via syntax-guided synthesis. arXiv preprint arXiv:2009.08770 (2020)
Pedregosa, F., et al.: Scikit-learn: machine learning in python. J. Mach. Learn. Res. 12, 2825–2830 (2011)
Ranjbar, N., Safabakhsh, R.: Using decision tree as local interpretable model in autoencoder-based LIME. In: CSICC, pp. 1–7. IEEE (2022)
Ribeiro, M.T., Singh, S., Guestrin, C.: “Why Should I Trust You?” 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–1144 (2016)
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–19 July 2018, pp. 5103–5111 (2018). https://www.ijcai.org/
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)
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–5), 575–615 (2021)
Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: International Conference on Machine Learning (ICML), pp. 5045–5054. PMLR (2018)
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)
Wang, F., Cao, Z., Tan, L., Zong, H.: Survey on learning-based formal methods: taxonomy, applications and possible future directions. IEEE Access 8, 108561–108578 (2020)
Acknowledgements
This work was supported in part from the European Union’s Horizon 2020 research and innovation programme under grant agreement N\(^\circ \) 956123 - FOCETA, by the State Government of Styria, Austria - Department Zukunftsfonds Steiermark, by the United States Office of Naval Research (ONR) through a National Defense Science and Engineering (NDSEG) Graduate Fellowship, and by the United States National Science Foundation (NSF) award CCF-2131476. The authors thank Benedikt Maderbacher and William Hallahan for their assistance with SyGuS encodings, and Timos Antonopoulos for his helpful comments on an earlier draft.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix
Appendix
Decision logic representation for an MNIST mimic program \(P_{f,100}\), showing the progression of pixel comparisons.
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Bjørner, K. et al. (2024). Formal XAI via Syntax-Guided Synthesis. In: Steffen, B. (eds) Bridging the Gap Between AI and Reality. AISoLA 2023. Lecture Notes in Computer Science, vol 14380. Springer, Cham. https://doi.org/10.1007/978-3-031-46002-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-46002-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-46001-2
Online ISBN: 978-3-031-46002-9
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science