One of the main challenges in modern AI systems is to explain the decisions of complex machine learning models, and recent years have seen a burgeoning of novel approaches. These approaches often rely on some structural components of the models under consideration, e.g., the set of features used for the classification task. As a result, explanations provided by these approaches are expressed in terms of the sub-symbolic information and, therefore, they are hard to interpret for users. In this paper, we argue that, in order to foster interpretability, these explanations should be expressed in terms of the knowledge that the users posses on the underlying application domain rather than on the sub-symbolic components of the model. To this end, our first contribution is the illustration of a novel formal framework for explaining the decisions of machine learning classifiers grounded on the Ontology-Based Data Management paradigm. Within this framework, explanations are defined by logical formulae using the symbols that an ontology defines and, as such, they posses a well-defined semantics. As a second contribution, we provide an algorithm that computes the best explanations that can be expressed in the class of conjunctive queries.
Classifiers form a prominent family of modern AI systems. Intuitively, a classifier is a systems used to
predict whether an object belongs to a specific class given a set of its relevant attributes [
While explanations based on raw data attributes may convey some information to AI Experts, it is often hard for general users to understand their meaning. This is especially true in the typical machine learning scenario where attributes are the results of a complex process of feature selection and carry little to no meaning by themselves. The goal of our work is to define a novel framework to express explanations using conceptual properties of the scenario of interest that are not limited by the data attributes used by the classifier.
Our framework is based on the notion of mappings, well-known by the AI community and widely used in the context of Information Integration [7] and Ontology-Based Data Management [8]. These mappings define the relation between the objects of the world that are relevant for a classifier and a set of conceptual notions that are relevant for the application domain. To formalize these conceptual notions, our framework makes use of ontologies that formalize the application domain. Combining domain ontologies and mappings is a well-established approach to lift information about raw data to the conceptual level [9, 10, 11, 12]. In our framework, these combinations, called ontological specifications , are used to formalize the relation between the classifier whose behavior we want to explain and the notions that users understand. We then use ontological specifications to provide a local explanation of a classifier expressed at the conceptual level of their ontologies via their mappings . In this way, we obtain explanations expressed as logical formulae over the symbols of the ontology and grounded on a formal semantics.
In this context, the contribution of this paper is the following. Firstly, we present the framework of ontological specifications together with a suitable notion of explanation (Section 2). Secondly, when ontologies and mappings are expressed in reasonably expressive languages, we study the computational complexity of verifying whether a given formula is an explanation. Finally, we present a general algorithm for the computation of best explanations (Section 3).
We proceed to present our framework for semantic explanations of ML models. Assume a possibly infinite set ∆ of elements that we call instances. Intuitively, ∆ is the set of all possible elements that the instance space of an ML model in our framework may possibly contain. Observe that instances are not yet characterized by their attributes as it is customary in learning algorithms. To bridge this gap, we further assume a countably infinite set A of unary function symbols that we call the set of attribute symbols. To each ∈ A, we associate a surjective function sem : ∆ → that we call the semantics of . Whenever the co-domain of sem is finite, we say that is a finite attribute . Intuitively, a pair = ⟨∆ , A⟩ provides a formal background to instance space elements and, for this reason, we refer to it as a data layer.
A classifier for ∆ is a function from ∆ to {0, 1}. Usually, classifiers operate on a restricted set of attributes of the input instances. To capture this property, we say that a classifier operates over a set of attributes ⊆ A if, for every pair , ′ ∈ ∆ , the fact that () = (′), for each ∈ , implies () = (′). We will call relevant attributes for . A classifier for ∆ is a -classifier if there exists a unique and finite set of relevant attributes ⊆ A for .
Let be the set of all possible values that an attribute in A may take, i.e., = ⋃︀ . We assume two countably infinite sets F and C of function symbols and relation symbols, respectively. For each ∈ F with arity , the semantics of is a function sem : → . Similarly, for each ∈ C with arity , the semantics of is a relation sem ⊆ . Intuitively, A, F, and C will form the terms of our declarative language. Assume a countably infinite set of variables , the set (F, C) is the set of all the expressions of the following forms: , with ∈ ∆ , (), with ∈ A and ∈ , or (1, . . . , ), with a function symbol of arity in F and 1, . . . , ∈ (F, C). The language ℒ(F, C) is defined as the set of all first-order formulae that can be expressed using terms in (F, C). The semantics of ℒ(F, C) is defined as customary using , sem, and sem to interpret ∈ ∆ , ∈ A and ∈ F, respectively. Given ∈ ℒ(F, C) with free variables ¯ and a function : → ∆ , we write |= to say that the formula obtained from by replacing each ∈ ¯ with () is true.
Assume a countably infinite set of predicate symbols P disjoint from C. A mapping assertion from ℒ(F, C) to P is an expression of the form ⟨ (), ()⟩ where () is a formula in ℒ(F, C) with one free variable and () is a first-order formula over P with the single free variable . A mapping from ℒ(F, C) to P is a finite set of mapping assertions from ℒ(F, C) to P. Intuitively, mappings define the connection between the instances in the data layer and the predicates in P. To express such connection, we use ontological specifications .
Formally, an ontological specification for ℒ(F, C) to P (simply, ontological specification) is a pair = ⟨, ⟩ where is a first-order theory over P and is a mapping from ℒ(F, C) to P. The semantics of an ontological specification is defined in terms of its models. An interpretation for P (simply, interpretation) is a first-order logic interpretation ℐ for the symbols of P whose domain is ∆ . Given a mapping assertion = ⟨, ⟩, we say that ℐ satisfies , if, for every function : → ∆ , |= implies , ℐ |= . A model for is an interpretation ℐ such that ℐ satisfies and ℐ satisfies , for each ∈ . We use () for the set of all models of ℐ.
With ontological specifications in place, we are now ready to formalize our notion of explanation. the notion of explanation we are looking for.
Let be an ontological specification as above and a first-order formula over P. We use (, ) for the set { ∈ ∆
| ∈ ℐ , for each ℐ ∈ ()}. Assume now a classifier for the data layer and an instance ∈ ∆ . A Weak Ontology-Based eXplanations (w-OBX) for the decision of over based on is a first-order formula () over the alphabet P and one free variable with the following properties: ∈ (, ), and, () = (), for each ∈ (, ). The next definition formalizes Definition 1. Let be a language of first-order formulae over P. A w-OBX for the decision of over for the decision of over based on such that ′ ∈ and (, ) ⊊ ( ′, ). based on is the best Ontology-Based Explanation in (-OBX) if ∈ and there exists no w-OBX ′ ℒ(F, C) formula: ︁( (︀ 1 2 · (() + ()))︀ ≥ 5
︁) Example 1. Consider a scenario where a classifier is used to provide movie recommendations. The relevant attributes for are (Critic Rating) and (Public Rating) with domain [0, 10]; and (Low Budget) and (Famous Cast) with domain {, }. Moreover, () = 1 if and only if satisfies the following ∧ ( () = ). Intuitively, recommends a movie if it received a good average score from critics and public and it stars non-famous actors. Suppose that we want to explain the decision () = 1 taken by for the movie such that () = 10, () = 10, () = , () = . For the explanation, we want to use the ontological symbols (Publicly Acclaimed), (Critically Acclaimed), (B-Movie), and (Cult Movie). Let and be, respectively, the decision of over based on , where CQ is the language of conjunctive queries.
TBox { ⊑ ; ⊑ ; } and mapping {1, 2, 3} with 1 = {(() = 10), ()}, 2 = {(() = 10), (); 3 = {(︀ (() = ) ∧ ( () = ))︀ , ()}. Let = ⟨, ⟩. It is easy to verify that the following are all w-OBX for the decision of over based on : ( ()∧ ()), (() ∧ ()), and ( () ∧ ()). However, () ∧ () is the only CQ-OBX for the
of the decision of over based on .
Theorem 1. Verification is coNP-complete.
Let ℒ−(F, C) be the quantifier-free subset of ℒ(F, C) that uses only finite attributes. In what follows, we assume that ) classifiers and formulae () in the left-hand side of mapping assertions are defined ∃.(, ), and ∃.(, ); ) theories over P are formulated in DL-Liteℛ in ℒ−(F, C); ) the right-hand side of mapping assertions allows only for formulae of the form (), [13]; and ) the language for expressing explanations is the class of conjunctive queries CQ. In this scenario, we consider the following computational problems. Verification: given also a CQ () over the alphabet P, check whether is a w-OBX of the decision of over based on ; Computation: compute all the CQ-OBXs
Next, we provide a technique to return the set of all CQ-OBXs of the decision of over based on (clearly, if two formulae () and ′() are such that (, ) = (′, ), then we say that they are equivalent w.r.t. and treat them as the same formula).
Given an instance ∈ ∆ and a mapping from ℒ(F, C) to P in our considered scenario, we denote by () the set of atoms obtained by chasing the instance w.r.t. , i.e: () contains the atom () (resp. ∃(), ∃− ()) if and only if there exists a mapping assertion of the form ⟨ (), ()⟩ (resp. ⟨ (), ∃.(, )⟩, ⟨ (), ∃.(, )⟩) in such that () is true. Furthermore, given a set () of atoms as above, we denote by () the CQ obtained by conjoining all the atoms in (), where we select a free variable and each atom of the form () is replaced with (), and each atom of the form ∃() (resp. ∃− ()) is replaced with ∃.(, ) (resp. ∃.(, )) in which is always a fresh existential variable. Given an instance ∈ ∆ and an ontology = ⟨, ⟩ in our scenario, we now prove that () is actually the smallest (up to equivalence w.r.t. ) CQ such that ∈ ( , ), in the sense that there exists no other CQ () for which ∈ (, ) and there is an instance ∈ ∆ satisfying ∈ ( , ) and ̸∈ (, ).
Proposition 1. Given an instance ∈ ∆ and an ontology = ⟨, ⟩, we have that () is the smallest (up to equivalence w.r.t. ) CQ such that ∈ ( , ).
Given an instance ∈ ∆ and an ontology = ⟨, ⟩ in our considered scenario, we denote by () the set of atoms obtained from () by adding the atom () if and only if there exists an atom of the form ′() ∈ () and |= ′ ⊑ , where both and ′ can be any basic DL-Liteℛ concept, i.e. concepts of the form , ∃, and ∃− with and in P.
Theorem 2. Let be a classifier, ∈ ∆ be an instance, = ⟨, ⟩ be an ontology specification, and () be a CQ-OBX of the decision over w.r.t. . We have that () is equivalent w.r.t. to a query of the form ′ (), where ′ ⊆ ().
Actually, the above results suggest a naive algorithm to compute the set of all the CQ-OBXs. Specifically, it is enough to consider all the possible ′ (), where ′ ⊆ (), and check that 1) ′ () is a w-OBX of the decision over based on , and 2) there is no other ′′ ⊆ () for which ′′ () is a w-OBX of the decision over based on and the formula PerfectRef( ′ , ) is strictly contained in the formula PerfectRef( ′′ , ), meaning that it can be the case that ( ′ , ) ⊊ ( ′′ , ). Here, PerfectRef denotes the algorithm used for rewriting CQs w.r.t. DL-Liteℛ TBoxes [13].
This work has been supported by MUR under the PNRR project FAIR (PE0000013) and by the EU under the H2020-EU.2.1.1 project TAILOR (grant id. 952215). [7] M. Lenzerini, Data integration: A theoretical perspective., in: Proceedings of the Twenty-First ACM SIGACT SIGMOD SIGART Symposium on Principles of Database Systems (PODS 2002), 2002, pp. 233–246. [8] M. Lenzerini, Ontology-based data management, in: Proceedings of the Twentieth International Conference on Information and Knowledge Management (CIKM 2011), 2011, pp. 5–6. doi:10. 1145/2063576.2063582. [9] G. Cima, M. Console, M. Lenzerini, A. Poggi, A review of data abstraction, Frontiers Artif. Intell. 6 (2023). URL: https://doi.org/10.3389/frai.2023.1085754. doi:10.3389/FRAI.2023.1085754. [10] F. Croce, G. Cima, M. Lenzerini, T. Catarci, Ontology-based explanation of classifiers, in: A. Poulovassilis, D. Auber, N. Bikakis, P. K. Chrysanthis, G. Papastefanatos, M. A. Sharaf, N. Pelekis, C. Renso, Y. Theodoridis, K. Zeitouni, T. Cerquitelli, S. Chiusano, G. Vargas-Solar, B. OmidvarTehrani, K. Morik, J. Renders, D. Firmani, L. Tanca, D. Mottin, M. Lissandrini, Y. Velegrakis (Eds.), Proceedings of the Workshops of the EDBT/ICDT 2020 Joint Conference, Copenhagen, Denmark, March 30, 2020, volume 2578 of CEUR Workshop Proceedings, CEUR-WS.org, 2020. URL: https://ceur-ws.org/Vol-2578/PIE3.pdf. [11] T. Catarci, M. Scannapieco, M. Console, C. Demetrescu, My (fair) big data, in: J. Nie, Z. Obradovic, T. Suzumura, R. Ghosh, R. Nambiar, C. Wang, H. Zang, R. Baeza-Yates, X. Hu, J. Kepner, A. Cuzzocrea, J. Tang, M. Toyoda (Eds.), 2017 IEEE International Conference on Big Data (IEEE BigData 2017), Boston, MA, USA, December 11-14, 2017, IEEE Computer Society, 2017, pp. 2974–2979. URL: https://doi.org/10.1109/BigData.2017.8258267. doi:10.1109/BIGDATA.2017.8258267. [12] G. Cima, A. Poggi, M. Lenzerini, The notion of abstraction in ontology-based data management,
Artificial Intelligence 323 (2023) 103976. [13] D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Tractable reasoning and eficient query answering in description logics: The DL-Lite family, Journal of Automated Reasoning 39 (2007) 385–429.