Model Checking Verification of MultiLayer Perceptrons in Datalog: a Many-valued Approach with Typicality Francesco Bartoli1 , Marco Botta1 , Roberto Esposito1 , Laura Giordano2 and Daniele Theseider Dupré2 1 Dipartimento di Informatica, Università di Torino, Italy 2 DISIT - Università del Piemonte Orientale, Alessandria, Italy Abstract Description logics with typicality have been considered under a “concept-wise” multi-preferential semantics as the basis of a logical interpretation of MultiLayer Perceptrons (MLPs). In this paper we exploit a Datalog-based approach to prove logical properties of a trained network by model checking, starting from its input/output behavior, building a many-valued preferential model for the verification of typicality properties. The model is also used for providing a probabilistic account of MLPs, exploiting typicality concepts and Zadeh’s probability of fuzzy events. We report about some experiments to the verification of properties of neural networks for the recognition of basic emotions. This work is a step in the direction of verifying and interpreting knowledge learned by a neural network, to achieve a trustworthy and explainable AI. Keywords Description Logic, Typicality, Neural Networks, Explainability 1. Introduction Preferential approaches to common sense reasoning [1, 2, 3, 4, 5], have been extended to description logics (DLs) to deal with inheritance with exceptions in ontologies, by allowing for non-strict inclusions, called typicality or defeasible inclusions, with different preferential semantics, e.g., [6, 7] and [8, 9], and closure constructions, e.g, [10, 11, 12, 9]. In recent work, a concept-wise multipreference semantics has been proposed [13] as a semantics for ranked Description Logic (DL) knowledge bases (KBs), i.e. knowledge bases in which defeasible or typicality inclusions of the form T(C) ⊑ D (meaning “the typical C’s are D’s" or “normally C’s are D’s"), stemming from KLM conditionals [1, 3], are given a rank, Datalog 2.0 2022: 4th International Workshop on the Resurgence of Datalog in Academia and Industry, September 05, 2022, Genova - Nervi, Italy $ francesco.bartoli@edu.unito.it (F. Bartoli); marco.botta@unito.it (M. Botta); roberto.esposito@unito.it (R. Esposito); laura.giordano@uniupo.it (L. Giordano); dtd@uniupo.it (D. Theseider Dupré) € http://informatica.unito.it/persone/marco.botta/ (M. Botta); http://informatica.unito.it/persone/roberto.esposito (R. Esposito); http://people.unipmn.it/laura.giordano/ (L. Giordano); http://people.unipmn.it/dtd/ (D. Theseider Dupré)  0000-0001-5366-292X (R. Esposito); 0000-0001-9445-7770 (L. Giordano); 0000-0001-6798-4380 (D. Theseider Dupré) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 54 Francesco Bartoli et al. CEUR Workshop Proceedings 54–67 representing their strength, where T is a typicality operator [6], that singles out the typical instances of concept C. The multi-preferential semantics has been extended [14] to weighted knowledge bases, in which typicality inclusions have a real (positive or negative) weight, representing plausibility or implausibility. The semantics has been exploited to provide a preferential interpretation to Multilayer Perceptrons (MLPs, [15]), an approach previously considered [16, 17] for self- organising maps (SOMs, [18]). In both cases, considering the domain of all input stimuli presented to the network during training (or in the generalization phase), one can build a semantic interpretation of the network as a multi-preferential interpretation, where preferences are associated to concepts. This allows properties of a neural network to be verified by model checking over a fuzzy preferential interpretation. A MLP can as well be regarded as a weighted conditional knowledge base [14] (based on a fuzzy concept-wise preferential semantics) by interpreting synaptic connections as conditional implications. Specifically, the notions of coherent [14], faithful [19] and φ-coherent [20] models of a weighted ALC knowledge base have been considered for fuzzy ALC with typicality. In previous work, proof methods for reasoning with weighted conditional KBs have been studied, in the two-valued case [21] for EL⊥ KBs, and in the finitely many-valued case [22], providing an approximation of fuzzy φ-coherent entailment for the boolean fragment. Finitely many-valued DLs are well-studied in the literature [23, 24, 25, 26]. In particular, for the boolean fragment LC of ALC (which does not contain roles, and then neither universal nor existential restrictions), the finitely many-valued Gödel and Łukasiewicz description logics, Gn LC and Łn LC, have been extended with a typicality operator, and a semantic closure construction, based on φn -coherent interpretations, has been introduced to deal with weighted KBs. ASP and asprin [27] have been exploited for deciding φn -coherent entailment, a many-valued approximation of φ-coherence entailment, and the ASP encoding is used to prove that the problem is in Πp2 [22]. In this paper, we investigate a Datalog-based approach to model checking for verifying the logical properties of a neural network, by constructing a preferential interpretation of the network starting from its input/output behavior over a set of input stimuli. We exploit the activations of units for those stimuli, to define a many-valued interpretation of the concepts associated with those units (namely, the units of interest for verification). More specifically, we exploit Datalog with weakly stratified negation [28] in the construction of the model of a neural network N over a given domain ∆ of input stimuli. This allows the verification in polynomial time of typicality properties of the form T(C) ⊑ Dθα, for θ ∈ {≥, ≤, >, <} and α ∈ [0, 1], as well as to evaluate the conditional probabilities P (D|C), based on Zadeh’s probability of fuzzy events [29], also including occurrences of typicality concepts T(C). We conclude the paper by reporting about some experiments to the verification of properties of neural networks for the recognition of basic emotions using the Facial Action Coding System (FACS) [30]. 55 Francesco Bartoli et al. CEUR Workshop Proceedings 54–67 2. A fuzzy and a finitely many-valued description logic Fuzzy description logics have been widely studied in the literature for representing vagueness in DLs [31, 32, 33], based on the idea that concepts and roles can be interpreted as fuzzy sets and fuzzy relations. In fuzzy logic, formulas have a truth degree from a truth space S, usually [0, 1], as in Mathematical Fuzzy Logic [34] or {0, n1 , . . . , n−1 n , n }, for an integer n ≥ 1. The n finitely many-valued case is also well studied for DLs [23, 24, 25, 26]; in the following, we will also consider a finitely many-valued extension of the boolean fragment of ALC with typicality. Let LC be the fragment of ALC with no roles, NC be a set of concept names and NI a set of individual names. The set of LC concepts can be defined inductively as follows: (i) A ∈ NC , ⊤ and ⊥ are concepts; (ii) if C and D are concepts, then C ⊓ D, C ⊔ D, ¬C are concepts. A fuzzy interpretation for LC is a pair I = ⟨∆, ·I ⟩ where ∆ is a non-empty domain and · is fuzzy interpretation function that assigns to each concept name A ∈ NC a function I AI : ∆ → [0, 1], and to each individual name a ∈ NI an element aI ∈ ∆. A domain element x ∈ ∆ belongs to the extension of A to some degree in [0, 1], i.e., AI is a fuzzy set. The interpretation function ·I is extended to complex concepts as follows: ⊤I (x) = 1 ⊥I (x) = 0 (¬C)I (x) = ⊖C I (x) (C ⊓ D)I (x) = C I (x) ⊗ DI (x) (C ⊔ D)I (x) = C I (x) ⊕ DI (x) where x ∈ ∆ and ⊗, ⊕, ▷ and ⊖ are arbitrary but fixed t-norm, s-norm, implication function, and negation function, chosen among the combination functions of various fuzzy logics (we refer to [32] for details). In particular, in Gödel logic a ⊗ b = min{a, b}, a ⊕ b = max{a, b}, a ▷ b = 1 if a ≤ b and b otherwise; ⊖a = 1 if a = 0 and 0 otherwise. In Łukasiewicz logic, a ⊗ b = max{a + b − 1, 0}, a ⊕ b = min{a + b, 1}, a ▷ b = min{1 − a + b, 1} and ⊖a = 1 − a. The interpretation function ·I is also extended to non-fuzzy axioms (i.e., to strict inclusions and assertions of an LC knowledge base) as follows: (C ⊑ D)I = infx∈∆ C I (x) ▷ DI (x) (C(a))I = C I (aI ) A fuzzy LC knowledge base K is a pair (T , A) where T is a fuzzy TBox and A a fuzzy ABox. A fuzzy TBox is a set of fuzzy concept inclusions of the form C ⊑ D θ α, where C ⊑ D is an LC concept inclusion axiom, θ ∈ {≥, ≤, >, <} and α ∈ [0, 1]. A fuzzy ABox A is a set of fuzzy assertions of the form C(a) θα where C is an LC concept, a ∈ NI , θ ∈ {≥, ≤, >, <} and α ∈ [0, 1]. Following Bobillo and Straccia [35], we assume that fuzzy interpretations are witnessed, i.e., the sup and inf are attained at some point of the involved domain. Definition 1 (Satisfiability and entailment). A fuzzy interpretation I satisfies a fuzzy LC axiom E (denoted I |= E), as follows: - I satisfies a fuzzy LC inclusion axiom C ⊑ D θ α if (C ⊑ D)I θ α; - I satisfies a fuzzy LC assertion C(a)θα if C I (aI )θ α, for θ ∈ {≥, ≤, >, <}. 56 Francesco Bartoli et al. CEUR Workshop Proceedings 54–67 Given a fuzzy KB K = (T , A), a fuzzy interpretation I satisfies T (resp. A) if I satisfies all fuzzy inclusions in T (resp. all fuzzy assertions in A). A fuzzy interpretation I is a model of K if I satisfies T and A. A fuzzy axiom E is entailed by a fuzzy knowledge base K, written K |= E, if for all models I =⟨∆, ·I ⟩ of K, I satisfies E. In the finitely many-valued case, we assume the truth space to be Cn = {0, n1 , . . . , n−1 n , n }, for n an integer n ≥ 1. A finitely many-valued interpretation for LC is a pair I = ⟨∆, · ⟩ where: ∆ is I a non-empty domain and ·I is an interpretation function that assigns to each a ∈ NI a value aI ∈ ∆, and to each A ∈ NC a function AI : ∆ → Cn . In particular, in [22] we have considered two finitely many-valued cases based on ALC, the finitely many-valued Łukasiewicz description logic Łn ALC and the finitely many-valued Gödel description logic Gn ALC, extended with a standard involutive negation ⊖a = 1 − a. Such logics are defined along the lines of the finitely many-valued Łukasiewicz description logic SROIQ [24], the fuzzy extension of the descrption logic SROIQ that joins Gödel and Zadeh fuzzy logics (called GZ SROIQ) [25], and the logic ALC ∗ (S) [23]. In the following we will focus on the LC fragment Gn LC of Gn ALC. For Gn LC the interpretation function ·I is extended to complex concepts and fuzzy axioms as above, and we assume the interpretation of negated concepts exploits involutive negation, i.e., (¬C)I (x) = ⊖C I (x) = 1 − C I (x). The notions of knowledge base, satisfiability and entailment are defined as above. 3. Fuzzy LC with typicality and φ-coherent models Let us consider now fuzzy LC with typicality LC F T, following the approach for ALC in [14, 19], as well as the finite many-valued case. The idea is similar to the extension of ALC with typicality in the two-valued case [6], but the degree of membership of domain individuals in a concept C is used to identify the typical elements of C. The extension allows for the definition of typicality concepts of the form T(C), corresponding to the set of most typical C-elements. Note that, in a fuzzy interpretation I = ⟨∆, ·I ⟩, the degree of membership C I (x) of x in a concept C induces a preference relation CI (y) For a witnessed fuzzy LC interpretation I, each preference relation 0 I = {x ∈ ∆ | C I (x) > 0}. One can provide a (crisp) interpretation of typicality concepts T(C) in an interpretation I as follows: if x ∈ min0 I ) {︃ 1 I (T(C)) (x) = (1) 0 otherwise where min< (S) = {u : u ∈ S and ∄z ∈ S s.t. z < u}. When (T(C))I (x) = 1, x is said to be a typical C-element in I. Let us denote with LC F T the extension of fuzzy LC with typicality, and with Gn LCT the extension of Gn LC with typicality. 57 Francesco Bartoli et al. CEUR Workshop Proceedings 54–67 Definition 2 ( LC F T interpretation). A LC F T interpretation I = ⟨∆, ·I ⟩ is a fuzzy LC in- terpretation, extended by interpreting typicality concepts as in (1). In a similar way, we can define a Gn LCT interpretation: a many-valued interpretation I = ⟨∆, ·I ⟩ implicitly defines a multi-preferential interpretation, where any concept C is associated to a preference relation