Extensions to Generalized Annotated Logic and an Equivalent Neural Architecture

TL;DR

This paper introduces an extension to generalized annotated logic enabling a binarized neural network framework that integrates symbolic reasoning with discrete optimization, aiming to improve explainability and modularity in neural systems.

Contribution

It proposes a novel extension to generalized annotated logic for neuro symbolic systems, creating an equivalent neural architecture trained via discrete optimization.

Findings

Proofs of correctness for the proposed framework

Discussion of challenges for implementation

Extension to logic enabling neural-symbolic hybridization

Abstract

While deep neural networks have led to major advances in image recognition, language translation, data mining, and game playing, there are well-known limits to the paradigm such as lack of explainability, difficulty of incorporating prior knowledge, and modularity. Neuro symbolic hybrid systems have recently emerged as a straightforward way to extend deep neural networks by incorporating ideas from symbolic reasoning such as computational logic. In this paper, we propose a list desirable criteria for neuro symbolic systems and examine how some of the existing approaches address these criteria. We then propose an extension to generalized annotated logic that allows for the creation of an equivalent neural architecture comprising an alternate neuro symbolic hybrid. However, unlike previous approaches that rely on continuous optimization for the training process, our framework is designed as a binarized neural network that uses discrete optimization. We provide proofs of correctness and discuss several of the challenges that must be overcome to realize this framework in an implemented system.

Equations

$$r\equiv {\ell }_0:{\mu }_0$$

$${\ell }_0:{\mu }_0$$

$${\mathbf{T}}_{\Pi }(I)({\ell }_0)=\mathbf{sup}(annoSe{t}_{\Pi ,I}({\ell }_0)),$$

$$a:[0,0]\leftarrow$$

$$a:[1,1]\leftarrow$$

$$r\equiv a:[f_{a,{\theta }_a^i}^{(i)}(X_a^{(i)}),1]\leftarrow \underset{{\ell }_j\in {\mathcal{L}}^{\prime }}{\bigwedge }{\ell }_j:[x_j,x_j^{\prime }].$$

$$f_{a,{\theta }_a^i}^{(i)}(X_a^{(i)})=Sign(relu(1+\sum _{j}0.5(1+{\theta }_{a,j}^i)(x_j-1)))$$

$$incon:[-1,1]\leftarrow$$

$$incon:[Sign(x+y),1]\leftarrow a:[x,x^{\prime }]\wedge \neg a:[y,y^{\prime }]$$

Full text

I Introduction

While deep neural networks have led to major advances in image recognition, language translation, data mining, and game playing, there are well-known limits to the paradigm such as lack of explainability, difficulty of incorporating prior knowledge, and modularity [1]. Neuro symbolic hybrid systems have recently emerged as a straightforward way to extend deep neural networks by incorporating ideas from symbolic reasoning such as computational logic [2, 3, 4, 5, 6, 7, 8]. In this paper, we first propose a list of desirable criteria for a neuro symbolic system and examine how some of the existing approaches each address these criteria. We then propose an extension to generalized annotated logic [9] that allows for the creation of an equivalent neural architecture comprising an alternate neuro symbolic hybrid. However, unlike previous approaches that rely on continuous optimization for the training process, our framework is designed as a binarized neural network [10] that uses discrete optimization. We provide proofs of correctness and discuss several of the challenges that must be overcome to realize this framework in an implemented system.

The rest of this paper is organized as follows. In Section II we propose a list of desirable criteria and briefly discuss which of the current approaches meet the criteria. In Section III we review generalized annotated logic along with our extensions, mainly related to the use of interpretations for literals (as opposed to atoms) and the use of a lower semi-lattice (instead of an upper semi-lattice). This is followed by a section containing proofs related to our extensions to annotated logic (Section IV). This allows us to then introduce our parametrized rule structure (Section V) and associated neural architecture (Section VI). We discuss how this framework can identify inconsistencies in Section VII, briefly discuss in Section VIII how our framework meets the criteria, and conclude with a discussion of challenges (Section IX).

II Criteria to Consider in Neuro Symbolic Reasoning and Related Work

Inspired on the critique of deep learning in [1], we have derived the following criteria for a neuro symbolic system.

Support for symbolic inference for arbitrary queries 2. 2.

Symbolic explanation of results amenable to both further analysis and human interpretation 3. 3.

Ability to integrate prior knowledge and/or constraints 4. 4.

Strong assurances of consistency 5. 5.

Ability to learn rule structure, including classical (i.e., non-fuzzy) rules 6. 6.

Scalability

The framework of logic tensor networks (LTN) [7, 8] provides a neural symbolic approach where symbols have an associated vector representation that in turn allows, via the training process, for logical sentences (known a-priori) to be assigned weights where the intuition is related to a level of truth. This follows from fuzzy logic, similar to prior approaches combining fuzzy logic and machine learning [11]. The framework excels in its ability to conduct symbolic inference on queries and provide symbolic results in a scalable manner as well as the ability to incorporate prior knowledge. However, the framework does not allow for the learning of logical rules and it treats consistency as a component of the loss function, hence not guaranteeing consistency. We note that the lack of consistency assurances means that we do not have guarantees that prior knowledge is indeed integrated. Further, the system does not provide an explanation of how it obtained a symbolic result. In many ways, the capabilities of LTN’s are similar to deep ontological networks [12] (although the two differ significantly in how they handle training data). However, the explainability problem is more pronounced in ontological neural networks due to its use of embeddings. In summary, LTNs and deep ontological networks meet criteria 1, 3, and 6—they allow for symbolic reasoning and incorporation of prior knowledge in a scalable manner but do not make consistency guarantees, learn rule structure, nor provide explanatory results.

The framework of logical neural networks (LNN) [6] overcomes some of the explainability issues of LTN and deep ontological networks. However, like LTN, it still does not have hard consistency guarantees, as consistency is handled as a component of the loss function. Further, it is not capable of learning rules without a-prior knowledge of their structure. In short, LNNs meet criteria 1, 2, 3, and 6—they provide much of the same capabilities of LTN and deep ontological networks, but also provide an explainable result due to the 1-1 relationship between logical syntax and neural structure. However, they cannot guarantee consistency or learn rule structure.

Differentiable inductive logic programming (ILP) [5, 4] is designed to learn logical rules using gradient descent. This approach suffers from scalability issues as it involves generating a large number of “rule templates” and assigning them weights using gradient descent. Further, this approach only learns weighted (fuzzy) rules as opposed to classical ones and also does not provide strong consistency guarantees. In short, differentiable ILP excels at learning structure, though not in the classical sense (criterion 5) and provides a symbolic framework and explainability (criteria 1 and 2). The work as presented does not incorporate prior knowledge or ensure consistency (criteria 3 and 4), but future work could possilby provide those extensions. However, a key drawback of this approach is scalability (criterion 6) due to the requirement to generate large amounts of rule templates.

A key insight into this work is the combined use of annotated logic and binarized neural networks to avoid rule template generation. The idea is that instead of generating a combinatorial number of rule templates for a given consequent, we can generate a constant number of rules and use binarized neural learning to prune the elements of the body. Annotated logic, which has a semantics that associated atoms with elements of a lattice structure allows us to have a “don’t care” element for a given atom in the body. With binarized weight learning, we can then use discrete weights to assign the “don’t care” element to weights associated with the atoms we desire to prune from the body. We avoid the vanishing gradient problem that is associated with discrete weight learning by using mature software developed for binarized neural networks [10] that is the result of a line of research on the use of pseudo-gradients for binary weights during gradient descent [13, 14, 15].

Neural answer set programming (NeurASP) [2] does provide strong notions of consistency, but to date has only been used to provide a logical layer on top of a neural network to enforce logical constraints, essentially introducing a capability absent in the other approaches discussed previously. However, this approach does not scale and does not support the learning of new rules. In short, NeurASP satisfies criteria 1-4, but does not meet criteria 5-6 (rule structure learning and scalability).

In what follows, we review generalized annotated programs [9] with some key extensions (the use of a lower semi-lattice for annotations and a semantic structure that maps literals instead of atoms to annotations). We posit that this provides the key to a framework that ensures that all criteria can be adhered to simultaneously.

III Generalized Annotated Programs

We now recapitulate the definition of Generalized Annotated Logic programs (from now on referred to as “GAPs”, for short) from [9], but with limited syntax and certain modifications. There are two reasons why it is advantageous to use GAPs:

It is a framework that easily allows atomic propositions to be associated with values from a lattice structure, which generalizes other real-valued logic paradigms previously introduced in the neuro symbolic reasoning literature [6, 8, 7, 5]. 2. 2.

We can set the annotations based on a lattice structure that can support describing an atomic proposition not only as true, but as false or uncertain (i.e., no knowledge).

Extension: Use of Lower Semi Lattice. In [9], the authors assumed the existence of an upper semi-lattice, $\mathcal{T}$ (not necessarily complete) with ordering $\sqsubseteq$. However, in this work, we propose to instead utilize a lower semi-lattice structure. Therefore, we have a single element $\bot$ and multiple top elements $\top_{0},\ldots\top_{i}\ldots\top_{max}$. The notation $height(\mathcal{T})$ is the maximum number of elements in the lattice in a path between $\bot$ and a top element (including $\bot$ and the top element)111In general, we shall assume that the lattice consists of finite, discrete elements.. Note that we provide rigorous proofs of certain results from [9] on a lower semi-lattice in Section IV.

The employment of a lower semi-lattice structure enables two desirable characteristics. First, we desire to annotate atoms with intervals of reals in $[0,1]$ as done in previous work [6, 16, 17]. Second, it allows for reasoning about such intervals whereby the amount of uncertainty (i.e., for interval $[l,u]$ the quantity $u-l$) decreases monotonically as an operator proceeds up the lattice structure. Therefore, we define the bottom element $\bot=[0,1]$ and a set of top elements $\{[x,x]\;|\;[x,x]\subseteq[0,1]\}$ (see note222N.B. that when using a semi-lattice of bounds, the notation “$\sqsubseteq$” loses its “subset intuition”, as $[0,1]\sqsubseteq[1,1]$ in this case, for example.). Specifically, we set $\top_{0}=[0,0]$ and $\top_{max}=[1,1]$. An example of such a semi-lattice structure is shown in Figure 1.

Syntax of GAPs (Review of prior work). We assume the existence of a set AVar of variable symbols ranging over $\mathcal{T}$ and a set $\mathcal{F}$ of function symbols, each of which has an associated arity. We start by defining annotations.

Definition III.1** (Annotation).**

*(i) Any member of $\mathcal{T}\,\cup\textsf{AVar}$ is an annotation.

(ii) If $f$ is an $n$-ary function symbol over $\mathcal{T}$ and $t_{1},\ldots,t_{n}$ are annotations, then $f(t_{1},\ldots,t_{n})$ is an annotation.*

One specific function we define is “$\neg$”, which is used in semantics of [9]. For a given $[l,u]$, $\neg([l,u])=[1-u,1-l]$. Note that we also use the symbol $\neg$ in our first-order language (following the formalism of [9]).

We define a separate logical language whose constants are members of set $\mathcal{C}$ and whose predicate symbols are specified by set $\mathcal{P}$. We also assume the existence of a set $\mathcal{V}$ of variable symbols ranging over the constants, that no function symbols are present, and terms and atoms are defined in the usual way (cf. [18]). We shall assume that $\mathcal{C},\mathcal{P},\mathcal{V}$ are discrete and finite. In general, we shall use capital letters for variable symbols and lowercase letters for constants. Similar to previous work [5, 3], we assume that all elements of $\mathcal{P}$ have an arity of either 1 or 2—we use $\mathcal{P}_{una}$ to denote the set of unary predicates and $\mathcal{P}_{rel}$ the set of binary predicates. We shall also denote a subsets of $\mathcal{P}$ to include “target predicates” written $\mathcal{P}_{tgt}$ that can consist of either binary or unary predicates ($\mathcal{P}_{tgt\_rel},\mathcal{P}_{tgt\_una}$) provided that they are not reserved words. We shall use the symbol $\mathcal{L}$ to denote the set of all ground literals and $\mathcal{A}$ for the set of all ground atoms. We now define the syntactical structure of GAPs that will be used in this work.

Definition III.2** (Annotated atoms, negations, literals).**

The core syntactic structures are defined as follows:

• •

Annotated atom.* If $\mathbf{a}$ is an atom and $\mathbf{\mu}$ is an annotation, then $\mathbf{a:\mu}$ is an annotated atom.*

• •

Annotated Negation.* If $\mathbf{a}$ is an atom and $\mathbf{\mu}$ is an annotation, then $\mathbf{\neg a:\mu}$ is an annotated negation.*

• •

Annotated Literal.* Collectively, atoms and negations are referred to as annotated literals.*

Definition III.3** (GAP Rule).**

If $\ell_{0}:\mu_{0},\ell_{1}:\mu_{1},\ldots,\ell_{m}:\mu_{m}$ are annotated literals (such that for all $i,j\in 1,m$, $\ell_{i}\not\equiv\ell_{j}$), then

[TABLE]

is called a GAP rule. We will use the notation $head(r)$ and $body(r)$ to denote $\ell_{0}$ and $\{\ell_{1},\ldots,\ell_{m}\}$ respectively. When $m=0$ ($body(r)=\emptyset$), the above GAP-rule is called a fact. A GAP-rule is ground iff there are no occurrences of variables from either AVar or $\mathcal{V}$ in it. For ground rule $r$ and ground literal $\ell$, $bodyAnno(\ell,r)=\mu$ such that $\ell:\mu$ appears in the body of $r$. A generalized annotated program $\Pi$ is a finite set of GAP rules.

Semantics of GAPs (Extended in this work). The formal semantics of GAPs are defined as follows. Note that we extend the notion of an interpretation to allow for a mapping of literals to annotations (as opposed to atoms). However, we add a requirement on the annotation between each atom and negation that ensures equivalence to the semantic structure of [9]. The intuition behind this extension is that we can more easily detect inconsistencies using the fixpoint operator, as we can just compare the annotations of each pair of literals (the atom and its negation).

Definition III.4** (Interpretation).**

An interpretation $I$ is any mapping from the set of all grounds literals to $\mathcal{T}$ such that for literals $a,\neg a$, we have $I(a)=\neg(I(\neg a))$. The set $\mathcal{I}$ of all interpretations can be partially ordered via the ordering: $I_{1}\preceq I_{2}$ iff for all ground literals $a$, $I_{1}(\ell)\sqsubseteq I_{2}(\ell)$. $\mathcal{I}$ forms a complete lattice under the $\preceq$ ordering.

Satisfaction Relationship (Review of prior work). We now present the concept of satisfaction:

Definition III.5** (Satisfaction).**

An interpretation $I$ satisfies a ground literal $\ell:\mu$, denoted $I\models\ell:\mu$, iff $\mu\sqsubseteq I(\ell)$. $I$ satisfies the ground GAP-rule

[TABLE]

(denoted $I\models\ell_{0}:\mu_{0}\leftarrow\ell_{1}:\mu_{1}\,\,\wedge\,\ldots\,\wedge\,\ell_{m}:\mu_{m}$) iff either

$I$* satisfies $\ell_{0}:\mu_{0}$ or* 2. 2.

There exists an $1\leq i\leq m$ such that $I$ does not satisfy $\ell_{i}:\mu_{i}$.

$I$* satisfies a non-ground literal or rule iff $I$ satisfies all ground instances of it.*

We say that an interpretation $I$ is a model of program $\Pi$ if it satisfies all rules in $\Pi$. Likewise, program $\Pi$ is consistent if there exists some $I$ that is a model of $\Pi$. We say $\Pi$ entails $\ell:\mu$, denoted $\Pi\models_{\mathit{ent}}\ell:\mu$, iff for every interpretation $I$ s.t. $I\models\Pi$, we have that $I\models\ell:\mu$. As shown by [9], we can associate a fixpoint operator with any GAP $\Pi$ that maps interpretations to interpretations.

Definition III.6**.**

Suppose $\Pi$ is any GAP and $I$ an interpretation. The mapping ${\mathbf{T}}_{\Pi}$ that maps interpretations to interpretations is defined as

[TABLE]

where $annoSet_{\Pi,I}(\ell_{0})=\{I(\ell_{0})\}\cup\{\mu_{0}\>\;|\;\>\ell_{0}:\mu_{0}\leftarrow\ell_{1}:\mu_{1}\,\wedge\ldots\wedge\,\ell_{m}:\mu_{m}\textit{ is a ground instance}$ $\textit{of a rule in }\Pi,\textit{ and for all }1\leq i\leq m,\textit{we have }I\models\ell_{i}:\mu_{i}\}$.

The key result of [9] (Theorem 2 in that paper, discussed in the next section) tells us that $\mathit{lfp}({\mathbf{T}}_{\Pi})$ precisely captures the ground atomic logical consequences of $\Pi$. We show this is also true (under the condition that $\Pi$ is consistent) even if the annotations are based on a lower lattice (see Theorem IV.2). In [9], the authors also define the iteration of ${\mathbf{T}}_{\Pi}$ as follows:

• •

${\mathbf{T}}_{\Pi}\uparrow 0$ is the interpretation that assigns $\bot$ to all ground literals.

• •

${\mathbf{T}}_{\Pi}\uparrow(i+1)={\mathbf{T}}_{\Pi}({\mathbf{T}}_{\Pi}\uparrow i)$.

For each ground $\ell\in\mathcal{L}$, the set $\Pi(\ell)$ is the subset of ground rules (to include facts) in $\Pi$ where $\ell$ is in the head. We will use the notation $m_{\ell}$ to denote the number of rules in $\Pi(\ell)$. For a given ground rule, we will use the symbol $r_{\ell,i}$ to denote that it is the $i$-th rule with atom $\ell$ in the head.

IV New Theoretical Results for Annotated Logic on a Lower Semi-lattice

The use of the lower semi-lattice structure for annotations in GAPs leads us to revisit some of the results of [9] that depend upon an upper semi-lattice structure. In this section, we shall review results from [9] that apply to an upper semi-lattice (and shall refer to results specific to the upper semi-lattice as “UGAPs”) and also prove analogous results for GAPs where the annotation uses a lower semi-lattice (“LGAPs”). Further, note that in UGAPs we shall refer to interpretations defined only as mappings of atoms to annotations. This makes it relatively straightforward to have consistency; consider the following proposition.

Proposition IV.1**.**

Any UGAP $\Pi$ consisting of UGAP-rules where the atom bodies and heads are atoms is consistent.

Proof.

Consider the interpretation $I$ such that $\forall a\in\mathcal{A}$, $I(a)=\top$. By the semantics of GAPs, this will satisfy all rules. ∎

To provide a specific example of an LGAP that is not consistent, consider the following two rules (here $a$ is a ground literal):

[TABLE]

So, we consider the key result of [9] below.

Theorem IV.1**.**

(Theorem 2 in [9]) For UGAP $\Pi$, ${\mathbf{T}}_{\Pi}$ is monotonic and has a least fixpoint $\mathit{lfp}({\mathbf{T}}_{\Pi})$. Moreover, for this case $\Pi$ entails $a:\mu$ iff $\mu\sqsubseteq\mathit{lfp}({\mathbf{T}}_{\Pi})(a)$.

However, under the condition that $\Pi$ is consistent, we can show a similar result.

Theorem IV.2**.**

If LGAP $\Pi$ is consistent, then:

${\mathbf{T}}_{\Pi}$* is monotonic,* 2. 2.

${\mathbf{T}}_{\Pi}$* has a least fixpoint $\mathit{lfp}({\mathbf{T}}_{\Pi})$, and* 3. 3.

$\Pi$* entails $a:\mu$ iff $\mu\leq\mathit{lfp}({\mathbf{T}}_{\Pi})(a)$.*

Proof.

(1 and 2) By creating an interpretation that maps literals to annotations, instead of atoms, the monotonicity of ${\mathbf{T}}_{\Pi}$ is trivial even in the case where $\Pi$ in inconsistent and has a least fixed point.

(3) Suppose, BWOC that $\Pi$ entails $a:\mu$ and $\mu>\mathit{lfp}({\mathbf{T}}_{\Pi})(a)$. However, this would imply there is a series of logical constructs that allow us to derive $a:\mu$, and this would trivially be reflected in the iterative applications of the ${\mathbf{T}}$ operator. Going the other way, BWOC if $\mu\leq\mathit{lfp}({\mathbf{T}}_{\Pi})(a)$ but $\Pi$ does not entail $a:\mu$ would imply that there is no application of the constructs in $\Pi$ that lead to the deductive conclusion of $a:\mu$; however this is again contradicted by the fact that ${\mathbf{T}}$ directly leverages the elements of $\Pi$. ∎

We can also show that for both LGAPs and UGAPs, we can bound the number of applications of ${\mathbf{T}}$ until convergence.

Theorem IV.3**.**

If (LGAP or UGAP) $\Pi$ is consistent, then $\mathit{lfp}({\mathbf{T}}_{\Pi})\equiv{\mathbf{T}}_{\Pi}\uparrow x$ where $x=height(\mathcal{T})*|\mathcal{L}|$.

Proof.

We know, by the definition of ${\mathbf{T}}$, for any $i\leq x$, that for all $a\in\mathcal{A}$, ${\mathbf{T}}_{\Pi}\uparrow i(a)\sqsubseteq{\mathbf{T}}_{\Pi}\uparrow x(a)$. Hence, we just need to consider the case where $i>x$ and $\mathit{lfp}({\mathbf{T}}_{\Pi})\equiv{\mathbf{T}}_{\Pi}\uparrow i$ and $\mathit{lfp}({\mathbf{T}}_{\Pi})\not\equiv{\mathbf{T}}_{\Pi}\uparrow x$. However, at each iteration the annotation of at least one atom must change. The bound on the number of changes in annotation is $height(\mathcal{T})$ (as the annotations must stay the same or increase monotonically, as $\Pi$ is consistent by the statement). Hence, we have a contradiction. ∎

We can also leverage the ${\mathbf{T}}$ operator to identify inconsistencies.

Theorem IV.4**.**

(LGAP or UGAP) $\Pi$ is inconsistent if and only if for value $i$, and ground atom $a$, if there exist $\mu,\mu^{\prime}\in annoSet_{\Pi,{\mathbf{T}}_{\Pi}\uparrow i}(a)$ where $\mu\not\sqsubseteq\mu^{\prime}$ and $\mu^{\prime}\not\sqsubseteq\mu$.

Proof.

Claim 1: If there exist $i,a$ such that the statement holds, then $\Pi$ is inconsistent. Suppose, BWOC, that such an $i,a$ pair exist and $\Pi$ is consistent. We know, by the definition of ${\mathbf{T}}$ that ${\mathbf{T}}({\mathbf{T}}\uparrow i)$ must be an interpretation. However, as there is no element above both $\mu,\mu^{\prime}$, ${\mathbf{T}}$ that ${\mathbf{T}}({\mathbf{T}}\uparrow i)$ cannot be a valid interpretation.

Claim 2: If $\Pi$ is inconsistent, then there exist $i,a$ such that the statement holds. Suppose, BWOC, $\Pi$ is inconsistent and there does not exist such an $i,a$ pair. Then, this implies that for all $a\in\mathcal{A}$ that there exists some $i^{\prime}$ where ${\mathbf{T}}({\mathbf{T}}\uparrow i^{\prime})={\mathbf{T}}\uparrow i^{\prime}$ which means for any $i^{\prime\prime}>i^{\prime}$ we have ${\mathbf{T}}\uparrow i^{\prime}={\mathbf{T}}\uparrow i^{\prime\prime}$. Therefore, by the definition of satisfaction, ${\mathbf{T}}\uparrow i^{\prime}$ must satisfy $\Pi$, which is a contradiction. ∎

V Parametrized GAP Rules

In this section, we present a rule structure and annotation function (that later is also used as an activation function in the associated neural architecture) that can allow for us to learn GAP rules from data by using a process like gradient descent. One of the key intuitions behind the use of a lower semi-lattice for annotations is that we can easily separate the concepts of negation and “no information.” Hence, in the classical case, the lattice structure would consist of three elements: a lower “uncertain” element and two upper elements, one for false and one for true (see Figure 2). Through the use of a semantic structure that assigns literals to annotations, we can restrict our rules to activation functions that only modify the lower bound (i.e., if we wish to adjust the upper bound on a literal, we can instead have a rule that adjusts the lower bound on its negation). Also note the use of the interval of $[-1,1]$ as opposed to $[0,1]$—this is due to the common values used for binarized neural networks [10] that we will use to prune unneeded atoms from the body.

Rule Structure. In this paper, we shall consider the propositional case (this is the case where all predicates are unary and we have a single constant). Hence, there is no grounding (see Section IX for discussions on grounding). So, for a given literal $a$ in the rule head and for a potential set of literals $\mathcal{L}^{\prime}$ in the body, we have the following rule $r$:

[TABLE]

In rule 1, we have rule $r$ that has literal $a$ in the head that is assigned a lower bound on the lattice element based on function $f_{a}^{(i)}$, which utilizes learned parameters $\theta_{a}^{i}$. Several observations: first, note the $i$ index is used in the case where multiple rules are used with literal $a$ in the head. Next, $X_{a}^{(i)}$ is the vector of the lower bound of the annotations of each literal in the body ($x_{j}$ is the $j$th component of $X_{a}^{(i)}$). Finally, also note that $x_{j}^{\prime}$ is unused by the annotation function for this particular rule (again, if we desire to use the upper bound, we can instead include the negation of literal $\ell_{j}$ in the set $\mathcal{L}^{\prime}$ and use its upper bound).

Annotation/Activation Functions. In defining the annotation function $f_{a,\theta_{a}^{i}}^{(i)}$, it must have the capability to use parameters to “turn off” a given literal in the body. We note that real-valued weights in traditional neural networks as well as the prior work described earlier cannot accomplish this task, hence the extensive use of fuzzy logic in other neural symbolic approaches. We seek to employ binarized neural networks [10] in which both weights and activations have values in the set $\{-1,1\}$. The work of [10] has led to successful use of a “gradient descent” style approach to discrete optimization for model training. This avoids the well-known problem of vanishing gradients by substituting the partial derivative for a “pseudo gradient” of the activation function. There are current implementations for binarized neural networks such as Larq333See https://docs.larq.dev/larq/ that have successfully employed this methodology.

For our purposes, the annotation function shall also be used as an activation function in the equivalent neural architecture. First, we present the meaning of the parameters. Let $\theta_{a,j}^{i}$ be the $j$th component of $\theta_{a}^{i}$. If this value is $1$, that means that literal $\ell_{j}$ should be considered in the body of the rule—likewise, if it is $-1$, then it should not. Hence, after training, we should be able to simply erase any $\ell_{j}$ where $\theta_{a,j}^{i}=-1$ to no effect. Second, we must consider the meaning of the activations. For $f_{a,\theta_{a}^{i}}^{(i)}$ to return $1$, then for every $\theta_{a,j}^{i}=1$, $x_{j}$ must also equal $1$. If there is any $j$ where $\theta_{a,j}^{i}=1$ and $x_{j}=-1$, then $f_{a,\theta_{a}^{i}}^{(i)}$ must return $-1$. The following $\mathit{relu}$ function accomplishes this requirement (note there are available pseudo gradients for binarized neural networks for $\mathit{relu}$).

We must therefore consider the meaning of the lower bound of the annotation assigned by function $f_{a,\theta_{a}^{i}}^{(i)}$. In the below function, $Sign$ assigns values greater than [math] to $1$, and $-1$ otherwise (as per [10]).

[TABLE]

So, consider that $\theta_{a,j}^{i}=-1$ does not affect the sum with respect to literal $\ell_{j}$. The same is true for any $x_{j}=1$. Therefore, if for all $j$ such that $\theta_{a,j}^{i}=1$ and $x_{j}=1$ then the function returns a $1$. Now, if for a single $\ell_{j}$ we have $\theta_{a,j}^{i}=1$ and $x_{j}=-1$, then the function returns $-1$.

We point out that the number of rules used for a given ground atom can be considered as a hyper-parameter. Unlike in [5, 4], where the parameters turn entire rules on or off, in this approach we are turning on or off atoms in the body. This avoids the need to generate large numbers of rule templates. However, it does rely on domain knowledge (e.g., in the form of a knowledge graph) to limit the number of literals considered in a given rule (in other words, we want to keep set $\mathcal{L}^{\prime}$ small).

VI Neural Architecture for Learning GAPs

In this section, we look at how a GAP can be embedded in a neural framework for use in training by gradient descent. The concept is similar to that of the differentiable inductive logic programming (ILP) literature [4, 5] in that it involves an unrolling of the fixed point operator. However, we use the rule structure and annotation/activation function of the previous section to avoid generating numerous rule templates.

We shall assume a RNN neural architecture consisting of $K$ recurrent cells. In order to assure correctness, $K$ must be set to the maximum number of applications of the fixpoint operator (see Theorem IV.3). We use $A$ to denote a vector of elements in $\mathcal{F}$ of size $n$—intuitively, we want each position of $A$ to correspond to the annotation of a single literal in $\mathcal{L}$. So, we shall assume a numbering of literals such that literal $a_{j}\in\mathcal{A}$ would correspond with the $j$-th position of $A$. The initial input to the first recurrent cell will be denoted $A_{0}$, where all positions are set to $\bot$. For recurrent cell $t$, $A_{t-1}$ is the input and $A_{t}$ is the output.

For each rule $r_{a_{j},i}$ there is an associated vector of body annotation lower bounds $X_{a_{j}}^{(i)}$ of size ${n_{a_{j},i}}\leq n$; this is of a smaller size than $A_{t}$ as a body of a given rule may not include all atoms. However, for a given annotation function $f_{a}^{(i)}$ in the head of a rule, when we say it evaluates an $n$-sized vector $A_{t}$, it is actually evaluating the positions in $A_{t}$ corresponding to the atoms for which there are positions in $X_{a_{j}}^{(i)}$.

In each recurrent cell $t$, vector $\tilde{A}_{t}^{(j)}$ is created and is of length $m_{a_{j}}$ (the number of rules, including facts, with atom $a_{j}$ in the head). Position $i$ of $\tilde{A}_{t}^{(j)}$ is equal to $f_{a_{j}}^{(i)}(\theta_{a_{j}}^{(i)},A_{t-1})$. For facts, this position will simply be the annotation in the head of the fact.

Finally, the result of recurrent cell $t$ is vector $A_{t}$ in which the $j$-th position of this vector corresponds with the supremum of the corresponding $\tilde{A}_{t}^{(j)}$. Note that as this is a supremum of annotations in which only the lower bound changes, this is equivalent to a max pooling layer that only applies the pooling function to a subset of neurons. The intuition is that each cell corresponds with one application of the ${\mathbf{T}}$ operator. Figure 3 shows a depiction of this architecture.

VII Identifying Inconsistencies

The use of the lower lattice for annotations does not allow for easy guarantees of consistency (i.e., see Proposition IV.1). While it is possible to guarantee consistency by determining rules with restrictive structures (e.g., disallowing negation in learned rules as in [5]), this becomes difficult if rules are created as a result of the training process (e.g., setting parameters that configure the rules through gradient descent).

Other approaches to dealing with consistency in the settings integrating symbolic and machine learning paradigms have included notions of quantifying a level of inconsistency and then attempting to minimize such inconsistency. This is commonly used in the (non-neural) probabilistic soft logic (PSL) [11]. This concept has also appeared in neuro symbolic approaches as well [6].

However, an advantage with the approach of this paper is that an inconsistency will be detected by some application of the fixpoint operator (Theorem IV.4). This is why we changed the domain of an interpretation to be literals instead of atoms, as we can more easily identify a case where an atom and its negation are assigned annotations in such a way to cause an inconsistency. We create a special atomic symbol $\mathit{incon}$ for this purpose. The negation of this symbol is never used; however, if this symbol is annotated with $[1,1]$ (“true”) then it means we have an inconsistency. In the logic program, we add a single rule of the form 3 below, and for each ground atom $a$ we add an instance of rule 4:

[TABLE]

Hence, for any application of the fixpoint operator, we know there is an inconsistency if $\mathit{incon}$ is true and we need not carry out further applications of the operator. Our intuition is that this can be used during the training process to either establish a loss function that disallows any inconsistency, or to conduct a check at each iteration of gradient descent. It is noteworthy that the fixpoint operator, which also is likely to bring further efficiencies to the training process, can be used in the forward pass as opposed to the equivalent neural architecture. Further, the fixpoint operator will also provide information on where the inconsistency occurs, which can also be useful in guiding the training process. Note that some domains may accept inconsistency if it is localized and not associated with certain hard constraints (e.g., specified by rules with no parameters, which this framework also supports).

VIII How the Framework Meets the Criteria

We now briefly review the criteria introduced in Section II and discuss how the proposed approach can meet them:

• •

As it is an inherently neuro symbolic approach, it meets criterion 1.

• •

Due to the direct mapping to an equivalent neural architecture, which is similar to LNN [6], it meets criterion 2 in that the results are directly explainable, symbolic, and amenable to further analysis.

• •

The framework can both allow parametrized rules (for induction) as well as directly represent logical statements in the equivalent neural architecture, which satisfies criterion 3—incorporation of prior knowledge—(as does [7, 3, 6]).

• •

We can provably show it can guarantee consistency, even when using negation, meeting criterion 4 (as does [2]).

• •

Through the use of parametrized rules, annotated logic, and binarized neural networks, it enables rule learning (criteria 5).

• •

Unlike [5], it avoids (non-scalable) template generation, instead building up antecedents by using the lattice structure to “turn off” certain atoms (meeting criterion 6).

Though, as we have argued, our proposed formalism meets all six criteria, there remain several hurdles to overcome, which we discuss in the following section.

IX Challenges and Conclusion

While the use of annotated logic in a neural symbolic framework is promising, there are several challenges to be addressed. First, it is expected that any neuro symbolic approach should support first order logic (i.e., the non-ground case). While there is nothing presented here that would not support such a capability, practical considerations around grounding can limit scalability in practice. We are exploring the use of knowledge graphs [19] as an ontology to limit relationships among constants to reduce the grounding problem. A second, but equally important, concern is dealing with inconsistency. It is challenging to specifically avoid inconsistency and ensure that the training process continues. Ultimately, this will require a determination of best practices around gradient descent and a vigilant measure of the boundaries of inconsistency. Third, and in the same vain, we also will need to explore other issues such as establishing best practices for connecting a neural network associated with a logic program with lower-level neural networks used for perception (e.g., CNN’s). Finally, implementation issues will clearly be very important in successfully developing tools based on this framework.

Acknowledgment

P.S. is supported by internal funding from the ASU Fulton Schools of Engineering. G.S. is supported by Universidad Nacional del Sur (UNS) under grant PGI 24/ZN34 and Agencia Nacional de Promoción Científica y Tecnológica under grant PICT-2018-0475 (PRH-2014-0007).