Document Open Access Logo

Anytime Approximate Formal Feature Attribution

Authors Jinqiang Yu , Graham Farr, Alexey Ignatiev , Peter J. Stuckey

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.30.pdf
  • Filesize: 5.79 MB
  • 23 pages

Document Identifiers

Author Details

Jinqiang Yu
  • Department of Data Science and AI, Monash University, Melbourne, Australia
  • Australian Research Council OPTIMA ITTC, Melbourne, Australia
Graham Farr
  • Department of Data Science and AI, Monash University, Melbourne, Australia
Alexey Ignatiev
  • Department of Data Science and AI, Monash University, Melbourne, Australia
Peter J. Stuckey
  • Department of Data Science and AI, Monash University, Melbourne, Australia
  • Australian Research Council OPTIMA ITTC, Melbourne, Australia

Funding

This research was partially funded by the Australian Government through the Australian Research Council Industrial Transformation Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA), Project ID IC200100009.

Cite AsGet BibTex

Jinqiang Yu, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey. Anytime Approximate Formal Feature Attribution. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.30

Abstract

Widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models on the one hand and a number of crucial issues pertaining to them warrant the need for explainable artificial intelligence (XAI). A key explainability question is: given this decision was made, what are the input features which contributed to the decision? Although a range of XAI approaches exist to tackle this problem, most of them have significant limitations. Heuristic XAI approaches suffer from the lack of quality guarantees, and often try to approximate Shapley values, which is not the same as explaining which features contribute to a decision. A recent alternative is so-called formal feature attribution (FFA), which defines feature importance as the fraction of formal abductive explanations (AXp’s) containing the given feature. This measures feature importance from the view of formally reasoning about the model’s behavior. Namely, given a system of constraints logically representing the ML model of interest, computing an AXp requires finding a minimal unsatisfiable subset (MUS) of the system. It is challenging to compute FFA using its definition because that involves counting over all AXp’s (equivalently, counting over MUSes), although one can approximate it. Based on these results, this paper makes several contributions. First, it gives compelling evidence that computing FFA is intractable, even if the set of contrastive formal explanations (CXp’s), which correspond to minimal correction subsets (MCSes) of the logical system, is provided, by proving that the problem is #P-hard. Second, by using the duality between MUSes and MCSes, it proposes an efficient heuristic to switch from MCS enumeration to MUS enumeration on-the-fly resulting in an adaptive explanation enumeration algorithm effectively approximating FFA in an anytime fashion. Finally, experimental results obtained on a range of widely used datasets demonstrate the effectiveness of the proposed FFA approximation approach in terms of the error of FFA approximation as well as the number of explanations computed and their diversity given a fixed time limit.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Computing methodologies → Machine learning
Keywords
  • Explainable AI
  • Formal Feature Attribution
  • Minimal Unsatisfiable Subsets
  • MUS Enumeration

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In CAV, pages 70-86, 2015. Google Scholar
  2. James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In PADL, pages 174-186, 2005. Google Scholar
  3. Anton Belov, Ines Lynce, and Joao Marques-Silva. Towards efficient MUS extraction. AI Commun., 25(2):97-116, 2012. Google Scholar
  4. Jaroslav Bendík, Ivana Cerná, and Nikola Benes. Recursive online enumeration of all minimal unsatisfiable subsets. In ATVA, pages 143-159, 2018. Google Scholar
  5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability: Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  6. Elazar Birnbaum and Eliezer L. Lozinskii. Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell., 15(1):25-46, 2003. Google Scholar
  7. Karthekeyan Chandrasekaran, Richard M. Karp, Erick Moreno-Centeno, and Santosh S. Vempala. Algorithms for implicit hitting set problems. In SODA, pages 614-629, 2011. Google Scholar
  8. Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In KDD, pages 785-794, 2016. Google Scholar
  9. Peter Clark and Robin Boswell. Rule induction with CN2: some recent improvements. In EWSL, pages 151-163, 1991. Google Scholar
  10. Li Deng. The MNIST database of handwritten digit images for machine learning research. IEEE Signal Processing Magazine, 29(6):141-142, 2012. Google Scholar
  11. Jerome H. Friedman. Greedy function approximation: A gradient boosting machine. The Annals of Statistics, 29(5):1189-1232, 2001. Google Scholar
  12. Enrico Giunchiglia and Marco Maratea. Solving optimization problems with DLL. In ECAI, pages 377-381, 2006. Google Scholar
  13. Éric Grégoire, Yacine Izza, and Jean-Marie Lagniez. Boosting MCSes enumeration. In IJCAI, pages 1309-1315, 2018. Google Scholar
  14. Addison Howard, Devrishi, Phil Culliton, and Yufeng Guo. Natural language processing with disaster tweets, 2019. URL: https://kaggle.com/competitions/nlp-getting-started.
  15. Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, and João Marques-Silva. Feature necessity & relevancy in ML classifier explanations. In TACAS (1), pages 167-186, 2023. Google Scholar
  16. Xuanxiang Huang and João Marques-Silva. The inadequacy of Shapley values for explainability. CoRR, abs/2302.08160, 2023. Google Scholar
  17. Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El-Yaniv, and Yoshua Bengio. Binarized neural networks. In NIPS, pages 4107-4115, 2016. Google Scholar
  18. Laurent Hyafil and Ronald L. Rivest. Constructing optimal binary decision trees is NP-complete. Inf. Process. Lett., 5(1):15-17, 1976. Google Scholar
  19. Alexey Ignatiev, Mikolas Janota, and Joao Marques-Silva. Quantified maximum satisfiability. Constraints An Int. J., 21(2):277-302, 2016. Google Scholar
  20. Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques-Silva. From contrastive to abductive explanations and back again. In AI*IA, pages 335-355, 2020. URL: https://doi.org/10.1007/978-3-030-77091-4_21.
  21. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. Abduction-based explanations for machine learning models. In AAAI, pages 1511-1519, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011511.
  22. Maurice G Kendall. A new measure of rank correlation. Biometrika, 30(1/2):81-93, 1938. Google Scholar
  23. Ron Kohavi. Scaling up the accuracy of naive-Bayes classifiers: A decision-tree hybrid. In KDD, pages 202-207, 1996. Google Scholar
  24. Solomon Kullback and Richard A Leibler. On information and sufficiency. The annals of mathematical statistics, 22(1):79-86, 1951. Google Scholar
  25. Himabindu Lakkaraju, Stephen H. Bach, and Jure Leskovec. Interpretable decision sets: A joint framework for description and prediction. In KDD, pages 1675-1684. ACM, 2016. Google Scholar
  26. Mark Liffiton and Ammar Malik. Enumerating infeasibility: Finding multiple MUSes quickly. In CPAIOR, pages 160-175, 2013. Google Scholar
  27. Mark Liffiton and Ammar Malik. Enumerating infeasibility: Finding multiple muses quickly. In CPAIOR, pages 160-175, 2013. Google Scholar
  28. Mark H. Liffiton, Maher N. Mneimneh, Ines Lynce, Zaher S. Andraus, Joao Marques-Silva, and Karem A. Sakallah. A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints An Int. J., 14(4):415-442, 2009. Google Scholar
  29. Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. Fast, flexible MUS enumeration. Constraints An Int. J., 21(2):223-250, 2016. Google Scholar
  30. Mark H. Liffiton and Karem A. Sakallah. On finding all minimally unsatisfiable subformulas. In SAT, pages 173-186, 2005. Google Scholar
  31. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1):1-33, 2008. Google Scholar
  32. Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In NeurIPS, pages 4765-4774, 2017. URL: https://proceedings.neurips.cc/paper/2017/hash/8a20a8621978632d76c43dfd28b67767-Abstract.html.
  33. Joao Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explanations for monotonic classifiers. In ICML, pages 7469-7479, 2021. URL: http://proceedings.mlr.press/v139/marques-silva21a.html.
  34. Joao Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, and Anton Belov. On computing minimal correction subsets. In IJCAI, pages 615-622, 2013. Google Scholar
  35. João Marques-Silva and Xuanxiang Huang. Explainability is NOT a game. CoRR, abs/2307.07514, 2023. Google Scholar
  36. João Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. In AAAI, pages 12342-12350, 2022. Google Scholar
  37. Carlos Mencia, Alexey Ignatiev, Alessandro Previti, and Joao Marques-Silva. MCS extraction with sublinear oracle queries. In SAT, pages 342-360, 2016. Google Scholar
  38. Carlos Mencia, Alessandro Previti, and Joao Marques-Silva. Literal-based MCS extraction. In IJCAI, pages 1973-1979, 2015. Google Scholar
  39. Tim Miller. Explanation in artificial intelligence: Insights from the social sciences. Artif. Intell., 267:1-38, 2019. URL: https://doi.org/10.1016/J.ARTINT.2018.07.007.
  40. Rishabh Misra and Prahal Arora. Sarcasm detection using news headlines dataset. AI Open, 4:13-18, 2023. Google Scholar
  41. Rishabh Misra and Jigyasa Grover. Sculpting Data for ML: The first act of Machine Learning. Independently published, January 2021. Google Scholar
  42. Vinod Nair and Geoffrey Hinton. Rectified linear units improve restricted boltzmann machines. In ICML, pages 807-814, 2010. Google Scholar
  43. Nina Narodytska, Nikolaj Bjørner, Maria-Cristina V. Marinescu, and Mooly Sagiv. Core-guided minimal correction set and core enumeration. In IJCAI, pages 1353-1361, 2018. Google Scholar
  44. Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Z. Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. PyTorch: An imperative style, high-performance deep learning library. In NeurIPS, pages 8024-8035, 2019. Google Scholar
  45. Alessandro Previti and João Marques-Silva. Partial MUS enumeration. In AAAI. AAAI Press, 2013. Google Scholar
  46. Alessandro Previti, Carlos Mencía, Matti Järvisalo, and João Marques-Silva. Premise set caching for enumerating minimal correction subsets. In AAAI, pages 6633-6640, 2018. Google Scholar
  47. J. Scott Provan and Michael O. Ball. The complexity of counting cuts and of computing the probability that a graph is connected. SIAM J. Comput., 12(4):777-788, 1983. Google Scholar
  48. Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987. URL: https://doi.org/10.1016/0004-3702(87)90062-2.
  49. Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. "Why should I trust you?": Explaining the predictions of any classifier. In KDD, pages 1135-1144, 2016. URL: https://doi.org/10.1145/2939672.2939778.
  50. Ronald L. Rivest. Learning decision lists. Mach. Learn., 2(3):229-246, 1987. Google Scholar
  51. Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining Bayesian network classifiers. In IJCAI, pages 5103-5111, 2018. URL: https://doi.org/10.24963/IJCAI.2018/708.
  52. Salil Vadhan. The complexity of counting in sparse, regular, and planar graphs. SIAM J. Comput., 31(2):398-427, 2001. Google Scholar
  53. L. G. Valiant. The complexity of computing the permanent. Theoret. Comput. Sci., 8(2):189-201, 1979. Google Scholar
  54. William Webber, Alistair Moffat, and Justin Zobel. A similarity measure for indefinite rankings. ACM Transactions on Information Systems (TOIS), 28(4):1-38, 2010. Google Scholar
  55. Jiancheng Yang, Rui Shi, Donglai Wei, Zequan Liu, Lin Zhao, Bilian Ke, Hanspeter Pfister, and Bingbing Ni. MedMNIST v2-a large-scale lightweight benchmark for 2D and 3D biomedical image classification. Scientific Data, 10(1):41, 2023. Google Scholar
  56. Jinqiang Yu, Alexey Ignatiev, and Peter J. Stuckey. On formal feature attribution and its approximation. CoRR, abs/2307.03380, 2023. https://arxiv.org/abs/2307.03380, URL: https://doi.org/10.48550/arXiv.2307.03380.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact