Towards Rigorous Understanding of Neural Networks via
  Semantics-preserving Transformations
In this paper we present an algebraic approach to the precise and global
verification and explanation of Rectifier Neural Networks, a subclass of
Piece-wise Linear Neural Networks (PLNNs), i.e., networks that semantically
represent piece-wise affine functions. Key to our approach is the symbolic
execution of these networks that allows the construction of semantically
equivalent Typed Affine Decision Structures (TADS). Due to their deterministic
and sequential nature, TADS can, similarly to decision trees, be considered as
white-box models and therefore as precise solutions to the model and outcome
explanation problem. TADS are linear algebras which allows one to elegantly
compare Rectifier Networks for equivalence or similarity, both with precise
diagnostic information in case of failure, and to characterize their
classification potential by precisely characterizing the set of inputs that are
specifically classified or the set of inputs where two network-based
classifiers differ. All phenomena are illustrated along a detailed discussion
of a minimal, illustrative example: the continuous XOR function.
Maximilian Schlüter, Gerrit Nolte, Alnis Murtovi, Bernhard Steffen
# Towards Rigorous Understanding of Neural Networks via Semantics-preserving Transformations

###### Abstract

In this paper we present an algebraic approach to the precise and global verification and explanation of _Rectifier Neural Networks_, a subclass of _Piece-wise Linear Neural Networks_ (PLNNs), i.e., networks that semantically represent piece-wise affine functions. Key to our approach is the symbolic execution of these networks that allows the construction of semantically equivalent _Typed Affine Decision Structures_ (TADS). Due to their deterministic and sequential nature, TADS can, similarly to decision trees, be considered as white-box models and therefore as precise solutions to the model and outcome explanation problem. TADS are linear algebras which allows one to elegantly compare Rectifier Networks for equivalence or similarity, both with precise diagnostic information in case of failure, and to characterize their classification potential by precisely characterizing the set of inputs that are specifically classified or the set of inputs where two network-based classifiers differ. All phenomena are illustrated along a detailed discussion of a minimal, illustrative example: the continuous XOR function.

## 1 Introduction

Neural networks are perhaps today's most important machine learning models, with exciting results, e.g., in image recognition [10], speech recognition [12, 13] and even in highly complex games [14, 15, 16]. As the name suggests, neural networks are learned from data using efficient, but approximative training algorithms [13, 1]. At their core, neural networks are (dataflow-oriented) computation graphs [1]. They consist of many computation units, called _neurons_, that are arranged in layers such that computations in each layer can be performed in parallel, with successive layers only depending on the preceding layer. Modern neural networks, in practice, possess up to multiple billions of parameters [13] and leverage parallel hardware such as GPUs to perform computations of this scale [1]. This highly quantitative approach is responsible for exciting success stories, but also for their main weakness: Neural network behavior is often chaotic and hard to comprehend for a human. Perhaps most infamously, a neural network's prediction can change drastically under imperceptible changes to its input, so-called _adversarial examples_[1, 14, 15].

The explainability of neural networks, which are computationally considered as black-boxes due to their highly parallel and non-linear nature, is therefore one of the current core challenges in AI research [15]. The fact that neural networks are increasingly used in safety-critical systems such as self-driving cars [1] turns trustworthiness of machine learning into a must [15]. However, state-of-the-art explanation technology is more about reassuring intuition, e.g., to support cooperative work of humans with AI systems, such as in the field of medical diagnostics [16], than about precise explanation or guarantees [17]. Moreover, current approaches to Neural Network verification are still in their infancy in that they are not yet sufficiently tailored to the nature of Neural Networks to achieve the required scalability or to provide diagnostic information beyond individual witness traces in cases where the verification attempts fail (cf. [1, 18, 19] and Section8 for a more detailed discussion).

In this paper, we present an algebraic approach to the verification and explanation of Rectifier Neural Networks (PLNN), a very popular subclass of neural networks that semantically represent piece-wise affine functions (PAF) [20]. Key to our approach are _Typed Affine Decision Structures_ (TADS) that concisely represent PAF in a white-box fashion that is as accessible to human understanding as decision trees. TADS can nicely be derived from PLNNs via symbolic execu
tion [14, 15], or, alternatively, compositionally along the PLNN's layering structure, and their algebraic structure allows for elegant solutions to verification and explanation tasks:

* TADS can be used for PLNNs similarly as _Algebraic Decision Diagrams_ (ADDs) have been used for Random Forests in [13] to elegantly provide model and outcome explanations as well as class characterizations.
* Using the algebraic operations of TADS one can not only decide the equivalence problem, i.e., whether two PLNNs are semantically equivalent, but also whether they are \(\epsilon\)-similar, i.e, never differ more than \(\epsilon\). In both cases, diagnostic information in terms of a corresponding 'difference' TADS is provided that precisely specifies where one of these properties is violated.
* TADS comprise non-continuous piece-wise linear operations which cannot be represented by PLNNs. This is necessary to not only deal with _regression tasks_, where one aims at approximating continuous functions, but also with _classification tasks_ with discrete output domains.1 In the latter case, TADS-based class characterization allows one to precisely characterize the set of inputs that are classified as members of a given class, or the set of inputs where two (PLNN-based) classifiers differ. Footnote 1: As PLNNs always represent continuous functions, an additional outcome interpretation mechanism is needed to bridge the gap from continuous networks to discrete classification tasks.
* Finally, TADS can also profitably be used for the verification of preconditions and postconditions, the illustration of which is beyond the scope of this paper but will be discussed in [12] in the setting of digit recognition.

The paper illustrates the essential features of TADS using a minimal, illustrative example: the continuous XOR function. The simplicity of XOR is ideally suited to provide an intuitive entry into the presented theory. A more comprehensive example is presented in [12], where digit recognition based on the MNIST data base is considered. In this highly dimensional setting, specific scalability measures are required to apply our TADS technology.

After specifying the details of our running example in Section2, Section3 sketches Algebraic Decision Structures that later on will be instantiated with Affine Functions recalled in Section4 to introduce the central notion of this paper, Typed Affine Decision Structures (TADS). Semantically, TADS represent piece-wise affine functions which mark them as a fitting representation for Rectifier Networks that represent continuous piece-wise affine functions2 and that are discussed in Section5. Our main contribution is the derivation of TADS, using both symbolic execution and compositionality along the layering structure of PLNN, as a complete and precise model explanation of PLNNs. We introduce TADS in Section6 and state important algebraic properties that allow the manipulations mentioned beforehand. Subsequently, Section7 illustrates the impact on verification and explanation of the algebraic properties of TADS that are also established in Section6 along the running example. The paper closes after a discussion of related work in Section8 with conclusions and direction to future work in Section9.

Footnote 2: Rectifier Networks are often also called Piece-wise Linear Neural Networks, the reason for us to denote them as PLNNs.

## 2 Running Example - XOR

As a running example throughout this paper, we discuss the XOR function under the perspective of a regression task and a classification task as specified below. We chose the XOR problem for illustration for two reasons:

* The XOR problem concerns a two-dimensional function which can be visualized as a function plot.
* While simple, the XOR problem has been a roadblock in early AI research due to it not being solvable by linear approaches [16]. Therefore, it

Figure 1: A baseline solution to the XOR-regression problem given by \(f_{*}(x,y)=|x-y|\). Note that this function is piece-wise linear, having two separate linear regions, which is minimal for the problem.
is a minimal problem that still _requires_ a more powerful, non-linear model such as a PLNN.

For the following formalizations, let us fix some basic notation: The set of natural numbers (including zero) is denoted \(\mathbb{N}\) and the set of real numbers \(\mathbb{R}\). Unions and intersections of sets are defined as usual. The cartesian product of two sets is defined as

\[M\times N:=\{\,(x,y)\,|\,x\in M\,\wedge\,y\in N\,\}.\]

A sequence of cartesian products over the same set may be abbreviated as \(M^{n}\) (\(n\geq 0\)) where

\[M^{0}=\emptyset\qquad M^{1}=M\qquad M^{n+2}=M\times M^{n+1}\]

and the Kleene star operator is defined as

\[M^{*}:=\bigcup_{n\in\mathbb{N}}M^{n}\]

Moreover, intervals of \(\mathbb{R}\) are of the form \([a,b]\) for \(a,b\in\mathbb{R}\) with \(a\leq b\) and denote the set of all real values between \(a\) and \(b\).

As a _regression_ task, the XOR problem is stated as follows:

**2.1 Definition** (XOR Regression).: Find a piecewise affine function \(f\colon[0,1]^{2}\to[0,1]\) that is continuous and satisfies:

\[f(0,0)\approx 0\approx f(1,1)\quad\text{and}\quad f(1,0)\approx 1\approx f(0,1)\]

Thus, a learning algorithm is tasked with approximating a continuous version of an XOR gate, interpolating between the four edge points for which the XOR function is defined.3

Footnote 3: The restriction to the interval \([0,1]\) is meant to ease the exposition.

When posing the XOR problem as a classification task, the XOR function can be regarded as a function with _discrete_ binary output 1 or 0 but with a continuous domain \(\mathbb{R}^{2}\).

**2.2 Definition** (XOR Classification).: Find a piece-wise affine function \(f\colon[0,1]^{2}\to\{0,1\}\) such that:

\[f(0,0)=0=f(1,1)\quad\text{and}\quad f(1,0)=1=f(0,1)\]

As the XOR-problem requires fixed values only at four points, there exist infinitely many solutions. This is typical for machine learning problems where only some few points are fixed and others are left for the machine learning model to freely interpolate. Different machine learning models have different principles that dictate this interpolation. For example, concerning PLNNs the interpolation is (piece-wise) linear.

In line with the principle of Occam's razor [20], humans4 would optimally solve the XOR-regression problem with a function as simple as:

Footnote 4: In contrast to, e.g., solutions learned by machines.

\[f_{*}(x,y)=|x-y|\]

A visualisation of \(f_{*}\) can be found in Figure 1. Similarly, a human would probably choose the following corresponding straightforward extension to the classification problem:

\[g_{*}(x,y)=\begin{cases}1&\text{if }f_{*}(x,y)\geq 0.5\\ 0&\text{otherwise}\end{cases}\]

An illustration of \(g_{*}\) can be found in Figure 2. It is straightforward to check that these functions solve the XOR-regression and XOR-classification problems optimally in the sense that they match the traditional XOR function on all points where it is defined.

The continuous XOR problems will serve as running examples throughout this work: We will demonstrate different representations of piece-wise linear functions (such as \(f_{*}\)) and transformations between them along the development of our theory, and showcase differences between the manually constructed solutions to the regression and classification tasks and their learned counterparts in Section 7.

## 3 Algebraic Decision Structures

In order to prepare the algebraic treatment of decision structures, we focus on decision structures whose leafs

Figure 2: A baseline solution to the XOR-classification problem given by \(g_{*}(x,y)=1\) iff \(f_{*}(x,y)\geq 0.5\).
are labeled with the elements of an algebra \(A=(\mathcal{A},O)\), so-called _Algebraic Decision Structures_ (ADDs). This subsumes the classical case where leafs of decision structures are elements of a set, as these are simply algebras where \(O\) is empty. In this section we summarize the definitions and theorems of [10] which are required later in this paper.5

Footnote 5: Some definitions and theorems were slightly improved or adjusted from [10] for better alignment with the rest of this paper. We omit the proofs for the adjustments because they are straightforward.

### Definition (Algebraic Structures)

An _algebraic structure_, or _algebra_ for short, is a pair \((\mathcal{A},O)\) of a carrier set \(\mathcal{A}\) and a set of operations \(O\). Operations \(\mathit{op}\in O\) have a fixed arity and are closed under \(\mathcal{A}\).

In the following the algebra is identified with its carrier set and both are written calligraphically.

### Definition (Algebraic Decision Tree)

An

Algebraic Decision Tree (ADT) over the algebra \(A\) and the predicates \(\mathcal{P}^{\mathcal{G}}\) is inductively defined by the following BNF:

\[T\ \mathop{\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,
**3.8 Definition (Vacuity)**.: Let \(\bar{\mathcal{P}}\) be the set of negated predicates of \(\mathcal{P}\). Then we call \(\pi=p_{0}\cdots p_{m}\in(\bar{\mathcal{P}}\cup\bar{\mathcal{P}})^{*}\) a predicate path.

* \(\pi\) is called a predicate path of a decision structure \(t\in\mathcal{S}_{A}\) iff there exists a path \(\pi^{\prime}=p_{0}^{\prime}\cdots p_{m}^{\prime}\in\mathcal{P}^{*}\) from the root of \(t\) to one of its other nodes such that \(p_{i}=p_{i}^{\prime}\) in case that \(\pi^{\prime}\) follows the left/true branch at \(p_{i}\) in \(t\) and \(p_{i}=\vec{p}_{i}^{\prime}\) otherwise. We denote the last predicate \(p_{m}\in\mathcal{P}\cup\bar{\mathcal{P}}\) of \(\pi\) by \(\mathit{final}(\pi)\).
* Given a predicate path \(\pi=p_{0}\cdots p_{m}\) the predicate \(\mathit{final}(\pi)\) is called _vacuous_ for \(\pi\) iff the conjunction of the preceding predicates \(p_{0}\wedge\cdots\wedge p_{m-1}\) in \(\pi\) implies \(\mathit{final}(\pi)\).
* Let \(\Pi_{n}\) be the set of predicate paths of \(t\in\mathcal{S}_{A}\) that end in a given node \(n\). We call \(n\) vacuous in \(t\), iff \(\mathit{final}(\pi)\) is vacuous for all paths \(\pi\in\Pi\) and \(\mathit{final}(\pi)\) coincides for all \(\pi\).
* A decision structure \(t\in\mathcal{S}_{A}\) is called _vacuity-free_ iff there exists no vacuous node.

This allows us to define the following optimization step.

**3.9 Definition (Vacuity Reduction)**.: Let \(t\in\mathcal{S}_{A}\) be a decision structure with a vacuous node \(n\) and \(\mathit{final}(\pi)\in\mathcal{P}\cup\bar{\mathcal{P}}\) be the last predicate of some predicate path \(\pi\) ending in \(n\). Then, re-routing all incoming edges of \(n\) to the 'true'-successor of \(n\) in case of \(\mathit{final}(\pi)\in\mathcal{P}\) and to the 'false'-successor otherwise is called a _vacuity reduction_ step.

ADSs, being DAGs, only have finitely many predicate paths which can be effectively analysed for vacuous predicates as long as the individual predicates are decidable. As the elimination of vacuous predicates is a simple semantics-preserving transformation we have:

**3.10 Theorem (Minimality)**.: _Every ADS can be effectively transformed into a semantically equivalent, vacuity-free ADS that is minimal in the sense that any further reduction would change its semantics._

In the remainder of the paper, we will not explicitly discuss the effects of semantic reduction and vacuity reduction. Rather, we will concentrate on the algebraic properties of ADS that they inherit from their leaf algebra via lifting.

### Lifting

It is well-known that algebraic structures \(A=(\mathcal{A},O)\) can point-wise be lifted to cartesian products and arbitrary function spaces \(M\to A\). This has successfully been exploited for Binary Decision Diagrams (BDDs) and Algebraic Decision Diagrams (ADDs) that canonically represent functions of type \(\mathbb{B}^{n}\rightarrow\mathbb{B}\) and \(\mathbb{B}^{n}\rightarrow\mathcal{A}\) respectively. In fact, the canonicity of these representations allows one to identify the BDD/ADD representations directly with their semantics which, in particular, reduces the verification of semantic equivalence to checking for isomorphism.

In our case, canonicity is unrealistic for two reasons (cf. Section6.1):

1. Considering predicates rather than Boolean values introduces infeasibility and thereby prohibits minimal canonical representations.
2. The ordering of predicates may lead to an exponential explosion of the representation. Please note that, in contrast to, e.g., the typical BDD setting, we do not have just a few (64, 128, 256,... or the like) input bits that specify the control of some circuit, but predicates capture the effect of the ReLU function in a history-dependent way; Predicates that result from computations in a later layer depend on predicates from earlier layers. Moreover, as predicates are continuous objects, the probability of them coinciding can be considered 0. Thus ordering predicates would typically lead to representations that are doubly exponential in the number of neurons of a neural network.

We will see, however, that all the algebraic properties we need also hold for unordered ADSs, and that we can conveniently compute on (arbitrary) representatives of the partition defined by semantic equivalence. This way we arrive at an exponential worst case complexity (in the size of the argument PLNNs) both, for the algebraic operations and the decision of semantic equivalence.

Although ADSs are not canonical one can effectively apply operators on concrete representatives while preserving semantics. Every operator can be lifted inductively as follows

**3.11 Definition (Lifted Operators)**.: For every operator \(\Box:\mathcal{A}^{2}\rightarrow\mathcal{A}\) of an algebra \(A=(\mathcal{A},O)\) we define the lifted operator \(\mathbin{\vbox{\hbox{\vrule height 0.4pt width 0.4pt depth 0.4pt\vrule heigh t 0.4pt width 0.4pt depth 0.4pt}\hrulefill\hbox{\vrule height 0.
Intuitively, for two ADS \(t_{1}\) and \(t_{2}\), this construction replaces leaves in \(t_{1}\) with copies of \(t_{2}\). Thus, each path of the resulting ADS \(t_{3}\) expresses a conjunction of one path in \(t_{1}\) and one path in \(t_{2}\). The partition of the domain imposed by all paths of \(t_{2}\) therefore coincides with the intersection imposed by the intersection of partitions imposed by \(t_{1}\) and \(t_{2}\). The required lifting of the operators to leaf nodes is straightforward (cf. Figure 4 for illustration).

The following theorem which states the correctness of the lifted operators can straightforwardly be proved by induction:

**3.12 Theorem** (Correctness of Lifted Operators): _Let \(t_{1},t_{2}\in\mathcal{S}_{\mathcal{A}}\) be two ADS over some algebra \(A=(\mathcal{A},O)\). Let \(\blacksquare\colon\mathcal{S}_{\mathcal{A}}{}^{2}\to\mathcal{S}_{\mathcal{A}}\) denote the lifted version of the operator \(\Box\in O\). Then the following equation holds for all \(\sigma\in\Sigma\):_

\[\llbracket t_{1}\mathbin{\blacksquare}t_{2}\rrbracket_{S_{\mathcal{A}}}(\sigma) :=\llbracket t_{1}\rrbracket_{S_{\mathcal{A}}}(\sigma)\Box\llbracket t_{2} \rrbracket_{S_{\mathcal{A}}}(\sigma)\]

### Abstraction

Abstraction is one of the most powerful means for achieving scalability. The following easy to prove theorem concerns the interplay of abstractions imposed by a homomorphism of the leaf algebra and their effect on some classification function.

**3.13 Theorem** (Abstraction): _Let \(A=(\mathcal{A},O)\) and \(A^{\prime}=(\mathcal{A}^{\prime},O^{\prime})\) be two algebras, and \(\alpha\colon A\to A^{\prime}\) a homomorphism. Then \(\alpha_{S}\colon\mathcal{S}_{A}\to\mathcal{S}_{A^{\prime}}\) defined by simply applying \(\alpha\) to all the leaves of the argument ADS completes the following commutative diagram:_

We will see in Section 7 how elegantly abstraction can be dealt with in the TADS setting: The abstraction that transforms the XOR regression setting into a classification setting can be easily realized via the TADS composition operator.

## 4 Affine Functions

The following notations of linear algebra are based on the book [1]. The real vector space \((\mathbb{R}^{n},+,\cdot)\) with \(n>0\) is an algebraic structure with the operations

\[+\colon\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}^{n} \text{vector addition}\] \[\cdot\colon\mathbb{R}\ \times\mathbb{R}^{n}\to\mathbb{R}^{n} \text{scalar multiplication}\]

which are defined as

\[(x_{1},\ldots,x_{n})+(y_{1},\ldots,y_{n}) =(x_{1}+y_{1},\ldots,x_{n}+y_{n})\] \[\lambda\cdot(x_{1},\ldots,x_{n}) =(\lambda\cdot x_{1},\ldots,\lambda\cdot x_{n})\]

A real vector \((x_{1},\ldots,x_{n})\) of \(\mathbb{R}^{n}\) is abbreviated as \(\vec{x}\). To refer to one of the components we write \(\vec{x}_{i}:=x_{i}\) (note the arrow ends before the subscript in contrast to \(\vec{x_{i}}\) which denotes the \(i\)-th vector). The dimension of a real vector space \(\mathbb{R}^{n}\) is given as \(\dim\mathbb{R}^{n}=n\).

A matrix \(\mathbf{W}\) is a collection of real values arranged in a rectangular array with \(n\) rows and \(m\) columns.

\[\mathbf{W}=\begin{pmatrix}w_{1,1}&w_{1,2}&\ldots&w_{1,m}\\ w_{2,1}&w_{2,2}&\ldots&w_{2,m}\\ \vdots&\vdots&\ddots&\vdots\\ w_{n,1}&w_{n,2}&\ldots&w_{n,m}\end{pmatrix}\]

To indicate the number of rows and columns one says \(\mathbf{W}\) has _type_\(n\times m\) also notated as \(\mathbf{W}\in\mathbb{R}^{n\times m}\).

An element at position \(i,j\) of the matrix \(\mathbf{W}\) is denoted by \(\mathbf{W}_{i,j}:=w_{i,j}\) (where \(1\leq i\leq n\) and \(1\leq j\leq m\)). A matrix \(\mathbf{W}\in\mathbb{R}^{n\times m}\) can be reflected along the main diagonal resulting in the transpose \(\mathbf{W}^{\top}\) of shape \(m\times n\) defined by the equation

\[(\mathbf{W}^{\top})_{i,j}:=\mathbf{W}_{j,i}\]

The \(i\)-th row of \(\mathbf{W}\) can be regarded as a \(1\times m\) matrix given by

\[\mathbf{W}_{i,\cdot}:=(w_{i,1},\ldots,w_{i,m}).\]

Similarly, the \(j\)-th column of \(\mathbf{W}\) can be regarded as a \(n\times 1\) matrix defined as

\[\mathbf{W}_{\cdot,j}:=(w_{1,j},\ldots,w_{n,j})^{\top}.\]

Matrix addition is defined over matrices with the same type to be component-wise, i.e,

\[(\mathbf{W}+\mathbf{N})_{i,j}:=\mathbf{W}_{i,j}+\mathbf{N}_{i,j}\]

and scalar multiplication as

\[(\lambda\cdot\mathbf{W})_{i,j}:=\lambda\cdot\mathbf{W}_{i,j}.\]

The (type-correct) multiplication of two matrices \(\mathbf{W}\in\mathbb{R}^{n\times r}\) and \(\mathbf{N}\in\mathbb{R}^{r\times m}\) is defined as

\[(\mathbf{W}\cdot\mathbf{N})_{i,j}:=\sum_{k=1}^{r}\mathbf{W}_{i,k}\cdot\mathbf{N}_{k,j}\]

Identifying

* \(n\times 1\) matrices with (column) vectors
* \(1\times m\) matrices with row vectors
* \(1\times 1\) matrices with scalars

as indicated above, makes the well known dot product of \(\vec{v},\vec{w}\in\mathbb{R}^{n}\)

\[\vec{v}^{\top}\cdot\vec{w}:=\sum_{i=1}^{n}\vec{v}_{i}\cdot\vec{w}_{i}\]

just a special case of matrix multiplication. The same holds for matrix vector multiplication that is defined for a \(n\times m\) matrix \(\mathbf{W}\) and a vector \(\vec{x}\in\mathbb{R}^{n}\) as

\[(\mathbf{W}\vec{x})_{i}:=(\mathbf{W}_{i}.)\vec{x}\]

Matrices with the same number of rows and columns, i.e., with type \(n\times n\) for some \(n\in\mathbb{N}\), are said to be _square matrices_. Square matrices have a neutral element for matrix multiplication, called _identity matrix_, that is zero everywhere except for the entries on the main diagonal which are one.

\[\mathbf{I}^{n}:=\begin{pmatrix}1&&0\\ &\ddots&\\ 0&&1\end{pmatrix}\]

The \(i\)-th unit vector \(\vec{e_{i}}\) is a vector where all entries are zero except the \(i\)-th which is one.

### Piece-wise Affine Functions

#### 4.1 Definition (Affine Function)

A function \(\alpha\colon\mathbb{R}^{n}\to\mathbb{R}^{m}\) is called _affine_ iff it can be written as

\[\alpha(\vec{x})=\mathbf{W}\vec{x}+\vec{b}\]

for some matrix \(\mathbf{W}\in\mathbb{R}^{m\times n}\) and vector \(b\in\mathbb{R}^{m}\).7

Footnote 7: Note that, in a traditional neural network application, the \(\mathbf{W}\) and \(\vec{b}\) occurring in a network are the result of some training procedure. In this work, we assume that they are always known and fixed.

We identify the semantics and syntax of affine functions with the pair \((\mathbf{W},\vec{b})\) which can be considered as a canonical representation of affine functions. Furthermore, we denote the set of all affine functions \(\mathbb{R}^{n}\to\mathbb{R}^{m}\) as \(\Phi(n,m)\) and call \((n,m)\) the _type_ of \(\Phi(n,m)\). The untyped version \(\Phi\) is meant to refer to the set of all affine functions, independently of their type.

#### 4.2 Lemma (Operations on Affine Functions)

_Let \(\alpha_{1},\alpha_{2}\) be two affine functions in canonical form, i.e.,_

\[\alpha_{1}(\vec{x}) =\mathbf{W_{1}}\vec{x}+\vec{b_{1}}\] \[\alpha_{2}(\vec{x}) =\mathbf{W_{2}}\vec{x}+\vec{b_{2}}\]

_Assuming matching types, the operations \(+\) (addition), \(\cdot\) (scalar multiplication), and \(\circ\) (function application) can be calculated on the representation as_

\[(s\cdot\alpha_{1})(\vec{x}) =(s\cdot\mathbf{W_{1}})\,\vec{x}+(s\cdot\vec{b_{1}})\] \[(\alpha_{1}+\alpha_{2})(\vec{x}) =(\mathbf{W_{1}}+\mathbf{W_{2}})\,\vec{x}+(\vec{b_{1}}+\vec{b_{2}})\] \[(\alpha_{2}\circ\alpha_{1})(\vec{x}) =(\mathbf{W_{2}}\mathbf{W_{1}})\,\vec{x}+(\mathbf{W_{2}}\vec{b_{1}}+\vec{b_{2 }})\]

_resulting again in an affine function in canonical representation._

It is well-known that the type resulting from function composition evolves as follows

\[\circ\colon\Phi(r,m)\times\Phi(n,r)\to\Phi(n,m).\]

The type of the operation is important for the closure axiom, the basis for most algebraic structures. This leads to the following well-known theorem [1]:

#### 4.3 Theorem (Algebraic Properties)

_Denoting, as usual, scalar multiplication with \(\cdot\) and function composition with \(\circ\), we have:_

* \((\Phi(n,m),+,\cdot)\) _forms a vector space and_
* \((\Phi(n,n),\circ)\) _forms a monoid._

This theorem can straightforwardly be lifted to untyped \(\Phi\) by simply restricting all operations to the cases where they are well-typed, i.e., where addition is restricted to functions of the same type \((+_{t})\), and function composition to situation where the output type of the first function matches the input type of the second \((\circ_{t})\):

#### 4.4 Theorem (Properties of Typed Operations)

\((\Phi,+_{t},\cdot,\circ_{t})\) _forms a typed algebra, i.e, an algebraic structure that is closed under well-typed operations._

Piece-wise affine functions are usually defined over a polyhedral partitioning of the pre-image space [1, 1, 2, 10].

#### 4.5 Definition (Halfspace)

Let \(\vec{w}\in\mathbb{R}^{n}\) and \(b\in\mathbb{R}\). Then the set

\[p=\{\,\vec{x}\in\mathbb{R}^{n}\,|\,\vec{w}^{\top}\cdot\vec{x}+b=0\,\}\]

is called a _hyperplane_ of \(\mathbb{R}^{n}\). A hyperplane partitions \(\mathbb{R}^{d}\) into two convex subspaces, called _halfspaces_. The positive respectively negative halfspace of \(p\) is defined as

\[p^{+} :=\{\,\vec{x}\in\mathbb{R}^{n}\,|\,\vec{w}^{\top}\cdot\vec{x}+b>0\,\}\] \[p^{-} :=\{\,\vec{x}\in\mathbb{R}^{n}\,|\,\vec{w}^{\top}\cdot\vec{x}+b<0\,\}\]
**4.6 Definition (Polyhedron).** A polyhedron \(Q\subseteq\mathbb{R}^{n}\) is the intersection of \(k\) halfspaces for some natural number \(k\).

\[Q=\bigcap_{i=1}^{k}\{\,\vec{x}\in\mathbb{R}^{n}\,|\,\vec{w_{i}}^{\top}\cdot\vec {x}+b_{i}\leq 0\,\}\]

**4.7 Definition (Piece-wise Affine Function).** A function \(\psi\colon\mathbb{R}^{n}\to\mathbb{R}^{m}\) is called _piece-wise affine_ if it can be written as

\[\psi(\vec{x})=\alpha_{i}(\vec{x})\ \ \text{for}\ \ \vec{x}\in Q_{i}\]

where \(Q=\{\,Q_{1},\ldots,Q_{k}\,\}\) is a set of polyhedra that partitions the space of \(\vec{x}\) and \(\alpha_{1},\ldots,\alpha_{k}\) some affine functions. We call \(\alpha_{i}=\mathbf{W}_{i}\vec{x}+\vec{b}_{i}\) (\(1\leq i\leq k\)) the function associated with polyhedron \(Q_{i}\).

The proof of the following property is straightforward:

**4.8 Proposition (Continuity).**_A piece-wise affine function is continuous iff at each border between two connected polyhedra the affine functions associated with either polygon agree._

### The Activation Function ReLU

In this paper, we focus on neural network architectures that use the ReLU activation function:

**4.9 Definition (ReLU).** The Rectified Linear Unit (ReLU)

\[\text{ReLU}^{k}:\mathbb{R}^{k}\to\mathbb{R}^{k}_{+}\]

is a projection of \(\mathbb{R}^{k}\) onto the space of positive vectors \(\mathbb{R}^{k}_{+}\) defined by replacing each component \(x_{i}\) of a vector \(\vec{x}\) by \(\max\{\,0,x_{i}\,\}\):

\[\big{(}\ \text{ReLU}^{k}(\vec{x})\,\big{)}_{j}:=\max\{\,0,x_{j}\,\}\]

If the input dimension is clear, we omit the index and just write ReLU.

The term \(\max\{\,0,x_{i}\,\}\) is continuous and piece-wise linear. As ReLU operates independently on all dimensions of its input, it is itself piece-wise linear.

From a practical perspective, ReLU is one of the best understood activation functions, and the corresponding rectifier networks are one of the most popular modern neural network architectures [1].

For ease of notation in later sections, we use the fact that ReLU operates on each component of a vector independently and can therefore be decomposed into

\[\text{ReLU}^{k}=\phi_{k}^{k}\circ\phi_{k-1}^{k}\circ\cdots\circ\phi_{1}^{k}\]

where \(\phi_{i}^{k}:\mathbb{R}^{k}\to\mathbb{R}^{k}\) is the _partial ReLU function_ defined by setting the \(i\)-th component of a vector \(\vec{x}\) to \(0\) iff \(x_{i}<0\). More formally,

\[\big{(}\,\phi_{i}^{k}(\vec{x})\,\big{)}_{j}:=\begin{cases}x_{j}&\text{if }i \neq j\\ \max\{\,0,x_{j}\,\}&\text{if }i=j\end{cases}\,.\]

## 5 Piece-wise Linear Neural Network

Piece-wise linear neural networks are specific representations of continuous piece-wise affine functions. Calling them piece-wise linear is formally incorrect (the term piece-wise affine would be correct), but established. For the ease of exposition, we restrict the following development to the case where all activation functions are partial ReLU functions. This suffices to capture the entire class of Rectifier Networks which, themselves, can represent all piece-wise affine functions [1]. We adopt the popular naming in the following definition:

**5.1 Definition (Rectifier Neural Networks).** The syntax for _Rectifier Neural Networks_, or here synonymously used, _Piece-wise Linear Neural Networks_ (PLNNs), is defined by the following BNF

\[\mathcal{N}\,:=\,\varepsilon\ |\ \alpha\;;\mathcal{N}\ |\ \phi\;;\mathcal{N}\]

where the meta variables \(\alpha\) and \(\phi\) stand for affine functions and partial ReLU functions, respectively. Writing PLNNs as \(N=f_{0}\;;\cdots;f_{l}\) where \(f\in\{\,\alpha,\phi\,\}\) we denote the set of all PLNNs with \(\text{dom}(f_{0})=\mathbb{R}^{n}\) and \(\text{codom}(f_{l})=\mathbb{R}^{m}\) as \(\mathcal{N}(n,m)\) and the set of all PLNNs as

\[\mathcal{N}=\bigcup_{n,m\in\mathbb{N}}\mathcal{N}(n,m)\]

This definition of a PLNN slightly flexibilizes the classical definition as it does not require the strict alternation of affine functions and activation functions and uses partial ReLU functions instead of ReLU. We will exploit this flexibility to directly have the right granularity for defining according operational semantics (cf. Section 5.2).

### Example (Representing XOR as PLNN).

As stated in Section 2, our baseline solution to the XOR regression model is defined by the function \(|x-y|\). We can represent this function as a PLNN \(N_{*}\). It consists of two affine functions

\[\alpha_{1}=\begin{pmatrix}1&-1\\ -1&1\end{pmatrix}\qquad\qquad\alpha_{2}=\begin{pmatrix}1&1\end{pmatrix}\]
and two partial ReLUs applied in this order:

\[N_{*}:=\alpha_{1}\,;\phi_{1}^{2}\,;\phi_{2}^{2}\,;\alpha_{2}\]

Note typically \(N_{*}\) would be defined as

\[N_{*}^{\prime}=\alpha_{1}\,;\text{ReLU}\,;\alpha_{2}\]

in the context of machine learning. However, as both definitions impose the same semantics

\[\llbracket N_{*}\rrbracket_{\text{\sc DS}}=\llbracket N_{*}^{\prime} \rrbracket_{\text{\sc DS}}\]

we defined it directly using the notational conventions of this paper. This construction uses the observation that

\[\text{ReLU}(x-y)=\begin{cases}x-y&\text{if }x>y\\ 0&\text{otherwise}\end{cases}\.\]

The following figure shows the (instantiated) corresponding network architecture:

\[\begin{array}{c}\includegraphics[scale=0.5]{fig
Thus, the operational semantics \([\![\,\cdot\,]\!]_{\mathrm{os}}\) provides a constructive, local, and correct semantic interpretation of PLNNs.

**5.7 Example (Semantics of \(\boldsymbol{N_{\star}}\)).** We consider the baseline solution to the XOR regression model defined by the function \(|x-y|\). The network \(N_{\star}\) implements this function as a PLNN. We calculate \([\![N_{\star}]\!]_{\mathrm{os}}\) by applying the SOS rules to the initial configuration \(\langle N_{\star},(1,0)^{\top}\rangle\).

\[\langle\alpha_{1}\,;\,\phi_{1}^{2}\,;\phi_{2}^{2}\,;\alpha_{2},(1, 0)^{\top}\rangle\] \[\stackrel{{\mathrm{tt}}}{{\longrightarrow}} \langle\phi_{1}^{2}\,;\phi_{2}^{2}\,;\alpha_{2},(1,-1)^{\top}\rangle\] \[\stackrel{{\mathrm{l}}}{{\longrightarrow}} \langle\phi_{2}^{2}\,;\alpha_{2},(1,-1)^{\top}\rangle\] \[\stackrel{{\mathrm{o}}}{{\longrightarrow}} \langle\alpha_{2},(1,0)^{\top}\rangle\] \[\stackrel{{\mathrm{tt}}}{{\longrightarrow}} \langle\varepsilon,1\rangle\]

This is the correct outcome. Note that the SOS rules correspond to an iterative processing of each component function (i.e., layer) of the neural network, much like function composition.

Next we will naturally adapt the presented rules to symbolic execution which, by itself, provides the first outcome explanation of PLNNs.

### Symbolic Execution of PLNNs

Symbolic execution aims at characterizing program states in terms of symbolic input values and corresponding path conditions. In particular, it reveals how program states depend on the initial values during execution. PLNNs are ideally suited for symbolic execution as they are acyclic computation graphs and contain only affine computations.

* Affine functions are closed under composition. This allows one to aggregate (partially evaluate) the entire symbolic computation history corresponding to some symbolic execution path in terms of a single affine function, and to express all paths conditions as affine inequalities also expressed in terms of the initial values.
* PLNNs possess finite, acyclic computation graphs which, conceptually, allows for precise execution without need for abstractions.

In Section6, we will see that this results in a directed, acyclic, side-effect free computation graph whose leaves are affine function in \(\Phi(n,m)\) that express the PLNN's effect on inputs belonging to the polyhedron specified by the path condition.

We define the required symbolic execution via derivation rules that transform configurations of the form \(\langle N,\alpha,\pi\rangle\) where

* \(N\in\mathcal{N}(r,m)\),
* \(\alpha\colon\mathbb{R}^{n}\to\mathbb{R}^{r}\) with representation \(\alpha(\vec{x})=\boldsymbol{W}\vec{x}+\vec{b}\),
* and \(\pi\) is a path condition

throughout the transformation. The dimensions of \(n\) and \(m\) are bound by the initial PLNN while \(r\) is the dimension of some hidden layer. The following definition operates on the concrete representations of \(N\), \(\alpha\), and \(\pi\). In the case of the last two, the representation is expected to be canonical and therefore syntax and semantics can be identified.8 Operations are expected to be applied directly to the representation. Thus, the effect of a concrete execution path of \([\![\,\cdot\,]\!]_{\mathrm{os}}\) is _aggregated_ (instead of simply recorded) into the components \(\alpha\) and \(\pi\) while \(N\) is destructed further and further until all layers have been considered.

Footnote 8: By using canonical representations it is impossible to trace the history of operations. One effectively cannot distinguish between isomorphic objects.

**5.8 Definition (Symbolic Execution of PLNNs).**

\[\langle\alpha^{\prime}\,;N,\alpha,\pi\rangle \stackrel{{\mathrm{tt}}}{{\longrightarrow}}_{ \mathrm{SOS}}\langle N,\alpha^{\prime}\circ\alpha,\pi\rangle\] \[\langle\phi_{i}^{k}\,;N,\alpha,\pi\rangle \stackrel{{\mathrm{l}}}{{\longrightarrow}}_{ \mathrm{SOS}}\langle N,\alpha,\pi^{\prime}\wedge\pi\rangle\] \[\langle\phi_{i}^{k}\,;N,\alpha,\pi\rangle \stackrel{{\mathrm{o}}}{{\longrightarrow}}_{ \mathrm{SOS}}\langle N,\boldsymbol{E}_{i}^{k}\circ\alpha,\neg\pi^{\prime} \wedge\pi\rangle\]

where \(\pi^{\prime}=\alpha(x)_{i}\geq 0\).

For a sequence

\[c_{0}\stackrel{{ a_{1}}}{{\longrightarrow}}_{ \mathrm{SOS}}c_{1}\,\cdots\,c_{n-1}\stackrel{{ a_{n}}}{{ \longrightarrow}}_{\mathrm{SOS}}c_{n}\]

of derivations we write \(c_{0}\stackrel{{ a_{1}\cdots a_{n}}}{{\longrightarrow}}_{ \mathrm{SOS}}c_{n}\). Further we denote with \((\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \!\!
The second states the effect of other starting values in the initial configuration. Note that this relation does not hold in the reversed case, as \(\circ\) and \(\wedge\) are not injective and the configuration is only determined up to isomorphism. The last identity corresponds to the result that of Definition 5.4 is uniquely determined. As the symbolic rules are more general the result is restricted to the case where the word \(w\) is known.

Moreover, the path conditions induce a partition of the input space \(\mathbb{R}^{n}\).

**5.10 Lemma** (Partition of \(\pi\)).: _For an arbitrary but fixed \(N\in\mathcal{N}\) define the set of all derivations with depth \(k\) as_

\[V_{k}(N):=\{\,c\mid\langle N,\operatorname{id},\operatorname{tt}\rangle \stackrel{{ w}}{{\longrightarrow}}_{\operatorname{SOS}}c\, \wedge\,|w|=k\,\}\]

_Define the set of all path conditions of the same \(V_{k}\) as \(\Pi_{k}\), then_

* _each_ \(\pi\in\Pi_{k}\) _defines a polyhedron for_ \(k>0\)__
* _the polyhedra of_ \(\Pi_{k}\) _are a partition of_ \(\mathbb{R}^{n}\)_._

Proof.: Induction over derivation sequences of \(N\). 

Specifically, for each input vector \(\vec{x}\in\mathbb{R}^{n}\), there exists exactly one sequence of derivations \(\langle N,\operatorname{id},\operatorname{tt}\rangle\stackrel{{ w}}{{\longrightarrow}}_{\operatorname{SOS}}\langle \varepsilon,\alpha,\pi\rangle\) such that \(\pi(\vec{x})\) holds. Therefore, the following is well-defined:

**5.11 Definition** (Semantic Functional \(\llbracket\,\cdot\,\rrbracket_{\operatorname{SOS}}\)).: The semantic functional for the symbolic operational semantics

\[\llbracket\,\cdot\,\rrbracket_{\operatorname{SOS}}:\mathcal{N}(n,m)\to( \mathbb{R}^{n}\to\mathbb{R}^{m})\]

is defined as \(\llbracket N\rrbracket_{\operatorname{SOS}}(\vec{x})=\vec{y}\) iff

\[\langle N,\operatorname{id},\operatorname{tt}\rangle\stackrel{{ *}}{{\longrightarrow}}_{\operatorname{SOS}}^{*}\langle \varepsilon,\alpha,\pi\rangle\;\;\;\wedge\;\;\;\pi(\vec{x})=1\;\;\;\wedge\;\; \alpha(\vec{x})=\vec{y}\]

Also the symbolic operational semantics is fully aligned with the denotational semantics:

**5.12 Theorem** (Correctness of \(\llbracket\,\cdot\,\rrbracket_{\operatorname{SOS}}\)).: _For any \(N\in\mathcal{N}\) we have: \(\llbracket N\rrbracket_{\operatorname{DS}}=\llbracket N\rrbracket_{ \operatorname{SOS}}\)._

Proof.: According to Theorem 5.12, it suffices to show the semantic equivalence with \(\llbracket\,\cdot\,\rrbracket_{\operatorname{SOS}}\). As both the concrete and the symbolic operational semantics define unique computation paths for each input vector, the proof follows straightforwardly by an inductive proof that establishes the desired equivalence as an invariant when simultaneously following these paths. More concretely, we can prove

\[\forall\vec{x}\in\mathbb{R}^{n}:\llbracket N\rrbracket_{\operatorname{ OS}}(\vec{x})=\llbracket N\rrbracket_{\operatorname{SOS}}(\vec{x})\]

using the following induction hypothesis

\[\langle N_{0},\vec{x_{0}}\rangle\stackrel{{ w}}{{\longrightarrow}}_{ \operatorname{OS}}\langle N_{k},\vec{x_{k}}\rangle\iff\] \[\langle N_{0},\operatorname{id},\operatorname{tt}\rangle\stackrel{{ w}}{{\longrightarrow}}_{\operatorname{SOS}}\langle N_{k},\alpha_{k},\pi_{k} \rangle\wedge\alpha_{k}(\vec{x_{0}})=\vec{x_{k}}\wedge\pi_{k}(\vec{x_{0}})\]

by a simple analysis of the following three cases:

1. \(N_{k+1}=\alpha^{\prime}\,;N_{k}\)
2. \(N_{k+1}=\phi_{i}^{k}\,;N_{k}\;\wedge\;\vec{x}_{i}\geq 0\)
3. \(N_{k+1}=\phi_{i}^{k}\,;N_{k}\;\wedge\;\vec{x}_{i}<0\) 

The symbolic operational semantics of PLNNs is sufficient to derive local explanations and decision boundaries similar to the ones presented in [1, 1, 2, 3]. In the following, we will show how symbolic operational semantics can be used to define semantically equivalent Typed Affine Decisions Structures (TADS) which, themselves, are specific Algebraic Decision Structures (ADS) as defined in the next section. TADS collect all the local explanations in an efficient query structure such that we arrive at model explanations.

**5.13 Example** (XOR-Regression).: As a brief example for the symbolic execution of PLNNs, we will calculate \(\llbracket N_{\star}\rrbracket_{\operatorname{SOS}}\) by applying the symbolic SOS rules to the initial configuration \(\langle N_{\star},\operatorname{id},\operatorname{tt}\rangle\). Symbolic interpretation is not deterministic for the partial ReLU functions. We therefore chose the execution path that corresponds to the former example \(\vec{x}=(1,0)^{\top}\), i.e., with the label sequence \(w=(\operatorname{tt},1,0,\operatorname{tt})\), for illustration:

\[\langle\alpha_{1}\,;\phi_{1}^{2}\,;\phi_{2}^{2}\,;\alpha_{2}, \begin{pmatrix}1&0\\ 0&1\end{pmatrix},\operatorname{tt}\rangle\] \[\stackrel{{\operatorname{tt}}_{\operatorname{SOS}}}{{ \longrightarrow}}\langle\phi_{1}^{2}\,;\phi_{2}^{2}\,;\alpha_{2},\begin{pmatrix} 1&-1\\ -1&1\end{pmatrix},\operatorname{tt}\rangle\] \[\stackrel{{ 1}}{{\longrightarrow}}_{\operatorname{SOS}} \langle\phi_{2}^{2}\,;\alpha_{2},\begin{pmatrix}1&-1\\ -1&1\end{pmatrix},x_{1}-x_{2}\geq 0\rangle\] \[\stackrel{{ 0}}{{\longrightarrow}}_{\operatorname{SOS}} \langle\alpha_{2},\begin{pmatrix}1&-1\\ 0&0\end{pmatrix},x_{1}-x_{2}>0\rangle\] \[\stackrel{{\operatorname{tt}}_{\operatorname{SOS}}}{{ \longrightarrow}}\langle\varepsilon,\begin{pmatrix}1&-1\\ 0&1\end{pmatrix},x_{1}-x_{2}>0\rangle\]

Note that the path conditions and the affine functions have been simplified in every step. The affine functions are given in their canonical representation \(\boldsymbol{W}\vec{x}+\vec{b}\) (as \(\vec{b}\) is zero in all steps it is omitted). For the path conditions we have not fixed a representation, instead they are simplified to aid readability. The most important simplifications are

\[\left(\begin{pmatrix}1&-1\\ -1&1\end{pmatrix}\vec{x}\right)_{1}\geq 0 \iff x_{1}-x_{2}\geq 0\] \[\neg(-x_{1}+x_{2}\geq 0)\wedge x_{1}-x_{2}\geq 0 \iff x_{1}-x_{2}>0\]
## 6 Typed Affine Decision Structures

Consider the transition system \((V,\rightarrow_{\textsc{sos}})\) that represents the symbolic operational semantics \([\![\,\cdot\,]\!]_{\textsc{sos}}\) of some \(N\in\mathcal{N}(n,m)\) where

\[V=\{\,c\mid\langle N,\mathrm{id},\mathrm{tt}\rangle\rightharpoonup_{\textsc{ SOS}}^{*}\,c\,\}\]

is the set of configurations which are reachable from \(\langle N,\mathrm{id},\mathrm{tt}\rangle\) and let (recall Definitions 3.4 and 4.1)

\[\tau\colon V\rightarrow\mathcal{S}_{\Phi}\]

denote the following inductively defined transformation that closely follows the symbolic SOS rules:

* \(\tau(\langle\varepsilon,\alpha,\,\cdot\,\rangle)\ :=\ \alpha\)
* \(\tau(\langle\alpha^{\prime}\,;N,\alpha,\,\cdot\,\rangle)\ :=\ (\mathrm{tt},\tau(\langle N,\alpha^{\prime}\circ\alpha,\, \cdot\,\rangle),\varepsilon)\)
* \(\tau(\langle\phi_{i}^{k}\,;N,\alpha,\,\cdot\,\rangle)\) \(:=\ (\alpha(x)_{i}\geq 0,\tau(\langle N,\alpha,\,\cdot\,\rangle),\tau( \langle N,\boldsymbol{E}_{i}^{k}\circ\alpha,\,\cdot\,\rangle))\)

where \(``\,\cdot\,"\) should be considered a don't care entry. Identifying \(N\) with its computation tree which is specified by its set of configurations that are reachable from \(\langle N,\mathrm{id},\mathrm{tt}\rangle\),9\(\tau\) can be regarded as an injective relabeling of this tree which results in the structure of an ADT:

Footnote 9: Please note that the transition labels \(\mathrm{tt},\,1\), and \(0\) are redundant.

**6.1 Theorem (TADT)**.: _Let \(N\in\mathcal{N}(n,m)\). Then \(\tau(N)\) is an ADT over \(\Phi(n,m)\) whose predicates are all of the form of affine inequalities._

Proof.: The proof follows by straightforward induction along the isomorphic structure of the two trees. The following invariants hold for all steps of the transformation

\[\tau(c)=(p,\tau(c_{t}),\,\cdot\,) \iff c\xrightarrow{1}_{\textsc{sos}}c_{t}\] \[\tau(c)=(p,\,\cdot\,,\tau(c_{f})) \iff c\xrightarrow{0}_{\textsc{sos}}c_{f}\]

where we abbreviate \(c=\langle N,\alpha,\pi\rangle\), \(c_{t}=\langle N^{\prime},\alpha^{\prime},p\wedge\pi\rangle\), and \(c_{f}=\langle N^{\prime},\alpha^{\prime},\neg p\wedge\pi\rangle\)

We call the structures resulting from \(\tau\)-transformation _Typed Affine Decision Trees_ (TADT). A TADT inherits the type from its underlying algebra of typed affine functions \(\Phi(n,m)\) (cf. Lemma 4.2 and Theorem 4.4). Similar to ADTs, TADT can also be generalized to acyclic graph structures:

**6.2 Definition (Typed Affine Decision Structure)**.: An ADS over the algebra \((\Phi(n,m),+_{t},\cdot,\circ_{t})\) where all predicates are linear inequalities in \(\mathbb{R}^{n}\) is called _Typed Affine Decision Structure_ of type \(n\times m\).

The set of all such decision structures is denoted by \(\Theta(n,m)\), and the set of all typed affine decision structures of any type with:

\[\Theta=\bigcup_{n,m\in\mathbb{N}^{+}}\Theta(n,m)\]

TADS are special kinds of ADS. Thus, they inherit the ADS semantics (cf. Definition 3.5) when specializing \(\Sigma\) to \(\mathbb{R}^{n}\) and \(\sigma\) to \(\vec{x}\). The fact that the semantics of leafs is given by affine functions that are also applied to \(\vec{x}\) is not important for the resulting specialized definition which reads:

**6.3 Definition (Semantics of TADS)**.: The semantic function

\[[\![\,\cdot\,]\!]_{\mathfrak{o}}\colon\Theta(n,m)\rightarrow(\mathbb{R}^{n} \rightarrow\Phi(n,m))\]

for TADS is inductively defined as

\[[\![\alpha]\!]_{\mathfrak{o}}(\vec{x}) :=\alpha(\vec{x})\] \[\![(p,l,r)]_{\mathfrak{o}}(\vec{x}) :=\begin{cases}[\![l]\!]_{\mathfrak{o}}(\vec{x})&\text{if }[\![p]\!](\vec{x})=1\\ [\![r]\!]_{\mathfrak{o}}(\vec{x})&\text{if }[\![p]\!](\vec{x})=0\end{cases}\]

Every PLNN \(N\) defines an ADT \(t_{N}\) over \(\Phi\). We can therefore apply the results of Section 3. In particular, we can apply the various reduction techniques which transform \(t_{N}\) into the more general form of an ADS, or more precisely, of a TADS.

Optimizations in terms of semantic reduction and infeasible path elimination do not alter the semantics of a (T)ADS. In other words

\[\Theta(N)\ =\ \{t\mid[\![t]\!]_{\mathfrak{o}}=[\![(\tau(N)]\!]_{\mathfrak{o}}\}\]

is closed under semantic reduction and infeasible path elimination. Moreover, we have:

**6.4 Theorem (Correctness of \([\![t]\!]_{\mathfrak{o}}\))**.: _Let \(N\ \in\ \mathcal{N}\) and \(t\in\Theta(N)\). Then we have:_

\[[\![N]\!]_{\textsc{ds}}=[\![t]\!]_{\mathfrak{o}}\]

In the following, we sometimes abuse notation and also write \(\tau(N)\) for other members of \(t\in\Theta(N)\) when the concrete structure of the TADS does not matter. This concerns, in particular, Section 7 where we always apply semantic reduction and infeasible path elimination to reduce size.

Following [GMR\({}^{+}\)18]:

In the state of the art a small set of existing interpretable models is recognized: decision tree, rules, linear models \([\![\ldots]\!]\). These models are considered easily understandable and interpretable for humans. ([GMR\({}^{+}\)18])
we have:

**6.5 Corollary (Model Explanation)**.: _TADS provide precise solutions to the model explanation problem, and therefore also to the outcome explanation problem._

Please note that outcome explanation is easily derived from model explanation simply by following the respective evaluation path.

**6.6 Example (XOR-TADS)**.: As an example, the resulting TADS of the symbolic execution ADS of \(N_{*}\) is shown in Figure 3.

### The TADS Linear Algebra

According to Theorem 4.4, \((\Phi,+_{t},\,\cdot_{t}\,)\) forms a typed algebra. Moreover, due to the canonical representation of affine functions, \(\Phi\) also supports the equality relation \(=\). Applying Theorem 3.12, all these operations can be lifted to obtain the following corresponding operations on TADS:

1. \(\oplus\colon\Theta(n,m)\times\Theta(n,m)\to\Theta(n,m)\)
2. \(\ominus\colon\Theta(n,m)\times\Theta(n,m)\to\Theta(n,m)\)
3. \(\ominus\colon\mathbb{R}\times\Theta(n,m)\to\Theta(n,m)\)
4. \(\bigodot\colon\Theta(n,m)\times\Theta(n,m)\to\Theta(n,1)\)

These operations lift in the order that they are given (1) addition, (2) subtraction10, (3) scalar multiplication, and (4) equality. The resulting TADS has size \(\mathcal{O}(|t_{1}|\cdot|t_{2}|)\) where \(|t_{i}|\) is the number of nodes of considered TADS \(t_{i}\). An example of addition is given in Figure 4.

Footnote 10: Subtraction is usually not stated explicitly as it can be defined using addition and scalar multiplication.

The operations \(\oplus\) and \(\odot\) are characteristic for vector spaces. Indeed, TADS form a (function) vector space (cf. Theorems 4.3 and 4.4):

**6.7 Theorem (The TADS Linear Algebra)**.: \((\Theta,\oplus_{t},\odot_{t})\) forms a typed linear algebra.

We will exploit this theorem in Section 7.

However, when lifting these two operators over affine predicates a second interpretation occurs naturally: that of _piece-wise affine functions_. Both interpretations are compatible, as stated in the following lemma.

**6.8 Theorem (Two Consistent Views on TADS)**.: _Let \(\psi_{1},\psi_{2}\colon\mathbb{R}^{n}\to\mathbb{R}^{m}\) be two piece-wise affine functions and \(\vec{x}\in\mathbb{R}^{n}\) be a real vector. Define \(\alpha_{1}\) as the affine function of \(\psi_{1}\) that is associated with the region for \(\vec{x}\) and \(\alpha_{2}\) for \(\psi_{2}\), respectively and denote with \(\Box\) a generic operation over (piece-wise) affine functions. Then if for all such \(\vec{x}\)_

\[\psi_{1}(\vec{x})\Box\psi_{2}(\vec{x})=\alpha_{1}(\vec{x})\Box\alpha_{2}(\vec {x})\]

_holds both interpretations agree for \(\Box\)._

One can easily show that this is indeed the case for \(\Box\in\{\,\oplus,\odot,\odot\,\}\). However, there is a slight difference in the interpretations. The first _lifts_ affine functions over affine predicates and the latter _associates_ affine functions with affine predicates. This distinction can, for example, be seen in the signature of the respective semantics:

\[\llbracket t\rrbracket_{S_{A}}\colon\mathbb{R}^{n} \to(\mathbb{R}^{n}\to\mathbb{R}^{m})\] \[\llbracket t\rrbracket_{\Theta}\colon\mathbb{R}^{n} \to\ \mathbb{R}^{m}\]

For TADS to be equivalent to piece-wise affine functions the semantics have to be adapted to \(\llbracket\cdot\,\rrbracket_{\Theta}\), which slightly differs from \(\llbracket\cdot\,\rrbracket_{S_{A}}\) in that the leafs are also evaluated under the input.

Considering Lemma 5.10, one can easily see that every path in a TADS defines a polyhedron and that the set of all paths partitions \(\mathbb{R}^{n}\). As all terminals of TADS are affine functions, it is straightforward to prove that for every TADS \(t\) the semantics \(\llbracket t\rrbracket_{\Theta}\) is a piece-wise affine function.

The complexity of piece-wise affine functions is commonly defined as the smallest number of classes (so-called regions) that are needed to partition the input space [12, 13, 14], and which we call _region complexity_. This complexity measure can easily be adopted for TADS using the above reasoning as it is simply the number of all paths from the root to its terminals. In other words, TADS are linear-size representations of PAF with respect to their region complexity which implies:

**6.9 Theorem (Complexity of Operations)**.: _The operations \(\oplus,\ominus,\bigodot\) are of quadratic and \(\odot\) of linear time region complexity._

Figure 3: The TADS \(\tau(N_{*})\).
Proof.: Via structural induction along Definition3.11 it is easy to establish that each node of the tree underlying \(t_{1}\) is processed at most once, while the nodes of the tree underlying \(t_{2}\) may be processed at most once for each leaf of \(t_{1}\). The theorem follows from the fact that the number of nodes in a binary tree is at most twice the number of its paths. 

Interesting is the expression \(t_{1}\ominus t_{2}\) which evaluates to the constant function \(0\) iff \(t_{1}\) and \(t_{2}\) are semantically equivalent. Thus we have the following:

**6.10 Corollary** (Complexity of \(\equiv\)).: _Deciding semantic equivalence between two TADS has quadratic time region complexity._

Please note that this way of deciding semantic equivalence does not only provide a Yes/No answer, but, in case of failure, also precise diagnostic information: For \(t_{2}-t_{1}\) we have (see Figure11)

* positive parts mark regions where \(t_{2}\) is bigger
* zero marks regions where both TADS agree
* negative parts mark regions where \(t_{1}\) is bigger

This is particularly interesting when combined with a threshold \(\varepsilon\) (see Figure13).

### The TADS Typed Monoid

As shown in previous sections, TADS are a comprehensible and efficient representation of piece-wise affine functions. In the following, we will go even further and show that TADS also directly support all common operations on piece-wise affine functions.

Piece-wise affine functions form a typed monoid under function composition, i.e., the composition of two piece-wise affine functions is again piece-wise affine assuming that domain and co-domain adequately match. This property is highly useful both, for the design of neural networks--which are themselves fundamentally compositions of multiple, simple piece-wise affine functions--and neural network analysis, as will be shown in Section7.

Consider the following result which follows as a consequence of the previous correctness theorems and the compositionality of \(\llbracket\cdot\rrbracket_{\mathrm{DS}}\):

**6.11 Corollary** (Compositionality).: _Let \(N_{0},N_{1},N_{2}\in\mathcal{N}\) with \(N_{0}=N_{1}\;;N_{2}\) and \(t_{i}\in\Theta(N_{i})\). Then we have:_

\[\llbracket N_{0}\rrbracket_{\mathrm{DS}} =\llbracket N_{1}\;;N_{2}\rrbracket_{\mathrm{DS}}\] \[=\llbracket N_{2}\rrbracket_{\mathrm{DS}}\circ\llbracket N_{1} \rrbracket_{\mathrm{DS}}\] \[=\llbracket t_{2}\rrbracket_{\mathrm{e}}\circ\llbracket t_{1} \rrbracket_{\mathrm{e}}=\llbracket t_{0}\rrbracket_{\mathrm{e}}\]

Obviously, there is a gap in the result that poses the question: "Is it possible to define composition operator that directly works on TADS?" Just composing the affine functions at the leafs, which would be sufficient to, e.g., for \(\oplus\), is insufficient because of the side effect of the first TADS. Thus we end up with the following composition operator that handles this side effect in a way that is typical for structured operational semantics:

**6.12 Definition** (TADS Composition).: _The composition operator \(\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}\) of TADS with type_

\[\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}:\Theta(n,r)\times \Theta(r,m)\to\Theta(n,m)\]

_is inductively defined as_

\[\alpha\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}} \alpha^{\prime} =\alpha^{\prime}\circ\alpha\] \[\alpha\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}(p,l, r) =(p\circ\alpha,\alpha\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$ \star$}}}l,\alpha\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}r)\] \[(p,l,r)\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}t =(p,l\mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}t,r \mathbin{\raisebox{-0.86pt}{\scalebox{1.2}{$\star$}}}t)\]

_where \(\alpha,\alpha^{\prime}\in\Phi\) are TADS identified with their affine function, \(t,l,r\in\Theta\) are TADS, and \(p\in\mathcal{P}\) is a predicate. Here \(p\circ\alpha\) with \(p=\alpha^{\prime}(x)_{i}\geq 0\) is defined as_

\[(\alpha^{\prime}\circ\alpha)(x)_{i}\geq 0\]

Figure 4: Example for (T)ADS addition. The (T)ADS in (a) and (b) are based on partial ReLUs and (c) is the sum of both. The input vector is given as \(\vec{x}=(a,b)\) with \(a,b\in\mathbb{R}\).
Notice that this definition is similar to the lifted operators of Definition 3.11. However, TADS composition is not side-effect free as can be seen by the modification of the predicate in the second case. This is due to the fact that the first TADS distorts the input vector space of the second TADS. Again, let us formalize the correctness of this operation.

**6.13 Theorem (TADS Composition)**.: _Let \(t_{1}\in\Theta(n,r)\) and \(t_{2}\in\Theta(r,m)\). Then we have:_

\[\llbracket t_{1}\ltimes t_{2}\rrbracket_{\mathrm{o}}=\llbracket t_{2} \rrbracket_{\mathrm{o}}\circ\llbracket t_{1}\rrbracket_{\mathrm{o}}\]

Proof.: Structural induction along the second component and in the inductive step induction along the first component. 

An example of a composition can be found in Figure 5. This directly yields:

**6.14 Corollary (The TADS typed Monoid)**.: \((\Theta,\ltimes)\) _forms a typed monoid, i.e, an algebraic structure that is closed under type-correct composition and that has typed neutral elements \(\varepsilon\)._

_On this structure \(\tau\) is a homomorphism between the monoids \((\Theta,\ltimes)\) and \((N,;)\), i.e., the following diagram commutes_

Due to their similarity to the lifted operators it is easy to show that composing to TADS results in a third TADS that has size complexity equal to product of its inputs and whose complexity with respect to the measure of affine regions is quadratic in its inputs. Following the same line of reasoning as for Theorem 6.9 yields:

**6.15 Theorem (Complexity of Composition)**.: _TADS compositions has quadratic time region complexity._

One may argue that semantic equivalence between two TADS is of limited practical value, in particular, as in most applications of neural networks, small errors are, to a certain degree accepted. In contrast, \(\epsilon\)-similarity, i.e., whether two TADS differ more than \(\epsilon\) for some small threshold \(\epsilon\in\mathbb{R}\), can be regarded as a practically very relevant notion, in particular, to study robustness properties. The corresponding property required for TADS leaves is easily defined:

\[l_{\epsilon}(x,y):=(|x-y|-\epsilon)\,\mathbb{I}(|x-y|\geq\epsilon)\]

Intuitively, this function yields \(0\) if the difference of \(x\) and \(y\) is less than \(\epsilon\) and the absolute value (minus epsilon) of their difference otherwise. \(l_{\epsilon}\) can easily be realized using only standard algebraic operations and ReLU applications which are already defined:

\[l_{\epsilon}=\mathrm{ReLU}(x-y-\epsilon)+\mathrm{ReLU}(y-x-\epsilon)\]

Just lifting this function to the TADS level

\[t_{4}=\mathrm{ReLU}(t_{1}\ominus t_{2}\ominus\epsilon)\oplus\mathrm{ReLU}(t _{2}\ominus t_{1}\ominus\epsilon)\]

(where \(\mathrm{ReLU}(t)=t\ltimes\tau(\mathrm{ReLU})\)) is sufficient to decide \(\epsilon\)-similarity. Thus we have:

**6.16 Corollary (Deciding \(\epsilon\)-similarity)**.: \(\epsilon\)_-similarity has quadratic time region complexity._

Please note that, again, this way of deciding \(\epsilon\)-similarity does not only provide a Yes/No answer, but, in case of failure, also precise diagnostic information. All this will be showcased in Section 7.

In the remainder of this section we elaborate on the compositionality that is imposed by \(\ltimes\):

**6.17 Corollary (Layer-wise Transformation)**.: _By Theorem 6.13, we can transform a PLNN layer-wise into a TADS._

\[\llbracket N\rrbracket_{\mathrm{DS}} =\llbracket\alpha_{1}\,;\ldots;\alpha_{n}\rrbracket_{\mathrm{ DS}}\] \[=\llbracket\tau(\alpha_{n})\rrbracket_{\mathrm{o}}\circ\cdots \circ\llbracket\tau(\alpha_{1})\rrbracket_{\mathrm{o}}\] \[=\llbracket\tau(\alpha_{1})\ltimes\cdots\ltimes\tau(\alpha_{n}) \rrbracket_{\mathrm{o}}\] \[=\llbracket\tau(N)\rrbracket_{\mathrm{o}}\]

As a consequence, the transformation function \(\tau\) can also be inductively defined using the following three atomic TADS

* identity \(\varepsilon\)
* affine functions \(\alpha\colon\mathbb{R}^{n}\to\mathbb{R}^{m}\) where \(n,m\in\mathbb{N}\)
* single ReLUs \(\phi_{i}^{n}\) where \(n,i\in\mathbb{N}\), \(i\leq n\)

which are illustrated in Figure 6.

**6.18 Corollary (Inductive Definition of \(\tau\))**.: _The transformation of a network to a TADS can be defined inductively as_

\[\tau^{\prime}(\varepsilon) =\varepsilon\] \[\tau^{\prime}(\alpha\,;N) =\alpha\ltimes\tau^{\prime}(N)\] \[\tau^{\prime}(\phi_{i}^{k}\,;N) =\left(\vec{e}_{i}^{\top}\!\cdot\vec{x}\geq 0,\mathbf{I}^{k},\mathbf{E} _{i}^{k}\right)\ltimes\tau^{\prime}(N)\]

_such that_

\[\tau^{\prime}(N) =\tau(N).\]

This consistency of viewpoints and operational handling indicates that the TADS setup is natural, and that it supports to approach PLNN analysis and explanation from various perspectives
## 7 TADS at Work

In this section, we continue the discussion of the XOR function as a minimal example to showcase the power of TADS for:

* **Model Explanation.** For a given PLNN, describe precisely its behavior in a comprehensible manner. This allows for a semantic comparison of PLNNs comprising (approximative) semantic equivalence with precise diagnostic information in case of violation.
* **Class Characterization.** PLNNs are frequently extended by the so-called argmax function to be used as classifiers. TADS-based class characterization allows one to precisely characterize the set of inputs that are specifically classified, or the set of inputs where two (PLNN-based) classifier differ.
* **Verification.** Verification is beyond the scope of this section but will be discussed in [20] in the setting of digit recognition.

In the remainder of this section we focus on the impact of Model Explanation and Class Characterization. Two properties of TADS are important here:

**Compositionality.** Due to the compositional nature of TADS, any TADS that represents a given PLNN can be modified and extended by _output interpretation_ mechanisms. This mirrors a very important use case of neural networks; while neural networks are fundamentally functions \(\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\), they are often used for discrete problems which requires a different interpretation of their output.

**Precision.** As the TADS transformation of a PLNN is semantics preserving, all results are precise.

Based on these properties it is possible to solve all the aforementioned problems elegantly by simple algebraic transformations of TADS.

### Model Explanation and Algebraic Implications

To start, we train a small neural network to solve the continuous XOR problem. The resulting network, \(N_{1}\), represents a continuous function \(f_{1}=\llbracket N_{1}\rrbracket_{\text{\tiny DS}}\) (see Figure 6(a)). \(N_{1}\) solves the XOR problem relatively well, with all corners being within a distance of \(<0.1\) to the desired values of \(1\) and \(0\) respectively.

The architecture of \(N_{1}\) is shown in Figure 9. Note that this architecture is much bigger than the architecture for \(N_{*}\) (cf., Section 5). This is needed as the

Figure 5: Example for TADS composition. The TADS (a) and (b) are based on partial ReLUs. TADS (c) is the composition of (a) and (b). Note the difference between _lifting_ (Figure 4) and _composing_ in the inner nodes. The input vector is given as \(\vec{x}=(a,b)\) with \(a,b\in\mathbb{R}\).

Figure 6: A few examples for atomic TADS. The input vector is given as \(\vec{x}=(a,b)\) with \(a,b\in\mathbb{R}\).
training procedure is approximate and does not reach a global optimum. On all substantially smaller networks, we failed to train a network that was close to the specifications of XOR.

#### 7.1.1 Model Explanation

First, we consider full model explanation of \(N_{1}\).11 We can attain a precise and complete characterization of \(f_{1}\) by creating the corresponding TADS \(t_{1}=\tau(N_{1})\) as shown in Figure (a)a. This TADS describes precisely and completely the behavior of \(f_{1}\) in a whitebox manner.

Footnote 11: Of course, in this two-dimensional case a function plot akin to Figure (a)a might seem sufficient, but this is not feasible in anything beyond two-dimensional problems.

Similarly to the function plot shown in Figure (a)a, the TADS gives a comprehensible view of \(f_{1}\).In contrast to the mere function plot, the TADS of Figure (a)a is a solid basis for further systematic analyses and extends to more than two dimensions.

Model Explanation as illustrated here is the basic use case of a TADS as a white-box model for PLNNs, however, the true power of TADS becomes apparent when used for high-level analyses using algebraic operations on TADS.

#### 7.1.2 Algebraic Implications

As mentioned in the last section, the training process of neural networks is approximate and can lead to many different solutions. A very natural question to ask is: "How differently do two neural networks solve the same problem?". This question can be answered using algebraic operations on TADS.

Consider \(N_{2}\), a PLNN that has also been trained with the network architecture shown in Figure 9, but with a different setting of hyperparameters.12 Its represented (semantic) function \(f_{2}=[\![N_{2}]\!]_{\mathrm{DS}}\) is depicted in Figure (b)b and the corresponding TADS \(t_{2}=\tau(N_{2})\) in Figure (b)b.

Footnote 12: The discussion of the learning process is beyond the scope of this paper.

As TADS form a linear algebra, one can easily mirror the computation \(f_{2}-f_{1}\) by \(t_{2}-t_{1}\) on TADS level. The result is identical because the transformation process is precise, i.e.,

\[[\![N_{2}]\!]_{\mathrm{DS}}-[\![N_{1}]\!]_{\mathrm{DS}}=f_{2}-f_{1}=[\![t_{2}- t_{1}]\!]_{\mathrm{\Theta}}\]

The resulting difference TADS \(t_{3}\) is shown in Figure 10 and the corresponding function graph in Figure 11.

\(t_{3}\) is ideal to study the semantic difference between PLNN \(N_{1}\) and\(N_{2}\). Most interestingly, as can be visually seen in Figure 11, the largest differences between both networks occur in the middle of the function domain, i.e., in the region most distant from the edges where the XOR problem is clearly defined. This matches the intuition that points further away from known points are more uncertain under neural network training.

Further, observe that the difference of both networks yields a TADS of roughly double the size. This moderate increase in size indicates the similarity of \(N_{1}\) and \(N_{2}\), as linear regions of the difference TADS \(t_{3}\) result from the intersection of the regions for \(f_{1}\) and \(f_{2}\) which could, in the worst case, grow quadratically.

As mentioned above (cf. Corollary 6.16), it is also possible to analyse \(\epsilon\)-similarity via algebraic operations to, in this case, obtain the TADS shown in Figure 12, which is much smaller than the full difference TADS (cf. Figure 10). The piece-wise affine function of this TADS is visualised in Figure 13.

Figure 7: Function graphs corresponding to the PLNNs \(N_{1}\) and \(N_{2}\). Observe that both PLNNs fulfill the conditions of the XOR problem very closely.
There are 8 regions in which the difference values exceed 0.3, all close to the center of \([0,1]^{2}\). This, again matches the intuition that the volatility of solution grows with the distance to the defined values.

This result is interesting as it shows that, while the two neural networks that we trained differ, they do not differ more than 0.3 except for a small region in the center of the input space. Similar constructions can be used to analyze robustness of neural networks. Robustness of neural networks is of large interest to neural network research [14] and the application of TADS to this problem is discussed in more detail in [13].

### Classification

Applications of neural networks are traditionally split into _regression tasks_ and _classification tasks_. In regression tasks, one seeks to approximate a function with continuous values, whereas classification tasks have dis

Figure 8: TADS corresponding to the PLNNs \(N_{1}\) and \(N_{2}\). Note that both TADS are a full characterization of the semantic functions \(f_{1}\) and \(f_{2}\), respectively.

Figure 9: The architecture of the networks \(N_{1}\) and \(N_{2}\). Weights and biases are omitted for brevity.
crete outputs. As learned, piece-wise linear functions are inherently continuous, classification tasks require an additional step that _interprets_ the continuous output of a neural network as one of multiple discrete classes. Note that this is a change of mindset, with the same neural network being interpreted differently depending on the context.

In our context, one might be interested in a model that classifies each input point \(\vec{x}\in\mathbb{R}^{2}\) as either \(1\) or \(0\) instead of returning a real-value.

#### 7.2.1 Class Characterization

A standard method for classification tasks is the interpretation of neural network outputs as a probability distribution over classes [1]. In our XOR example, it is natural to interpret \(f_{1}(\vec{x})\) as the probability of \(\vec{x}\) belonging to class \(1\) and \(1-f_{1}(\vec{x})\) as the probability of \(\vec{x}\) belonging to class \(0\).

At evaluation time, one might naturally choose the class with the highest probability. Thus, \(N_{1}\)'s output is set to \(1\) if it is greater than \(0.5\) and \(0\) otherwise, which is, actually, in line with the definition of \(g_{*}\). Applying

\[\mathbb{I}(x\geq 0.5)=\begin{cases}1&\text{if }x\geq 0.5\\ 0&\text{otherwise}\end{cases}.\]

to the continuous learned function \(f_{1}\) therefore results in a suitable classifier for this problem:

\[g=\mathbb{I}(x\geq 0.5)\circ f_{1}\]

Note that \(\mathbb{I}(x\geq 0.5)\) is not continuous and therefore cannot be represented by a PLNN.13

Footnote 13: This is a general observation that holds for all discrete valued classification tasks. Most notably, the argmax function, a standard method for n-ary classification, can also not be represented by a PLNN and must be handled on the side of TADS. More discussions on the role of argmax in classification can be found in [13].

To construct the TADS, we use the compositionality of TADS. We manually construct the simple TADS \(\tau(\mathbb{I}(x\geq 0.5))\) as shown in Figure 15 and compose it with the TADS \(t_{1}\) of \(f_{1}\). The resulting TADS

\[t_{1}^{c}=\tau(\mathbb{I}(x\geq 0.5))\Join t_{1}\]

is shown in Figure 13(a). Note that this TADS is reminiscent of a binary decision diagram with just two final nodes. Figure 15(a) and shows precisely which inputs are interpreted as \(1\) and which as \(0\). As we only have two classes here, this classification can be considered as what is called _class characterization_ in [1] for both classes \(0\) and \(1\). Please note that class characterizations allows one to change the perspective from a classification task to the task of finding adequate candidates of specific profile, here given as a corresponding class.

This shows, that, given an output interpretation that maps the continuous network outputs to discrete classes, it is possible to transform neural networks, fundamentally blackbox representations of real valued functions, into semantically equivalent decision diagrams, fundamentally whitebox representations of discrete valued functions.

#### 7.2.2 Comparison of Classifiers

After having constructed TADS that characterize the classification behavior of neural networks, we can also characterize the _difference_ in classification behavior of two neural networks. We can simply do so by using the lifted equality relation to the TADS level and compute the TADS:

\[t_{1}^{c}\ \ \ominus\ t_{2}^{c}\]

The resulting TADS is shown in Figure 16(a) and the corresponding function graph in Figure 15(c). This plot describes precisely the areas where both functions differ and where they coincide.

Notably, it shows that, while the absolute difference of \(f_{1}\) and \(f_{2}\) is highest in the center of the interval \([0,1]^{2}\), the networks agree in that area with respect to classification. Indeed, it appears that the largest difference with respect to classification occurs in the diagonals separating the classes \(1\) and \(0\). This is not too surprising, as it is at the borderline between classes were small changes may affect the classification result.

Using an encoding of boolean values as \(1\) and \(0\) respectively, we can also compute the difference of \(t_{1}^{c}\) and \(t_{2}^{c}\)

\[t_{1}^{c}\ \ \ominus\ t_{2}^{c}\]

This TADS not only describes where \(t_{1}^{c}\) and \(t_{2}^{c}\) disagree, but also how they disagree. The corresponding TADS is shown in Figure 16(b).

This shows the utility of TADS for output interpretation. While the absolute difference between two networks is a suitable measure of difference for _regression_ tasks, the difference of the classification functions is suitable for _classification_. Playing with this difference, e.g., by modifying the classification function, is a powerful analytical instrument. E.g., in settings with many classes, separately analyzing the class characterizations of the individual classes typically leads to much smaller and easier to comprehend TADS and may therefore be a good means to increase scalability.

In machine learning, one often compares learned classifiers to groundtruth solutions by sampling from the
groundtruth solution and checking whether the neural network matches the groundtruth predictions. TADS enable a straightforward and precise way of evaluating a neural network in instances where one has access to the groundtruth model. E.g., the TADS of Figure13 precisely specifies where \(N_{1}\) differs from the baseline solution \(\mathbb{I}(|x-y|\geq 0.5)\).

## 8 Related Work

The presented TADS-based approach towards understanding of neural networks is explicitly meant to bridge between the various existing initiative that aim in the same direction, but typically with quite different means. In this section, we review the state of the art under three perspectives:

* The intent, explainability, as approached in the neural networks community.
* Applied concepts, e.g., symbolic execution that aim at (locally) precise results.
* Applied background, in particular concerning piece-wise affine functions.

Whereas the first perspective (Section8.1) is conceptually distant, both in its applied technologies as well as in its achievements, the mindset of second perspective (Section8.2) is similar in aims and means, but except for our previous work restricts its attention to a locally precise analysis close to some (partly symbolic) input. The third perspective just concerns the mathematical background (Section8.3). We are not aware of any previous work that systematically applies algebraic reasoning to achieve precise explanation and verification results about neural networks.

### Machine Learning Explainability

In recent years, explainable machine learning (XML) as a subfield of machine learning has seen a surge of activity. In line with existing machine learning research, XML focuses on approaches that scale efficiently at the cost of precision and comprehensibility.

Due to vast amount of work in this direction we can only provide sketch of the field here which, from our perspective, is characterized by is use of 'traditional' deep learning technologies such as gradient based optimization and its focus on directly investigating the neural networks themselves in an approximative fashion and without explicit link to some semantic model.

A typical example of a gradient-based method is activation maximization [16, SCD\({}^{+}\)17] which seeks to find, for one class \(C\) and network \(N\), the input \(\vec{x}\) for which \(\llbracket\vec{x}\rrbracket\) is maximal for class \(C\). Being based on gradient based optimization this approach is clear approximate.

Other examples of approaches working on the neural network level are frequently found in attribution methods. Attribution methods focus on attributing a prediction \(\llbracket N\rrbracket(\vec{x})=y\), to parts of the input that one deems responsible for this prediction. In general, this question is unclear and subjective. As a consequence, there exist multiple different methods that attribute the prediction differently to the original input. Examples include gradient based saliency maps [11, 10], layer-wise relevance propagation (LRP) [1] and deep taylor decomposition [11]. As attribution is natural to answer for linear models, these methods focus on linearly approximating the model (gradient based saliency maps) or parts of the model (LRP and deep taylor decomposition). The latter methods depend strongly on the neural network architecture and not on its semantics.

These methods are useful to gain rough intuition, but they do not offer any guarantees or reliable results. This is a direct consequence of most of these methods working with classical machine learning tools such as backpropagation and numerical optimization, which are fast but approximative [1].

The class of XML methods that is most closely related to TADS are local proxy models like LIME [14] and SHAP [10]. Both methods consider one fixed input \(\vec{x}\) and treat the model as a black-box. They observe the model's behavior on multiple perturbations of the form \(\vec{x}+p\) with \(p\) being sampled randomly. Then, they use simple machine learning models such as a linear classifier or a decision tree to describe the model's behavior on the perturbations \(\vec{x}+p\) they observed.

These methods are similar in their intent to the TADS approach as they use conceptually simple models to represent the blackbox behavior of a neural network. However, both LIME and SHAP are imprecise. They both sample only a few points \(\vec{x}+p\) in the neighborhood of \(\vec{x}\) and might miss important properties of the neural network model. Further, both methods use a machine learning classifier to represent these points. These classifiers are usually linear models (or a comparably simple model) and cannot capture the full behavior of the network, which leads to potentially large and uncontrolled errors.

We are not aware of XML methods that provides guarantees strong enough to justify a responsible use in safety critical applications.
### Conceptually Related Work

Symbolic Execution of Neural Networks.More closely related to TADS are approaches to explainability based on symbolic execution of neural networks.

The idea of explainability via symbolic (or rather concolic execution) of neural networks was already explored in the works of [14]. In their work, the authors translate a given PLNN into an imperative program and conoclically execute one given input \(\vec{x}\in\mathbb{R}^{n}\). This corresponds to exploring the one path of a TADS corresponding to \(\vec{x}\). This yields the path condition and the affine transformation that are responsible for the prediction \(\mathcal{N}(\vec{x})\). The authors further use these explanations to find adversarial examples and find parts of an input that they deem important for a given classification. The results of this work are promising, but (very) local, as they restrict themselves to one linear region of the input.

The authors of [1] propose a method that closely mirrors the method of [14]. In essence, both methods are almost identical but differ in their conceptual derivation of the method. The authors of [1] also consider sets of predictions and work out what features act as discriminators in many of these predictions.

Moving from the idea of explanation, the authors of [14] consider concolic testing instead. Similar to the work of [14], they execute singular inputs conoclically. They use the results from concolic execution to heuristically derive new inputs that cover large areas of the input space.

TADS improve on these approaches in two ways. First, TADS offer a global viewpoint on neural network semantics, independent of a sample set. Second, TADS support algebraic operations on a conceptual level to derive globally precise explanation and verification results. As illustrated in Section7 algebraic operations nicely serve as a toolbox to derive tailored and precise analyses.

Neural Network Verification.Neural network verification aims to verify properties of neural networks, usually piece-wise linear neural networks using techniques from SMT-solving and abstract interpretation extended by domain specific techniques [15, 16, 17]. Verification approaches are usually precise or at least provide a counterexample if a property is shown false. Modern solvers can scale quite well but are still far from being able to tackle practically relevant application [1].

Verification approaches are related to TADS as they also provide tools for the precise analysis of piece-wise linear neural networks. However, while SMT-based verification approaches currently scale better than TADS, they focus only on binary answers to a verification problem. They are not able to provide full diagnostics and descriptions of where and how an error occurs. However, please note, SMT-based approaches should not be considered as an alternative but rather as a provider of technologies that can also be applied at the TADS level. In fact, we use SMT solving, e.g., to eliminate infeasible paths in TADS.

Precise Explainability of Random Forests.This work is conceptually closely related to and builds upon the work of [14, 15]. There, ADDs are used and extended to derive explainable global models for random forests. Similar to the approach in this paper, these models are derived through a sequence of semantics-preserving transformations and later on refined by performing algebraic operations on the white-box representation of random forests. In fact, considering the underlying mindset, the work in this paper can be regarded as an extension of our work on random forest to neural networks. However, the much higher complexity of PLNN requires substantial generalization which, to our surprise, did not clutter the theory, but rather added to its elegance.

### Technologically Related Work

Linear Regions of Neural Networks.Vast amounts of research have been conducted regarding the number and shape of linear regions in a given PLNN [11, 12, 13, 14, 15, 16, 17, 18, 19, 18, 19, 18, 17, 20, 16]. Linear regions are of huge interest to neural network research as they give a natural characterization of the expressive power of neural network classes. This research is beneficial to the understanding of TADS as it can be used to bound the size of TADS and understand where and when explosions and size occur. On the other hand, TADS give a precise and minimal representation of the linear regions belonging to given neural network and can be used to facilitate experiments in this field, e.g., to find a linear region containing a negative example for a given property that could not be verified [15].

Structures for Polyhedral Sets.At their core, TADS are efficient representations of multiple polyhedral regions within high dimensional spaces. Similar problems occur in other divisions of computer science, most notably computer graphics.
TADS are closely related to Binary Space Partition Trees (BSP-trees) [17] and comparable structures [16]. These structures are built to represent a partition of a real-dimensional space into polygons much like TADS do. TADS extend these structures with optimizations from ADDs to account for domain specific properties of piece-wise linear functions that are not present in the general case of polygonal partitions.

## 9 Conclusion and Future Work

We have presented an algebraic approach to the precise and global explanation of Rectifier Neural Networks (PLNNs), one of the most popular kinds of Neural Networks. Key to our approach is the symbolic execution of these networks that allows the construction of semantically equivalent _Typed Affine Decision Structures_ (TADS). Due to their deterministic and sequential nature, TADS can be considered as white-box models and therefore as precise solutions to the model explanation problem, which directly imposes also solutions to the outcome explanation, and class characterization problems [11, 12]. Moreover, as linear algebras, TADS support operations that allows one to elegantly compare Rectifier Networks for equivalence or \(\epsilon\)-similarity, both with precise diagnostic information in case of failure, and to characterize their classification potential by precisely characterizing the set of inputs that are specifically classified or the set of inputs where two Network-based classifiers differ. These are steps towards a more rigorous understanding of Neural Networks that is required when applying them in safety-critical domains without the possibility of human interference such as self-driving cars.

This elegant situation at the semantic TADS level is in contrast with today's practical reality where people directly work with learned PLNNs that are, in particular, characterized by their hidden layers that often comprise millions sometimes even billions of parameters. The reason for this complex structure is learning efficiency, a property paid for with semantic intractability: There is essentially no way to control the impact of minor changes of a parameter or input values, and even the mere evaluation for a sample input exceed the capacity of a human's mind by far. This is why PLNNs are considered as black-box models.

The reason why TADS have not yet been studied may be due to their size: they may be exponentially larger than a corresponding PLNN. The reason for this expansion is the transformation of the incomprehensible hidden layers structure into a large decision structure, which, conceptually, is as easy to comprehend as a decision tree and a linear classifier. In this sense, our transformation into TADS can be regarded as trade of size for transparency, turning the verification and explanation problem into a scalability issue. There are at least three promising angles for attacking the scalability problem:

1. Learned PLNN have a high amount of noise resulting from the underlying learning process that works by locally optimizing individual parameters of the hidden layers. Noise reduction may have a major impact on size. Detecting noise is clearly a semantic task and can therefore profit from TADS-based semantic analyses.
2. PLNN are accepted to be approximative. Thus controlled modifications with minor semantic impact are easily tolerated. TADS provide the means to control the effect of modifications and thereby to keep modifications in the tolerable range.
3. Modern neural network architectures are typically compositions of multiple sub-networks that are intended to support the learning of different subtasks. However, this structure at the representational layer gets semantically blurred during joint the learning process which, e.g., prohibits compositional approaches as known from formal methods. The semantic transparency of TADS may provide means to reinforce the intended compositional structure also at the semantical level in order to support compositional reasoning and incremental construction.

Of course, there seems to be a hen/egg problem here. If we can construct the TADS, we are able to reduce it in order to achieve scalability. On the other hand, we need scalability first to construct the TADS. This is a well-known problem in the formal methods world, and, despite a wealth of heuristics and domain-specific technologies, the answer is _compositionality_ and _incremental construction_. This is exactly in line with the observation reported in the third item above: We need to learn how to use divide and conquer techniques for PLNN in a semantics-aware fashion. TADS are designed to support this quest by providing both a leading mindset and a tool-supported technology.
