# Detecting Information Relays in Deep Neural Networks

Arend Hintze  Department of MicroData Analytics, Dalarna University, Sweden
BEACON Center for the Study of Evolution in Action<EMAIL_ADDRESS>Christoph Adami
BEACON Center for the Study of Evolution in Action  Department of Microbiology
and Molecular Genetics  Program in Evolution, Ecology, and Behavior, Michigan
State University, United States of America

###### Abstract

Deep-learning of artificial neural networks (ANNs) is creating highly
functional tools that are, unfortunately, as hard to interpret as their
natural counterparts. While it is possible to identify functional modules in
natural brains using technologies such as fMRI, we do not have at our disposal
similarly robust methods for artificial neural networks. Ideally,
understanding which parts of an artificial neural network perform what
function might help us to address a number of vexing problems in ANN research,
such as catastrophic forgetting and overfitting. Furthermore, revealing a
network’s modularity could improve our trust in them by making these black
boxes more transparent. Here we introduce a new information-theoretic concept
that proves useful in understanding and analyzing a network’s functional
modularity: the relay information $I_{R}$. The relay information measures how
much information groups of neurons that participate in a particular function
(modules) relay from inputs to outputs. Combined with a greedy search
algorithm, relay information can be used to identify computational modules in
neural networks. We also show that the functionality of modules correlates
with the amount of relay information they carry.

##  1 Introduction

Neural networks, be they natural or artificial deep-learned ones, notoriously
are black boxes [9, 1]. To understand how groups of neurons perform
computations, to obtain insight into the algorithms of the human mind, or to
be able to trust artificial systems, we need to make the network’s processing
more transparent. To this end, various information-theoretic and other methods
have been developed to shed light on the inner workings of neural networks.
Transfer entropy [32] seeks to identify how much information is transferred
from one node (or neuron) to the next, which in principle can detect causal
links in a network [2] or be used to understand general properties about how
information is distributed among nodes [36, 18]. In general, information
theory can be used to make inferences in cognitive- and neuroscience [27, 11,
37]. Predictive information [4, 3] determines how much the outputs of a neural
network depend on the inputs to the system or on hidden states. Integrated
information [38] quantifies how much a system combines inputs into a single
experience and identifies the central component(s) in which that happens.
Information theory is also used to determine cognitive control [12] and neural
coding [7] in natural systems. Finally, information theory is used to
characterize representations [25] that quantify how much (and where)
information is stored about the environment.

In spite of this diversity of applications of information theory to neuronal
networks, the question of which module or subset of nodes in an artificial
neural network performs which function remains open. In cognitive or
neuroscience, this question is often answered using functional magnetic
resonance imaging (fMRI) [24]. This method identifies functional cortical
areas by their oxygen-consumption increase required to perform a particular
task (an approach that does not require information theory). In deep
convolutional neural networks, such an approach is impossible for obvious
reasons. One approach is to determine the degree of modularity from the
weights that connect nodes [35], by determining how compartmentalized
information is [16, 21], or by performing a knockout analysis that allows
tasks to be associated with the processing nodes of the neural network [8].
However, results from such a knockout analysis are often not conclusive.

Neural networks trained via backpropagation are unlikely to be modular since
this training method recruits all weights into the task trained [17].
Similarly, dropout regularization [15] is believed to cause all weights to be
involved in solving a task (making the neural network more robust), which in
turn prevents overfitting. Consequently, information is expected to be spread
out among nodes rather than compartmentalized in specific groups. This lack of
compartmentalization is believed to be the cause of catastrophic forgetting
[26, 13], where a network trained on one task can achieve high performance,
but the moment the network is sequentially trained on a new task the
performance of the network when tested on the old task drops catastrophically.

While many methods seek to prevent catastrophic forgetting [29], such as
Elastic Weight Consolidation (EWC) [22], algorithms such as LIME [31], and
even replay during sleep [14], it is still argued that catastrophic forgetting
has not been solved [19]. If catastrophic forgetting is due to a lack of
modularization of information, it becomes crucial to accurately measure this
modularization to identify learning schemes that promote modules. The problem
of identifying modules responsible for different functions is further
aggravated when information theory and perturbation analysis (via node
knockout) disagree [5, 33].

When identifying candidate neurons in hidden layers that might contain
information about the inputs that are used in decision-making, perturbing
those neurons by noise or knockout should disrupt function. Similarly, hidden
nodes not containing information about inputs should, when perturbed in this
manner, not alter the outputs encoding decisions. However, if information is
stored redundantly, perturbing only part of the redundant nodes will not
necessarily disrupt function, even though they carry information. At the same
time, nodes without function or information can still accidentally perturb
outputs when experiencing noise [5, 33].

Here we develop a new information-theoretic measure that quantifies how much
information a set of nodes relays between inputs and outputs (relay
information $I_{R}$). This measure can be applied to all combinations of
neurons (sets) to identify which set of a given size contains the most
information. While the number of sets of neurons is exponential in size, the
number of tests required to find the set with the largest amount of
information can be significantly reduced by taking advantage of the fact that
a smaller subset cannot have more information than its superset. Thus, this
measure can be combined with a greedy search algorithm that identifies the
relevant computational modules connecting the inputs to the outputs. We will
demonstrate on a wide range of examples the function and applicability of this
new method. Specifically, using a positive control in which the nodes relaying
the information from inputs to outputs are known, we demonstrate that relay
information indeed allows us to recover the relevant functional nodes. We
compare this control to a regularly-trained neural network, and show that
perturbations on nodes carrying relay information indeed cause failures in
their predicted functionality.

##  2 Methods

###  2.1 Training Artificial Neural Networks

The neural networks used here are implemented using PyTorch [30] and trained
on the MNIST handwritten numerals dataset [23]. The MNIST dataset consists of
60,000 training images and 10,000 test images of the ten numerals 0-9. Each
grey-scale image has $28\times 28$ pixels with values normalized between
$-1.0$ to $1.0$. Here we use two different networks. The full network has 784
input nodes, followed by a layer of 20 hidden nodes with a standard summation
aggregation function, and a $\tanh$ threshold function. The output layer needs
10 nodes to account for the ten possible numeral classes and uses the same
aggregation and threshold function as the hidden layer. The composite network
is an aggregate of ten sub-networks each trained to recognize only a single
number. In each of the sub-networks, the hidden layer has two nodes, with a
single node in the output layer.

Networks are trained using the Adam optimizer [20] until they either reach a
recognition accuracy of 95% or else reach a given fixed number of training
epochs. The node in the output layer with the highest activation is used to
indicate the network’s prediction of the numeral depicted in the image (argmax
function).

###  2.2 Composing an Artificial Neural Network from smaller ones

In a typical ANN performing the MNIST classification task, all nodes of the
hidden layer are involved in relaying the information from the input to the
output layer: a phenomenon we previously termed informational smearing [16] as
the information is “smeared” over many neurons as opposed to being localized
to one or a few neurons. Our control network is constructed in such a manner
that functionality is strictly distributed to very specific nodes.
Specifically, we construct a network with 20 hidden nodes by aggregating ten
sub-networks with two hidden nodes each. Each of the sub-networks is only
trained to recognize a single numeral amongst the background of the other
nine, using only two hidden nodes. By combining these 10 sub-networks networks
into the composite model, we can create a control in which the relay neurons
(the two hidden neurons in each of the sub-networks) are guaranteed to only
relay information about a very specific function (see Figure 1).

Figure 1: Illustration of the composite network. For each of the ten numerals,
an independent neural network (sub-network) is trained to recognize a single
numeral among the others. Each of those ten networks has 784 input nodes to
receive data from the $28\times 28$ pixel-wide MNIST images. Each hidden layer
has two nodes followed by a single node at the output layer (top panel). The
composite network (bottom panel) is assembled from these ten subnetworks.
Colors represent which weights in the combined weight matrix come from which
corresponding sub-network. Weights shown as white remain $0.0$. Consequently,
the weight matrix connecting the hidden layer to the output layer is de facto
sparse.

###  2.3 Information-theoretic Measure of Computational Modules

An artificial neural network can be viewed as an information-theoretic channel
[34] that relays the information received at the input layer to the output
layer while performing some computations along the way. To measure the
throughput of information, define the random variable $X_{\rm in}$ with ten
states (one for each numeral) and Shannon entropy $H(X_{\rm in})$, while the
outputs form a random variable $X_{\rm out}$ with entropy $H(X_{\rm out})$.
The mutual information between both $I(X_{\rm in};X_{\rm out})$ [see Eq. (1)]
consequently measures how much the output symbol distribution is determined by
the inputs (and vice versa, as this is an un-directed measurement).

$I(X_{\rm in};X_{\rm out})=H(X_{\rm in})+H(X_{\rm out})-H(X_{\rm out},X_{\rm
in})$ (1)

Here, $H(X_{\rm out},X_{\rm in})$ stands for the joint entropy of the input
and output variables.

At the initialization of the network, weights are randomly seeded, giving rise
to a network that randomly classifies images. In this case, the confusion
matrix is relatively uniform and the conditional entropy $H(X_{\rm out}|X_{\rm
in})=H(X_{\rm out},X_{\rm in})-H(X_{\rm in})\approx H(X_{\rm out})$, leading
to low information $I(X_{\rm in};X_{\rm out})$. However, over the course of
training the prediction accuracy increases, leading ultimately to a strictly
diagonal confusion matrix and a vanishing conditional entropy $H(X_{\rm
out}|X_{\rm in})$, implying that every numeral is properly classified. In this
case the information channel has maximal information (information equals
capacity) when measured over the training or test set.

We can view this joint channel as being composed of two sequential channels:
one from the inputs to the hidden states, and one from the hidden states to
the outputs. The information that the outputs receive is still determined by
the inputs, but now via the hidden variable $Y$. A perfect channel can only
exist if the hidden layer has sufficient bandwidth to transmit all of the
entropy present at the inputs, that is $H(Y)\geq H(X_{\rm in})$.

We can now write the information that flows from the inputs via the hidden
states to the outputs in terms of the shared information between all three
random variables

$\displaystyle I(X_{\rm in};X_{\rm out};Y)$ $\displaystyle=$ $\displaystyle
H(X_{\rm in})+H(X_{\rm out})+H(Y)$ (2) $\displaystyle-$ $\displaystyle
H(X_{\rm in},X_{\rm out})-H(X_{\rm in},Y)-H(X_{\rm out},Y)$ $\displaystyle+$
$\displaystyle H(X_{\rm in},X_{\rm out},Y)\;.$

Because information must pass through the hidden layer, this “triplet
information” must be equal to the information $I(X_{\rm in};X_{\rm out})$ (see
Fig. 2).

Figure 2: Entropy Venn diagram for the random variables $X_{\rm in}$, $X_{\rm
out}$, and $Y$. The shared information between all three variables equals the
information $I(X_{\rm in};X_{\rm out})$ because no information can flow from
$X_{\rm in}$ to $X_{\rm out}$ without passing through $Y$.

However, in general not all the nodes that comprise $Y$ carry information. Let
us imagine for example that the set of hidden nodes $Y$ is composed of a set
$Y_{R}$ that shares information with $X_{\rm in}$ and $X_{\rm out}$, and a set
$Y_{0}$ that does not share this information, that is, $I(X_{\rm in};X_{\rm
out};Y_{0})=0$, with $Y=Y_{R}\otimes Y_{0}$. We will discuss the algorithm to
determine which neurons belong in the set of relay neurons $\mathbb{Y_{R}}$
further below.

Figure 3: A: Input/output structure of an ANN with inputs $X_{\rm in}$,
outputs $X_{\rm out}$, and a hidden layer $Y=Y_{R}\otimes Y_{0}$. The relay
information passes from the inputs via the relay neurons $Y_{R}$ to the output
(green arrow). B: The Venn diagram for the four variables $X_{\rm in}$,
$X_{\rm out}$, $Y_{R}$, and $Y_{0}$, with ellipses quantifying the entropy of
each of the variables colored according to panel A. The information shared
between $X_{\rm in}$ and $X_{\rm out}$ is outlined in yellow. The relay
information Eq. (3) is indicated by the green area.

The nodes that comprise $Y_{0}$ could, for example, have zero-weight
connections to the inputs, the outputs, or both. They are defined in such a
way that none of the information $I(X_{\rm in};X_{\rm out})$ (area outlined in
yellow in Fig. 3B) is shared with them.

We call the information that is relayed through the “critical” nodes that
carry the information (the nodes in the set $Y_{R}$) the relay information.
While we could define this information simply as the information shared
between $X_{\rm in}$ that is also shared with the neurons identified to be in
the set of $\mathbb{Y_{R}}$ (see section 2.4), it is important to deal with
cases where neurons that are informationally inert (they do not read
information from $X_{\rm in}$ nor write into $X_{\rm out}$) could nevertheless
copy the state of a neuron that does relay information. As discussed in
Appendix A, such neurons may be classified as belonging to the set
$\mathbb{Y}_{0}$ (because removing them does not reduce the information
carried by the set) yet show a nonvanishing $I(X_{\rm in};X_{\rm out};Y_{0})$
since they are copying a neuron in $Y_{R}$. In order to eliminate such
contributions, we measure the relay information conditional on the state of
neurons in $Y_{0}$, that is

$I_{R}=H(X_{\rm in};X_{\rm out};Y_{R}|Y_{0})\;,$ (3)

which is indicated in the entropic Venn diagram in Fig. 3 as the area colored
in green. An explicit expression for $I_{R}$ can be obtained simply by writing
Eq. (2) for $Y_{R}$ instead of $Y$, and conditioning every term on $Y_{0}$.

The removal of hidden neurons that do not contribute to information transfer
suggests a simple algorithm that identifies such neurons: start with the full
set and remove neurons one-by-one, and keep only those neurons that lead to a
reduction of the information being relayed. However, this search is in reality
more complex because neurons can carry redundant information. We discuss this
algorithm in the following section.

###  2.4 Shrinking Subset Aggregation Algorithm

In order to find the minimal subset of nodes $\mathbb{Y}_{R}$ that carry all
of the information flowing from $X_{\rm in}$ to $X_{\rm out}$, we should in
principle test all possible bi-partitions of neurons in $Y$. It is not
necessary to test all possible partitions, because we discuss each feature in
$X_{\rm out}$ (here, each numeral) separately, that is, either a group carries
information about this feature, or it does not.

Unfortunately, the number of bi-partitions of a set is still exponential in
the set size, so a complete enumeration can only be performed efficiently for
small sets. However, it turns out that in most cases a greedy algorithm that
removes nodes one-by-one will find the minimal set $\mathbb{Y}_{R}$ (see
Appendix A).

We start with the largest partition in which all nodes belong to the set
$\mathbb{Y}_{R}$, and none to $\mathbb{Y}_{0}$. Now all possible subsets in
which a single node is moved from $\mathbb{Y}_{R}$ to $\mathbb{Y}_{0}$ can be
tested. The subset with the highest information [Equation (3)] is retained,
and the node with the lowest information contribution is permanently moved
into subset $\mathbb{Y}_{0}$. This process is repeated until only one node is
left in $\mathbb{Y}_{R}$. Over the course of this procedure (assuming perfect
estimation of entropy from sample data), the set with the highest information
for each set size should be identified (see Algorithm 1).

Algorithm 1 Shrinking Subset Aggregation Algorithm

$\mathbb{Y}=\\{0,...,n\\}$

$\mathbb{Y}_{0}\leftarrow\emptyset$

$\mathbb{Y}_{R}\leftarrow\mathbb{Y}$

while $\mathbb{Y}_{R}\neq\emptyset$ do

for $\forall a\in\mathbb{Y}_{R}$ do

$\mathbb{Y}_{R}^{\prime}\leftarrow\mathbb{Y}_{R}-{a}$

$\mathbb{Y}_{0}^{\prime}\leftarrow\mathbb{Y}_{0}+{a}$

$I_{a}\leftarrow I_{R}(X_{\rm in};X_{\rm
out};\mathbb{Y}_{R}^{\prime}|\mathbb{Y}_{0})$ (see Equation 3)

end for

$a\leftarrow\\{\mathbb{Y}_{R};a=min(I_{a})\\}$

$\mathbb{Y}_{R}\leftarrow\mathbb{Y}_{R}-{a}$

$\mathbb{Y}_{0}\leftarrow\mathbb{Y}_{0}+{a}$

end while

As discussed in Appendix A, this algorithm can sometimes fail to identify the
correct minimal subset. First, estimates of entropies from finite ensembles
can be inaccurate: these estimates are both noisy and biased (see, for
example, [28]), leading to the removal of the wrong node from the set
$\mathbb{Y}_{R}$. Second, information can be stored redundantly. Imagine a
network of ten nodes, with three nodes forming the relay between inputs and
outputs, while another set of two nodes is redundant with those other three
nodes. The greedy algorithm will work until all those five nodes are in the
set $\mathbb{Y}_{R}$. Removing any of those nodes will not drop the
information content of the larger set, since the information is fully and
redundantly contained in both the set of three and the set of two. Thus, all
five nodes appear equally unimportant to the algorithm, which can now not
decide anymore which node to remove. It might remove one of the nodes in the
set of three, leading to the set of two becoming the crucial computational
module. Alternatively, removing a node from the smaller set promotes the
larger set to become the crucial computational set. Either way, the algorithm
has a chance to fail to find a unique set because there could be several.

One way to amend the algorithm would be to allow the process to dynamically
branch. In case multiple nodes upon removal do not reduce the information
retained in the remaining set $\mathbb{Y}_{R}$, all possible branches can be
pursued. Such a fix will significantly increase the computational time.
However, as we do not expect the occurrence of redundant sets to be a
prominent feature of many networks, we have not explored this alternative
algorithm further.

###  2.5 Knockout Analysis

To test the informational relevance of individual nodes of the hidden layer,
we can perform “knockout” experiments. To “knock out” a node (to render it
non-functional), a node in the hidden layer is forced to take on a value of
$0.0$ during the forward pass. At the same time, all weights of the first
layer leading to such a node are set to $0.0$, as are all weights of the
second layer that are affected by that node. Alternatively, the values of the
nodes to be knocked out in the hidden layer could have been forced to $0.0$
when the forward pass reaches the hidden layer. These methods are equivalent.

###  2.6 Binning

The computations performed by the neural network use continuous inputs, and
due to the $\tanh$-like threshold function the activation levels of neurons in
the hidden layer are confined to the interval $[-1,1]$. While entropies can be
computed on continuous variables (so-called differential entropies, see [34]),
we here use discrete entropies, which requires a discretization of the
continuous values. In particular, we are mapping all continuous values to the
binary categories $0$ and $1$. We previously used the median value of a
neuron’s excitation level as the threshold for the bin [6]. Instead, here the
hidden-state values are clustered using a $k$-means clustering algorithm with
$k=2$. Using the median for binning ensures that the resulting distribution
has maximal entropy because one can assume that each bin receives half of the
values. However, we often found that a maximum-entropy assumption for a neuron
to be inappropriate. Using a $k$-means clustering algorithm to distribute
values into bins gives a better approximation of the relative entropy between
states.

###  2.7 Aggregated relay information

The greedy algorithm identifies a sequence of sets of nodes that continuously
shrink because it is always the node contributing the least to $I_{R}$ that is
removed next. Consequently, every time a node is removed, we can also quantify
the loss of information for that particular node $n$ as the difference in
$I_{R}$ between the larger set containing the node $\mathbb{Y}_{R}\cup n$ and
smaller set without it $\mathbb{Y}_{R}$ [see Eq. (4)]:

$\Delta I(n)=I_{R}(\mathbb{Y}_{R}\cup n)-I_{R}(\mathbb{Y}_{R})$ (4)

Interestingly, when this process arrives at a set of nodes that taken together
are essential in relaying the information, it can happen that the removal of
any of the nodes of the set causes the remaining neurons to have $I_{R}=0$.
Information in such an essential set can be seen to be encrypted, to the point
where no node can be removed without loosing all information [5]. However,
this creates a situation in which the last nodes, when removed, appear to not
contribute any information, even tough they are essential.

Thus, we quantify the amount that each node contributes to the relay
information in terms of the sum of all $\Delta I_{R}$ over all previously
removed nodes as

$I_{A}=\sum^{n}\Delta I(n)\;.$ (5)

Using the information loss due to the removal of a node from the essential
set, we can also quantify the essentiality of a neuron in terms of the loss of
information the removal of node $n$ causes when it is removed from the
remaining set of nodes. If a neuron is meaningless or redundant, $\Delta I(n)$
will vanish.

##  3 Results

###  3.1 Identification of Information Relays

To determine if the proposed metric and optimization method correctly
identifies the nodes that relay information from the outputs to the inputs, we
trained two kinds of networks. A standard ANN with 20 hidden nodes was trained
to correctly identify all ten numerals. As a control, ten sub-networks with
two hidden nodes were trained on a single numeral each. From the ten smaller
networks, a full network was composed (see Figure 1) that can perform the same
task as the network trained on all numerals at the same time.

Figure 4: Training accuracy as a function of training epoch. (A): Full model
(top panel). The accuracy to predict each numeral is indicated with lines of
different colors (see legend). Accuracy on the training set is shown as solid
lines while accuracy on the test is indicated by dotted lines. The average
performance classifying all numbers is shown in black.(B): Accuracy of each of
the ten sub-network models used to create the composite model as a function of
training epoch. Colors indicate the accuracy for detecting an individual
number. Training other networks had marginally different outcomes (data not
shown).

Figure 4 shows the mean accuracy of recognizing each of the different digits
as a function of training epoch, for the full as well as the composite
network. Note that the full network only needed 43 epochs to reach 96%
accuracy, while the training of the smaller models took significantly longer.
The full model was trained until it reached an accuracy of 0.96, the smaller
models were trained until they reach an accuracy of 0.98. Smaller networks
could easily be trained to achieve this high 98% accuracy while training the
full network is usually limited to 96%. In order to observe networks
performing as optimally as possible, and to maximize the information between
inputs and outputs, networks were trained until they reached those practical
limits [10].

Because in the composite network the two hidden neurons of each sub-network
are guaranteed to serve as relays for the relevant information, we can use
this network as a positive control to test whether our algorithm correctly
detects relay information, and whether neurons carrying non-overlapping
information (each of the hidden neuron sets only carry the information about
one specific numeral) are either more or less vulnerable to knockout.

In order to test whether the greedy algorithm finds the correct minimal
informative subset in the full model, we performed an exhaustive search of all
$(2^{N})-1$ (with $N=20$) bi-partitions of the hidden nodes to find the
minimal set. We then compared the result of the exhaustive search with the
candidate set resulting from the shrinking subset aggregation algorithm. This
algorithm, if not implementing as a branching algorithm, only needs
$\frac{N(N+1)}{2}$ computations, reducing the computational complexity from
exponential to quadratic.

Figure 5 shows that different partitions contain very different amounts of
information about the output. In general, the larger the set $\mathbb{Y}_{R}$,
the more information it represents, but we also see that the highest
information found within sets of a particular size is always higher than the
maximal information found amongst all sets that are smaller (as proved in
Appendix A, with the caveat of redundant sets). The shrinking subset
aggregation algorithm exploits this observation of smaller sets always having
less information than their larger superset and is capable of identifying the
subsets $\mathbb{Y}_{R}$ (and consequently also $\mathbb{Y}_{0}$) with the
highest information content for all sets of the same size, but without the
complete enumeration of all possible sets. We find that fewer than 0.9% of the
correct sets have equal or more information than the set identified by the
greedy algorithm. As discussed earlier, the failure of the greedy algorithm to
correctly identify the most informative set can be attributed to noise in the
entropy estimate due to the finite sample size, as well as to the presence of
redundant sets with identical information content.

Figure 5: Information content in all possible bi-partitions (black dots), for
different set sizes. Top ten panels show relay information for the full model,
while the bottom ten panels show the same for the composite model. Each panel
shows relay information about a different numeral in the MNIST task, indicated
by the index of the panel. The red line corresponds to the set identified by
the shrinking subset aggregation algorithm. Fewer than 0.9% of all subsets
have a higher information content then the one identified by the algorithm.
The top panel for the composed, the bottom panel for the regularly trained
neural network.

We now investigate whether the greedy algorithm properly identifies the
relevant subsets that are critical in relaying the information from inputs to
outputs, that is, whether the information they carry is indeed used to predict
the depicted numeral. We define the importance of a node as the sum of all
information loss that this node conveyed before it was removed (aggregated
relay information, see Methods).

Figure 6A shows that both the importance analysis (via the aggregated relay
information) and the essentiality analysis identify the proper nodes that
relay the information from inputs to outputs in the composite model that
serves as the positive control. Aside from the sampling noise, each pair of
hidden nodes that were trained to be the relays correctly show up as carrying
high information (see Figure 6). The nodes identified as relays are also
essential, because moving either from $\mathbb{Y}_{R}$ to $\mathbb{Y}_{0}$
coincides with a loss of information (see Figure 6 B).

Figure 6: A: the aggregated information loss $\Delta I(a)$ for all possible 20
nodes ($x$-axis) and the ten different numeral classes ($y$-axis) shown in
gray scale (brighter shades indicate higher loss of information. B: Node
essentiality for each hidden neuron and numeral. Bright squares indicate
essential nodes, while black squares would indicate redundant or meaningless
nodes. The red dot (node 16, numeral 1), points to a neuron that appears to
relay information (panel A), but is entirely redundant (red dot in panel B).

Training the full network via backpropagation is not expected to create
modules of hidden nodes that each only relay information about one specific
numeral. Indeed, we find information to be relayed in an unstructured fashion
in this network (see Figure 7 A). Interestingly, nodes that are positively
identified as relays do not necessarily seem to be essential, suggesting that
many nodes contain redundant information. (see Figure 7 B). This further
supports our previous findings that backpropagation smears or distributes
function across all nodes rather that isolating functions into structured
modules [16, 21].

Figure 7: Aggregated relay information A) and essentiality B) for each node
and every numeral class for a regularly trained network (full network). The
same methods and axis were used as in Figure 6.

###  3.2 Information Relays are critical for the function of the Neural
Network

To verify that the sets $\mathbb{Y}_{R}$ with high information are indeed
relaying information from the inputs to the outputs, we can study the effect
of knock-outs on those nodes. Because we expect a correlation between knock-
out-effect size (the sensitivity of the node to perturbation) and the size of
the informative set, care must be taken when interpreting the correlation
between relay information and knock-out-effect size (sensitivity). Smaller
sets can relay less information and have a potentially smaller effect when
knocked out. We performed a multiple regression to test if a correlation
between the knockout effect and the information content within each set goes
beyond the correlation between both due to the confounding set size. Figure 8)
shows the result of an ANOVA that for all numerals and for both models (full
and composite). The correlation coefficient between sensitivity and set size
(Fig 8A) is about half (or smaller) the correlation coefficient between
sensitivity and relay information, suggesting that the nodes relaying the
information about the numeral indeed contribute in an essential manner to
function. For all computations, the ANOVA found vanishing $p$-values and high
$t$-statistics, further supporting the finding that while set size correlates
with the knockout effect, the knockout effect is explained better by the
information content of the set.

Figure 8: Correlation coefficients for the multiple regression analysis
between he knockout effect ($K$) for each set analyzed is explained by a
summation of the set size ($S$) and the information content ($I$). The
correlation between effect size and set size $S$ is in red, while the
correlartion between effect size and relay information is in black. A: Full
model, B: composite model.

##  4 Discussion

We introduced a new information-theoretic concept: the “relay information”. It
quantifies the amount of information within a set of nodes inside a
communication channel that passes through this set, and not through other
nodes within the same channel. Relay information can be used to identify which
nodes in a hidden layer of a neural network are responsible for what
classification function. We constructed a greedy algorithm that identifies the
minimal informative set of nodes that carry the relay information, and tested
it on the MNIST hand-written numeral classification task using a regular
neural network, as well as a control in another network in which we know–by
construction–the function of each hidden node. We further showed with a
knockout analysis that the identified sets indeed are functional.

The concepts and methods we introduced are general and can be applied to any
task where a network (be it neurtal or genetic) performs its function by
taking inputs, computing outputs, and then using those outputs for prediction.
In the future, it would be interesting to study if this method also applies
to, for example, time series classification, recurrent neural networks,
convolutional layers, or even generative tasks.

In this work We only studied a specific optimizer (ADAM), loss function (mean
squared error), and threshold function (hyperbolic tangent and argmax). We
conjecture that our method applies to all other variances of deep learning.
However, we also conjecture that the way in which information is distributed
across the network will depend on the method and parameters of the
optimization procedure, and will test this dependence in future work. Finally,
by testing different discretizations of neuronal firing levels, the method
should be able identify relay neurons and thus functional modules in
biological brains, and thus help in studying information flow in functioning
brains.

In this work we found that the greedy algorithm correctly identifies the
minimal informative set in almost all cases. However, we expect that the
failure rate depends on the task being studied, the data set size as well as
the amount of redundancy among neurons. In networks with significant
redundancy, we can imagine that the algorithm fails significantly more often,
in which case a branching algorithm may have to be designed, which would carry
a significant complexity cost.

Author Contributions
AH implemented all computational analysis and methods, AH and CA designed the
experiments and devised the new methods, CA proved the SSA algorithm soundness
in the case of no redundant information. AH and CA wrote the manuscript.

Data Availability
The code for the computational experiments and the data analysis will be made
available upon acceptance of the manuscript on github.

Acknowledgements
We thank Clifford Bohm for extensive discussions. This research was supported
by Uppsala Multidisciplinary Center for Advanced Computational Science SNIC
2020-15-48, and the National Science Foundation No. DBI-0939454 BEACON Center
for the Study of Evolution in Action.

## Appendix A

Here we show that as long as information is not redundantly encoded, it is
possible to remove nodes one-by-one in a greedy fashion so that the minimal
information reduction by single-node-removal is not deceptive. In a deceptive
removal, removing a pair of nodes reduces the information by a smaller amount
than each of the individuals would have removed.

Say the information to predict feature $X_{\rm out}$ is stored in $n$
variables $Y_{1}\cdots Y_{n}$. This information is

$\displaystyle I(X_{\rm out};Y_{1}\cdots Y_{n})\;.$ (6)

The general rule to study node removal is the identity

$\displaystyle I(X_{\rm out};Y_{1}\cdots Y_{n})=I(X;Y_{1}\cdots
Y_{n-1})+H(X_{\rm out};Y_{n}|Y_{1}\cdots Y_{n-1})\;.$ (7)

We can easily convince ourselves of this, by imagining $Y=Y_{1}\cdots Y_{n-1}$
and $Y_{n}=Z$, then this equation is just

$\displaystyle I(X;YZ)=I(X;Y)+H(X;Z|Y)\;,$ (8)

which is easily seen by writing the Venn diagram between $X$, $Y$, and $Z$.

Let us study the simplest case of three nodes. The three possible information
reductions are

$\displaystyle\Delta I_{1}$ $\displaystyle=$ $\displaystyle H(X_{\rm
out};Y_{1}|Y_{2}Y_{3})\;,$ (9) $\displaystyle\Delta I_{2}$ $\displaystyle=$
$\displaystyle H(X_{\rm out};Y_{2}|Y_{1}Y_{3})\;,$ (10) $\displaystyle\Delta
I_{3}$ $\displaystyle=$ $\displaystyle H(X_{\rm out};Y_{3}|Y_{1}Y_{2})\;.$
(11)

We will now prove that if $\Delta I_{3}<\Delta I_{1}$ and at the same time
$\Delta I_{3}<\Delta I_{2}$ (implying that node 3 should be removed first)
then it is not possible that the information reduction due to removal of nodes
1 and 2 at the same time $\Delta I_{12}<\Delta I_{3}$, so that we should have
removed nodes 1 and 2 at the same time instead of node 3 (making the removal
of node 3 deceptive).

Let’s first write down $\Delta I_{12}$. Since

$\displaystyle H(X_{\rm out};Y_{1}Y_{2}Y_{3})=I(X_{\rm out};Y_{3})+H(X_{\rm
out};Y_{1}Y_{2}|Y_{3})\;,$ (12)

we know that

$\displaystyle\Delta I_{12}=H(X_{\rm out};Y_{1}Y_{2}|Y_{3})\;.$ (13)

We can rewrite this as

$\displaystyle H(X_{\rm out};Y_{1}Y_{2}|Y_{3})=H(X_{\rm
out};Y_{2}|Y_{3})+H(X_{\rm out};Y_{1}|Y_{2}Y_{3})\;.$ (14)

This is the same rule as (8), just conditioned on a variable111All
information-theoretic equalities remain true if the left-hand side and the
right-hand side are conditioned on the same variable..

Eq. (14) implies that

$\displaystyle\Delta I_{12}=H(X_{\rm out};Y_{2}|Y_{3})+\Delta I_{1}\;.$ (15)

Now since $H(X_{\rm out};Y_{2}|Y_{3})\geq 0$, we know that $\Delta
I_{12}\geq\Delta I_{1}$. But since $\Delta I_{1}>\Delta I_{3}$ by assumption,
it follows immediately that

$\displaystyle\Delta I_{12}>\Delta I_{3}$ (16)

contradicting the claim that it is possible that $\Delta I_{12}<\Delta I_{3}$.

Clearly, the same argument will apply if we ask whether larger groups are
removed first: they can never remove less information than the smallest
information removed by a single node in that group.

If information is redundantly encoded, the greedy algorithm can fail. Suppose
two nodes are copies of each other $Y_{1}=Y_{2}$, making them perfectly
correlated: they carry the same exact information about $X_{\rm out}$. In that
case, we can remove any of the two nodes and it will not change the
information, that is, $\Delta I_{1}=\Delta I_{2}=0$:

$\displaystyle I(X_{\rm out};Y_{1}Y_{2}Y_{3})=I(X_{\rm
out};Y_{1}Y_{3})=I(X_{\rm out};Y_{2}Y_{3})\;.$ (17)

But once we removed one (say we removed $Y_{1}$), then removing $Y_{2}$
potentially removes information, as

$\displaystyle I(X_{\rm out};Y_{2}Y_{3})=I(X_{\rm out};Y_{3})+H(X_{\rm
out};Y_{2}|Y_{3})\;.$ (18)

Now that $Y_{1}$ is removed, the redundancy is gone and $H(X_{\rm
out};Y_{2}|Y_{3})$ could be large even though $\Delta I_{1}=H(X_{\rm
out};Y_{1}|Y_{2}Y_{3})=0$. This failure of the greedy algorithm is at the
origin of the discrepancies between the true minimal set of nodes (obtained by
exhaustive enumeration) and the set identified by the greedy algorithm, but
the failure is clearly rare.

## References

  * [1] Amina Adadi and Mohammed Berrada.  Peeking inside the black-box: a survey on explainable artificial intelligence (xai).  IEEE Access, 6:52138–52160, 2018.
  * [2] Pierre-Olivier Amblard and Olivier JJ Michel.  On directed information theory and granger causality graphs.  Journal of Computational Neuroscience, 30(1):7–16, 2011.
  * [3] Nihat Ay, Nils Bertschinger, Ralf Der, Frank Güttler, and Eckehard Olbrich.  Predictive information and explorative behavior of autonomous robots.  The European Physical Journal B, 63(3):329–339, 2008.
  * [4] William Bialek, Ilya Nemenman, and Naftali Tishby.  Predictability, complexity, and learning.  Neural Computation, 13(11):2409–2463, 2001.
  * [5] Clifford Bohm, Douglas Kirkpatrick, Victoria Cao, and Christoph Adami.  Information fragmentation, encryption and information flow in complex biological networks.  Entropy, 24:735, 2022.
  * [6] Clifford Bohm, Douglas Kirkpatrick, and Arend Hintze.  Understanding memories of the past in the context of different complex neural network architectures.  Neural Computation, 34(3):754–780, 2022.
  * [7] Alexander Borst and Frédéric E Theunissen.  Information theory and neural coding.  Nature Neuroscience, 2(11):947–957, 1999.
  * [8] Nitash C G, Barbara Lundrigan, Laura Smale, and Arend Hintze.  The effect of periodic changes in the fitness landscape on brain structure and function.  In ALIFE 2018: The 2018 Conference on Artificial Life, pages 469–476. MIT Press, 2018.
  * [9] Davide Castelvecchi.  Can we open the black box of ai?  Nature, 538:20–223, 2016.
  * [10] Samuel Chapman, David Knoester, Arend Hintze, and Christoph Adami.  Evolution of an artificial visual cortex for image recognition.  In ECAL 2013: The Twelfth European Conference on Artificial Life, pages 1067–1074. MIT Press, 2013.
  * [11] Alexander G Dimitrov, Aurel A Lazar, and Jonathan D Victor.  Information theory in neuroscience.  Journal of Computational Neuroscience, 30(1):1–5, 2011.
  * [12] Jin Fan.  An information theory account of cognitive control.  Frontiers in Human Neuroscience, 8:680, 2014.
  * [13] Robert M French.  Catastrophic forgetting in connectionist networks.  Trends in Cognitive Sciences, 3(4):128–135, 1999.
  * [14] Ryan Golden, Jean Erik Delanois, Pavel Sanda, and Maxim Bazhenov.  Sleep prevents catastrophic forgetting in spiking neural networks by forming a joint synaptic weight representation.  PLoS Comput Biol, 18:e1010628, 2022.
  * [15] Geoffrey E Hinton, Nitish Srivastava, Alex Krizhevsky, Ilya Sutskever, and Ruslan R Salakhutdinov.  Improving neural networks by preventing co-adaptation of feature detectors.  arXiv preprint arXiv:1207.0580, 2012.
  * [16] A. Hintze, D. Kirkpatrick, and C. Adami.  The structure of evolved representations across different substrates for artificial intelligence.  In T. Ikegami, N. Virgo, O. Witkowski, M. Oka, R. Suzuki, and H. Iizuka, editors, Proceedings Artificial Life 16, Cambridge, MA, 2018\. MIT Press.
  * [17] Arend Hintze.  The role weights play in catastrophic forgetting.  In 2021 8th International Conference on Soft Computing & Machine Intelligence (ISCMI), pages 160–166. IEEE, 2021.
  * [18] Arend Hintze and Christoph Adami.  Cryptic information transfer in differently-trained recurrent neural networks.  In 2020 7th International Conference on Soft Computing & Machine Intelligence (ISCMI), pages 115–120. IEEE, 2020.
  * [19] Ronald Kemker, Marc McClure, Angelina Abitino, Tyler Hayes, and Christopher Kanan.  Measuring catastrophic forgetting in neural networks.  In Proceedings of the 32nd AAAI Conference on Artificial Intelligence, pages 3390–3398, 2018.
  * [20] Diederik P. Kingma and Jimmy Ba.  Adam: A method for stochastic optimization.  In Yoshua Bengio and Yann LeCun, editors, 3rd International Conference for Learning Representations, San Diego, CA, 2015.
  * [21] Douglas Kirkpatrick and Arend Hintze.  The role of ambient noise in the evolution of robust mental representations in cognitive systems.  In ALIFE 2019: The 2019 Conference on Artificial Life, pages 432–439. MIT Press, 2019.
  * [22] James Kirkpatrick, Razvan Pascanu, Neil Rabinowitz, Joel Veness, Guillaume Desjardins, Andrei A Rusu, Kieran Milan, John Quan, Tiago Ramalho, Agnieszka Grabska-Barwinska, et al.  Overcoming catastrophic forgetting in neural networks.  Proceedings National Academy of Sciences USA, 114(13):3521–3526, 2017.
  * [23] Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner.  Gradient-based learning applied to document recognition.  Proceedings of the IEEE, 86(11):2278–2324, 1998.
  * [24] Nikos K Logothetis.  What we can do and what we cannot do with fMRI.  Nature, 453:869–878, 2008.
  * [25] Lars Marstaller, Arend Hintze, and Christoph Adami.  The evolution of representation in simple cognitive networks.  Neural Computation, 25(8):2079–2107, 2013.
  * [26] Michael McCloskey and Neal J Cohen.  Catastrophic interference in connectionist networks: The sequential learning problem.  In Psychology of Learning and Motivation, volume 24, pages 109–165. Elsevier, 1989.
  * [27] Mark D McDonnell, Shiro Ikeda, and Jonathan H Manton.  An introductory review of information theory in the context of computational neuroscience.  Biological Cybernetics, 105(1):55–70, 2011.
  * [28] L. Paninski.  Estimation of entropy and mutual information.  Neural Computation, 15:1191–1253, 2003.
  * [29] German I Parisi, Ronald Kemker, Jose L Part, Christopher Kanan, and Stefan Wermter.  Continual lifelong learning with neural networks: A review.  Neural Networks, 113:54–71, 2019.
  * [30] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala.  Pytorch: An imperative style, high-performance deep learning library.  In H. Wallach, H. Larochelle, A. Beygelzimer, F. d’Alché Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019.
  * [31] Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin.  ”Why should I trust you?” Explaining the predictions of any classifier.  In Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining, pages 1135–1144, 2016.
  * [32] Thomas Schreiber.  Measuring information transfer.  Physical Review Letters, 85:461, 2000.
  * [33] M. Sella.  Tracing computations in deep neural networks.  Master’s thesis, School of Information and Engineering, Dalarna University, Falun, Sweden, 2022.
  * [34] Claude Elwood Shannon.  A mathematical theory of communication.  The Bell System Technical Journal, 27(3):379–423, 1948.
  * [35] James M Shine, Mike Li, Oluwasanmi Koyejo, Ben Fulcher, and Joseph T Lizier.  Nonlinear reconfiguration of network edges, topology and information content during an artificial learning task.  Brain Informatics, 8(1):1–15, 2021.
  * [36] Ali Tehrani-Saleh and Christoph Adami.  Can transfer entropy infer information flow in neuronal circuits for cognitive processing?  Entropy, 22:385, 2020.
  * [37] Nicholas M Timme and Christopher Lapish.  A tutorial for information theory in neuroscience.  eNeuro, 5(3), 2018.
  * [38] Giulio Tononi.  Integrated information theory.  Scholarpedia, 10(1):4164, 2015.


$\mathcal{B}=(B_{\sf p},{\mathbb{R}},d_{B}:B_{\sf
p}^{2}\rightarrow{\mathbb{R}},{r_{1}}_{B}:B_{\sf p}\rightarrow{\mathbb{R}})$

of ${\mathcal{T}}^{m}_{d}\cup{\sf Free}(r_{1})$ as follows:

  * •

Take as $\mathcal{B}_{\sf p}$ an isomorphic copy (via isomorphism $i$) of the
set
$\\{c_{\mathcal{A}}\mid c\text{ constant of sort {\sf p} occurring in }G\\}$,

  * •

Define $d_{B},{r_{1}}_{B}$ as follows:

    * –

$d_{\mathcal{B}}(i(c_{\mathcal{A}}),i(d_{\mathcal{A}})):=d_{\mathcal{A}}(c_{\mathcal{A}},d_{\mathcal{A}})$;

    * –

${r_{1}}_{\mathcal{B}}(i(c_{\mathcal{A}})):={r_{1}}_{\mathcal{A}}(c_{\mathcal{A}})$.

The converse implication is analogous, with the only difference that we first
construct a partial algebra
$\mathcal{A}=({\mathbb{R}},d_{A}:{\mathbb{R}}^{2}\rightarrow{\mathbb{R}},{r_{1}}_{A}:{\mathbb{R}}\rightarrow{\mathbb{R}})$
by considering an injective map from the support of sort ${\sf p}$ in
${\mathbb{R}}$ and then we use the locality property of
${\mathcal{T}}^{m}_{d}\cup{\sf Free}(r_{1})$ to prove the existence of a total
model with support ${\mathbb{R}}$.

###  0.A.2 Tests for Example 4

We use sehpilot (an implementation of Algorithm 1) to derive constraints
$\Gamma$ on the parameters $r_{1},r_{2}$ such that

$\pi^{i}(u,v)\wedge\pi^{e}(u,v)=(u\neq v\land d(u,v)\leq
r_{1}(u))\wedge(d(u,v)>r_{2}(u))$

is unsatisfiable (we consider the case in which $d$ is an uninterpreted
function). Since sehpilot first uses H-PILoT for the hierarchical reduction
(and afterwards Redlog for quantifier elimination), the input file is in
H-PILoT syntax:

⬇

Base_functions:={(+,2), (-,2), (*,2)}

Extension_functions:={(r1, 1, 1), (r2, 1, 1), (d, 2, 1)}

Relations:={(<=, 2), (<, 2), (>=, 2), (>, 2)}

Query := NOT(u = v);

d(u,v) <= r1(u);

d(u,v) > r2(u);

Note that when using sehpilot the user has to specify which symbols have to be
eliminated.

Assume that $r_{1}$ and $r_{2}$ are parameters (and thus should not be
eliminated). Since the variable $u$ occurs as an argument of $r_{1}$ and
$r_{2}$ (which are parameters), $u$ should not be eliminated. We have to
eliminate the remaining symbols, i.e. $v$ and $d$. We obtain the following
output (in verbose mode) from sehpilot:

⬇

[2021-02-12 14:06:07,115 | INFO] convert prefix notation

{’e_3’: ’r2(u)’, ’e_2’: ’r1(u)’, ’e_1’: ’d(u, v)’}

to

{’e_3’: ’r2(u)’, ’e_2’: ’r1(u)’, ’e_1’: ’d(u, v)’}

[2021-02-12 14:06:07,115 | INFO] assignments of new variables

e_3 = r2(u)

e_2 = r1(u)

e_1 = d(u, v)

[2021-02-12 14:06:07,115 | INFO] reduced assignments

e_3 = r2(u)

e_2 = r1(u)

e_1 = d(u, v)

[2021-02-12 14:06:07,115 | INFO] variables that will be eliminated

by REDLOG:

e_1, d, v

[2021-02-12 14:06:07,116 | INFO] extension functions declared in loc-file

[(’r1’, 1, 1), (’r2’, 1, 1), (’d’, 2, 1)]

[2021-02-12 14:06:07,116 | INFO] universal arguments

u, u

[2021-02-12 14:06:07,116 | INFO] add switches:

off nat;

[2021-02-12 14:06:07,117 | INFO] saved REDLOG file with

new variable declaration

/home/dpeuter/Work/FroCoS-2021/example4.dat

[2021-02-12 14:06:07,315 | INFO] REDLOG query after

variable elimination:

all(u, e_2 - e_3 > 0)

[2021-02-12 14:06:07,315 | INFO] REDLOG command:

run_redlog_computation := not (e_2 - e_3 > 0);

[2021-02-12 14:06:07,508 | INFO] REDLOG command:

run_redlog_computation := rlnnf (not(e_2 - e_3 > 0));

[2021-02-12 14:06:07,707 | INFO] reduce constants {} of

e_2 - e_3 <= 0

to

e_2 - e_3 <= 0

[2021-02-12 14:06:07,707 | INFO] REDLOG command:

run_redlog_computation := rlsimpl (e_2 - e_3 <= 0);

Constraints (H-PILoT syntax, reduced):

(FORALL u). r1(u) - r2(u) <= _0

The generated constraint $\Gamma=\forall u(r_{1}(u)\leq r_{2}(u))$ is exactly
the constraint we obtained by applying Steps 1-5 of Algorithm 1 by hand in
Example 4.

We used verbose mode for the output of sehpilot such that more details are
displayed in the output file. This way one can follow easily the different
steps. One can for example see which new constants are introduced in the
hierarchical reduction ($e_{1}$, $e_{2}$ and $e_{3}$) and which terms they
represent. The output also shows the result obtained directly after the
elimination ($e_{2}>e_{3}$), the negation of this result ($e_{2}\leq e_{3})$,
and finally the universally quantified formula with the constants replaced
back with the corresponding terms ($\forall u(r_{1}(u)\leq r_{2}(u))$).

Remark: The current implementation of sehpilot assumes that the problems are
expressed in a local extension of the theory of real closed fields and a
reduction to quantifier elimination in the theory of real-closed fields is
performed. For the examples we considered this does not lead to loss of
generality because the constraints on constants of sort ${\sf p}$ are only
equalities and disequalities. If variables initially of sort ${\sf p}$ are
eliminated, they do not occur below any parameter. Such variables occur
separately from the variables of original sort ${\sf num}$ in the quantifier
elimination problem.

This means that the quantifier elimination problem is of the form

$\exists x_{1},\dots,x_{n}\exists y_{1},\dots,y_{m}C_{\sf
p}(x_{1},\dots,x_{n})\wedge C_{\sf num}(y_{1},\dots,y_{m})$

where $x_{1},\dots,x_{n}$ are variables of sort ${\sf p}$ and
$y_{1},\dots,y_{m}$ are variables of sort ${\sf num}$, which is equivalent to:

$\exists x_{1},\dots,x_{n}C_{\sf
p}(x_{1},\dots,x_{n})~{}~{}\wedge~{}~{}\exists y_{1},\dots,y_{m}C_{\sf
num}(y_{1},\dots,y_{m}).$

Quantifier elimination in the theory of real-closed fields can be used for the
formula $\exists y_{1},\dots,y_{m}C_{\sf num}(y_{1},\dots,y_{m})$.

If we consider theories whose models of sort ${\sf p}$ contain infinitely many
elements, then – since the constraint $C_{\sf p}$ contains only equalities and
disequalities – the method for quantifier elimination in the theory of
infinite sets can be simulated by the method for quantifier elimination in
real closed fields. This is the reason why for this type of problems we can
use quantifier elimination in the theory of real closed fields without
problems.

###  0.A.3 Tests for Example 8

In order to check whether the class containment

${\bf QUDG}(r)=({\bf MinDG}(r)\cap{\bf MaxDG}(1))^{-}\subseteq({\bf
MinDG}(r)\cap{\bf MaxDG}(1))^{+}$

holds we have to check whether $G_{1}\land g_{i}$ is unsatisfiable for all
$i\in{1,2,3,4,5}$ (where $G_{1}$ is the axiomatization for ${\bf QUDG}(r)$ and
the $g_{i}$ are the ground formulae obtained from the negation of $G_{2}$, the
axiomatization of the other class; cf. Example 8).

We assume that $d$ is a metric. Using H-PILoT we can show that $G_{1}\land
g_{i}$ is unsatisfiable w.r.t. ${\mathcal{T}}_{d}^{m}$ for $i\in\\{1,2,3\\}$.
We here only show the test for the case $G_{1}\land g_{4}$ in detail (the case
$G_{1}\land g_{5}$ is similar and yields the same results).

We check satisfiability of $G_{1}\land g_{4}$ w.r.t. ${\mathcal{T}}_{d}^{m}$
using H-PILoT. We have the following input file:

⬇

Base_functions:={(+,2), (-,2), (*,2)}

Extension_functions:={(r, 1, 1), (d, 2, 1), (F, 2, 1)}

Relations:={(<=, 2), (<, 2), (>=, 2)}

Clauses :=

% axioms for G1

(FORALL x,y). d(x,y) <= r(x), d(x,y) > _1

–> x = y, _0 = _1;

(FORALL x,y). d(x,y) <= r(x), d(y,x) <= r(y)

–> x = y, F(y,x) = _1;

(FORALL x,y). d(x,y) > _1 –> F(x,y) = _0;

(FORALL x,y). d(x,y) > _1 –> F(y,x) = _0;

(FORALL x,y). F(x,y) = _1 –> F(y,x) = _1;

% axioms for d being a metric

(FORALL x,y). d(x,y) >= _0;

(FORALL x,y). d(x,y) = _0 –> x = y;

(FORALL x,y). x = y –> d(x,y) = _0;

(FORALL x,y). d(x,y) = d(y,x);

(FORALL x,y,z). d(x,y) <= d(x,z) + d(z,y);

% F is either 0 or 1

(FORALL x,y). –> F(x,y) = _0, F(x,y) = _1;

Query :=

% g4 of (not G2)

NOT(a = b);

d(a,b) <= r(a);

F(a,b) = _0;

% needed for instantiation

F(a,b) = F(a,b);

F(b,a) = F(b,a);

F(a,a) = F(a,a);

F(b,b) = F(b,b);

d(a,b) = d(a,b);

d(b,a) = d(b,a);

d(a,a) = d(a,a);

d(b,b) = d(b,b);

r(a) = r(a);

r(b) = r(b);}

Note that the trivial equalities at the end of the file are used to ensure
that H-PILoT computes sufficiently many instances. We obtain the following
output from H-PILoT:

⬇

Reduced problem written to example8-Tm-4.smt.

Unknown. Prover says ’sat’ but this can only be trusted

for local extensions and this problem is not known to be

local.

H-PILoT spent 0.208608s on the problem.

The prover needed 0.01677 s for the problem.

Total running time: 0.225378s.

Since we know that ${\mathcal{T}}^{m}_{d}\cup{\sf Free}(r_{1},r_{2})$ is a
$\Psi$-local theory extension and we ensured that H-PILoT computes
sufficiently many instances, we know that $G_{1}\wedge g_{4}$ is satisfiable.
This means that the class inclusion does not hold in general. We use sehpilot
to derive (weakest) conditions $\Gamma$ on parameters such that
unsatisfiability of $G_{1}\land\Gamma\land g_{4}$ is guaranteed.

We first consider $r$ to be the only parameter, i.e. we tell sehpilot to
eliminate $F$ and $d$ ($a$ and $b$ appear as arguments of parameter $r$ and
are therefore not eliminated). The input file is the same file that was used
for checking satisfiability with H-PILoT. We get the following output (using
verbose mode) from sehpilot:

⬇

[2021-02-20 12:55:56,356 | INFO] convert prefix notation

{’e_10’: ’r(b)’, ’e_9’: ’r(a)’, ’e_8’: ’d(b, b)’,

’e_7’: ’d(b, a)’, ’e_6’: ’d(a, b)’, ’e_5’: ’d(a, a)’,

’e_4’: ’F(b, b)’, ’e_3’: ’F(b, a)’, ’e_2’: ’F(a, b)’,

’e_1’: ’F(a, a)’}

to

{’e_10’: ’r(b)’, ’e_9’: ’r(a)’, ’e_8’: ’d(b, b)’,

’e_7’: ’d(b, a)’, ’e_6’: ’d(a, b)’, ’e_5’: ’d(a, a)’,

’e_4’: ’F(b, b)’, ’e_3’: ’F(b, a)’, ’e_2’: ’F(a, b)’,

’e_1’: ’F(a, a)’}

[2021-02-20 12:55:56,356 | INFO] assignments of new variables

e_10 = r(b)

e_9 = r(a)

e_8 = d(b, b)

e_7 = d(b, a)

e_6 = d(a, b)

e_5 = d(a, a)

e_4 = F(b, b)

e_3 = F(b, a)

e_2 = F(a, b)

e_1 = F(a, a)

[2021-02-20 12:55:56,356 | INFO] reduced assignments

e_10 = r(b)

e_9 = r(a)

e_8 = d(b, b)

e_7 = d(b, a)

e_6 = d(a, b)

e_5 = d(a, a)

e_4 = F(b, b)

e_3 = F(b, a)

e_2 = F(a, b)

e_1 = F(a, a)

[2021-02-20 12:55:56,356 | INFO] variables that will be

eliminated by REDLOG:

e_1, e_7, e_6, e_3, d, e_5, e_8, e_4, F, e_2

[2021-02-20 12:55:56,357 | INFO] extension functions

declared in loc-file

[(’r’, 1, 1), (’d’, 2, 1), (’F’, 2, 1)]

[2021-02-20 12:55:56,357 | INFO] universal arguments

b, a

[2021-02-20 12:55:56,358 | INFO] add switches:

off nat;

[2021-02-20 12:55:56,358 | INFO] saved REDLOG file with

new variable declaration

/home/dpeuter/Work/FroCoS-2021/example8/example8-Tm-4.dat

[2021-02-20 12:55:56,631 | INFO] REDLOG query after

variable elimination:

all({a, b}, e_9 > 0 and e_9 - 1 <= 0 and e_10 - e_9 < 0

and a - b <> 0 or e_9 - 1

>= 0 and e_10 - 1 < 0 and a - b <> 0)

[2021-02-20 12:55:56,631 | INFO] REDLOG command:

run_redlog_computation := not (e_9 > 0 and e_9 - 1 <= 0

and e_10 - e_9 < 0 and a - b <> 0 or e_9 - 1 >= 0

and e_10 - 1 < 0 and a - b <> 0);

[2021-02-20 12:55:56,830 | INFO] REDLOG command:

run_redlog_computation := rlnnf (not(e_9 > 0

and e_9 - 1 <= 0 and e_10 - e_9 < 0 and a - b <> 0

or e_9 - 1 >= 0 and e_10 - 1 < 0 and a - b <> 0));

[2021-02-20 12:55:57,039 | INFO] reduce constants {} of

(e_9 <= 0 or e_9 - 1 > 0 or e_10 - e_9 >= 0 or a - b = 0)

and (e_9 - 1 < 0 or e_10 - 1 >= 0 or a - b = 0)

to

(e_9 <= 0 or e_9 - 1 > 0 or e_10 - e_9 >= 0 or a - b = 0)

and (e_9 - 1 < 0 or e_10 - 1 >= 0 or a - b = 0)

[2021-02-20 12:55:57,039 | INFO] REDLOG command:

run_redlog_computation := rlsimpl ((e_9 <= 0

or e_9 - 1 > 0 or e_10 - e_9 >= 0 or a - b = 0)

and (e_9 - 1 < 0 or e_10 - 1 >= 0 or a - b = 0));

Constraints (H-PILoT syntax, reduced):

(FORALL a, b). AND(OR(r(a) <= _0, r(a) - _1 > _0,

r(b) - r(a) >= _0, a - b = _0), OR(r(a) - _1 < _0,

r(b) - _1 >= _0, a - b = _0))

Redlog does not simplify the results of the quantifier elimination very well,
so in many cases one obtains long formulae, which sometimes can be simplified.
In this case the constraint computed by sehpilot can be simplified to

$C^{r}=\forall x,y(r(y)<1\wedge x\neq y\rightarrow r(y)\geq r(x)).$

We could also choose different parameters, e.g. we could assume $d$ and $r$ to
be parameters and then tell sehpilot to eliminate only $F$. In this case the
computed constraint will be:

⬇

Constraints (H-PILoT syntax, reduced):

(FORALL b, a). OR(NOT(d(b, b) = _0), d(b, a) <= _0,

d(a, b) <= _0, d(a, b) - _1 > _0, d(a, b) - r(a) > _0,

NOT(d(a, b) - d(b, a) = _0), NOT(d(a, a) = _0),

r(b) - d(b, a) >= _0, a - b = _0)

This constraint can be simplified to

$C^{d,r}=\forall x,y(x\neq y\wedge d(x,y)\leq 1\wedge d(x,y)\leq
r(x)\rightarrow d(y,x)\leq r(y)).$

##  Appendix 0.B Proof of Theorem 2

Theorem 2. Let ${\mathcal{K}}$ be a set of $\Sigma$-flat clauses, with the
property that every variable occurs only once in every term. Let $\Psi$ be a
term closure operator with the property that for every flat set of ground
terms $T$, $\Psi(T)$ is flat.

Assume that ${\mathcal{K}}$ and $\Psi$ have the property that for every flat
set of ground terms $T$ and for every clause $C\in{\mathcal{K}}$, if $C$
contains terms $f(x_{1},\dots,x,\dots,x_{n})$ and
$g(y_{1},\dots,x,\dots,y_{m})$ (where $f,g\in\Sigma$ are extension functions
and $f$ and $g$ are not necessarily different), if
$f(t_{1},\dots,t,\dots,t_{n}),g(s_{1},\dots,s,\dots,s_{m})\in\Psi_{{\mathcal{K}}}(T)$
then
$f(t_{1},\dots,s,\dots,t_{n}),g(s_{1},\dots,t,\dots,s_{m})\in\Psi_{{\mathcal{K}}}(T)$.
Then $({\sf Emb}_{w,f}^{\Psi})$ implies $({\sf Loc}_{f}^{\Psi})$.

Proof: Assume that ${\mathcal{T}}_{0}\cup{\mathcal{K}}$ is not a $\Psi$-local
extension of ${\mathcal{T}}_{0}$. Then there exists a set $G$ of ground
clauses (with additional constants) such that
${\mathcal{T}}_{0}\cup{\mathcal{K}}\cup G\models\perp$ but
${\mathcal{T}}_{0}\cup{\mathcal{K}}[\Psi_{\cal K}(G)]\cup G$ has a weak
partial model $P$ in which all terms in $\Psi_{\cal K}(G)$ are defined. We
assume w.l.o.g. that $G=G_{0}\cup G_{1}$, where $G_{0}$ contains no function
symbols in $\Sigma$ and $G_{1}$ consists of ground unit clauses of the form
$f(c_{1},\dots,c_{n})\approx c$ where $c_{i},c$ are constants in
$\Sigma_{0}\cup\Sigma_{c}$ and $f\in\Sigma$.

We construct another structure, $\mathcal{A}$, having the same support as $P$,
which inherits all relations in ${\sf Pred}$ and all maps in
$\Sigma_{0}\cup\Sigma_{c}$ from $P$, but on which the domains of definition of
the $\Sigma$-functions are restricted as follows: for every $f\in\Sigma$,
$f_{\mathcal{A}}(a_{1},\dots,a_{n})$ is defined if and only if there exist
constants $c^{1},\dots,c^{n}$ such that $f(c^{1},\dots,c^{n})$ is in
$\Psi_{\cal K}(G)$ and $a^{i}=c^{i}_{P}$ for all $i\in\\{1,\dots,n\\}$. In
this case we define
$f_{\mathcal{A}}(a_{1},\dots,a_{n}):=f_{P}(c^{1}_{P},\dots,c^{n}_{P})$. The
reduct of $\mathcal{A}$ to $(\Sigma_{0}\cup\Sigma_{c},{\sf Pred})$ coincides
with that of $P$. Thus, $\mathcal{A}$ is a model of ${\mathcal{T}}_{0}\cup
G_{0}$. By the way the operations in $\Sigma$ are defined in $\mathcal{A}$ it
is clear that $\mathcal{A}$ satisfies $G_{1}$, so $\mathcal{A}$ satisfies $G$.

We now show that $\mathcal{A}\models_{w}{\mathcal{K}}$. Let $D$ be a clause in
${\mathcal{K}}$. If $D$ is ground then all its terms are defined, and all
terms starting with an extension function are contained in
$\Psi_{{\mathcal{K}}}(G)$, i.e. $D\in{\mathcal{K}}[\Psi_{{\mathcal{K}}}(G)]$,
so $D$ is true in $P$, hence it is also true in $\mathcal{A}$.

Now consider the case in which $D$ is not ground. Let
$\beta:X\rightarrow\mathcal{A}$ be an arbitrary valuation. Again, if there is
a term $t$ in $D$ such that $\beta(t)$ is undefined, we immediately have that
$\beta$ weakly satisfies $D$. So let us suppose that for all terms $t$
occurring in $D$, $\beta(t)$ is defined. We associate with $\beta$ a
substitution $\sigma$ as follows: Let $x$ be a variable.We have the following
possibilities:

Case 1: $x$ does not occur below any extension function. This case is
unproblematic. We can define $\sigma(x)$ arbitrarily.

Case 2: $x$ occurs in a unique term $t=f(...x...y...)$ (which may occur more
than once) and $x$ occurs only once in $t$. From the fact that $\beta(t)$ is
defined, we know that there are ground terms which we will denote by
$t_{x},t_{y},\dots$ such that
$\beta(x)=(t_{x})_{P},\beta(y)=(t_{y})_{P},\dots$. Since
$\beta(t)=f_{A}(...(t_{x})_{P}\dots(t_{y})_{P}\dots)$ is defined,
$f(\dots,t_{x},\dots,t_{y},\dots)\in\Psi_{\cal K}(G)$. We can define
$\sigma(x)=t_{x}$.

Case 3: $x$ occurs in two or more terms of the form
$f_{k}(x^{k}_{1},\dots,x,\dots,x^{k}_{n_{k}})$, $1\leq k\leq p$, $p\geq 2$,
but occurs at most once in any term of $C$, where $f_{1},\dots,f_{n}$ are
function symbols, not necessarily different (but in terms starting with the
same function symbols $x$ occurs on different positions).

From the fact that $\beta(f_{k}(x^{k}_{1},\dots,x,\dots,x^{k}_{n}))$ is
defined, we know that there are ground terms which we will denote by
$t^{k}_{x},t_{x^{k}_{i}}$ such that for every $k$ with $1\leq k\leq p$:

  * •

$\beta(x)=(t^{k}_{x})_{P},\beta(x^{k}_{i})=(t_{x^{k}_{i}})_{P}$ for $1\leq
k\leq p$ and $1\leq i\leq n_{k}$, and

  * •

$\beta(f_{k}(x^{k}_{1},\dots,x,\dots,x^{k}_{n_{k}}))=f_{\mathcal{A}}((t_{x^{k}_{1}})_{P},...,(t^{k}_{x})_{P},\dots,(t_{x^{k}_{n}})_{P})$,
i.e. $f(t_{x^{k}_{1}},\dots,t^{k}_{x},\dots,t_{x^{k}_{n}})\in\Psi_{\cal
K}(G)$.

We know that $\Psi_{{\mathcal{K}}}$ has the property that for every clause
$C\in{\mathcal{K}}$, if $C$ contains terms
$f_{i}(x^{i}_{1},\dots,x,\dots,x^{i}_{n_{i}})$ and
$f_{k}(x^{k}_{1},\dots,x,\dots,x^{k}_{n_{k}})$ and if

$f_{i}(t_{x^{i}_{1}},\dots,t^{i}_{x},\dots,t_{x^{i}_{n_{i}}})\in\Psi_{\cal
K}(G)$ and
$f_{k}(t_{x^{k}_{1}},\dots,t^{k}_{x},\dots,t_{x^{k}_{n_{k}}})\in\Psi_{\cal
K}(G)$

then also
$f_{i}(t^{i}_{x^{i}_{1}},\dots,t^{k}_{x},\dots,s_{x^{i}_{n_{i}}})\in\Psi_{\cal
K}(G)$
and$f_{k}(t^{k}_{x^{k}_{1}},\dots,t^{i}_{x},\dots,s_{x^{k}_{n_{k}}})\in\Psi_{\cal
K}(G)$.

This means that we can define $\sigma(y)=t_{y}$ for every linear variable; for
every variable $x$ which occurs in different terms, let $t_{x}$ be one of the
terms obtained as before (say $t_{x}=t^{1}_{x}$) and define $\sigma(x)=t_{x}$.

Thus, we can construct a substitution $\sigma$ with
$\sigma(D)\in{\mathcal{K}}[G]$ and $\beta\circ\sigma=\beta$. As
$(P,\beta)\models_{w}\sigma(D)$ we can infer
$(\mathcal{A},\beta)\models_{w}D$.

We now show that $D(\mathcal{A})=\\{f(a_{1},\dots,a_{n})\mid
f_{A}(a_{1},\dots,a_{n})\text{ defined}\\}$ is closed under $\Psi_{\cal K}$.
By definition, $f(a_{1},\dots,a_{n})\in D(\mathcal{A})$ iff there exist
$\text{ constants }c_{1},\dots,c_{n}$ with ${c_{i}}_{A}=a_{i}$ for all $i$ and
$f(c_{1},\dots,c_{n})\in\Psi_{\cal K}(G)$. Thus,

$\begin{array}[]{rll}D(\mathcal{A})&=\\{f(a_{1},\dots,a_{n})\mid
f_{A}(a_{1},\dots,a_{n})\text{ defined}\\}&\\\
&=\\{f({c_{1}}_{\mathcal{A}},\dots,{c_{n}}_{\mathcal{A}})\mid c_{i}\text{
constants with }f(c_{1},\dots,c_{n})\in\Psi_{\cal K}(G)\\}&\\\
&={\overline{h}}(\Psi_{\cal
K}(G))&\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\text{
where }h(c_{i})=a_{i}\text{ for all }i\\\ \Psi_{\cal
K}(D(\mathcal{A}))&=\Psi_{\cal K}({\overline{h}}(\Psi_{\cal
K}(G)))={\overline{h}}(\Psi_{\cal K}(\Psi_{\cal
K}(G)))&\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\text{
by property (iv) of }\Psi\\\ &\subseteq{\overline{h}}(\Psi_{\cal
K}(G))=D(\mathcal{A})&\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\text{
by property (iii) of }\Psi\\\ \end{array}$

As $\mathcal{A}\models_{w}{\mathcal{K}}$, $\mathcal{A}$ weakly embeds into a
total algebra $\mathcal{B}$ satisfying ${\mathcal{T}}_{0}\cup{\mathcal{K}}$.
But then $\mathcal{B}\models G$, so
$\mathcal{B}\models{\mathcal{T}}_{0}\cup{\mathcal{K}}\cup G$, which is a
contradiction. $\Box$

Remark: A similar result can be proved also in the case in which some
variables occur several times below a function symbol if
$\Psi_{{\mathcal{K}}}$ has the property that if $f(x_{1},\dots,x,\dots,x\dots
x_{n})\in{\mathcal{K}}$ and
$f(t_{1},\dots,s,\dots,t,\dots,t_{n})\in\Psi_{{\mathcal{K}}}(T)$
then $f(t_{1},\dots,t,\dots,t,\dots,t_{n})\in\Psi_{{\mathcal{K}}}(T)$ and
$f(t_{1},\dots,s,\dots,s,\dots,t_{n})\in\Psi_{{\mathcal{K}}}(T)$.

##  Appendix 0.C Constrained Horn Clauses: Definitions

We give the definitions of constrained Horn clauses, mainly following the
presentation in [12].

######  Definition 5 ([12])

Conjunctions $\Pi$ of constrained Horn clauses are constructed as follows:

$\displaystyle\Pi$ $\displaystyle::={\sf chc}\wedge\Pi\mid\top$
$\displaystyle{\sf chc}$ $\displaystyle::=\forall var.{\sf chc}\mid{\sf
body}\rightarrow{\sf head}$ $\displaystyle{\sf pred}$ $\displaystyle::={\sf
upred}\mid\phi$ $\displaystyle{\sf head}$ $\displaystyle::={\sf pred}$
$\displaystyle{\sf body}$ $\displaystyle::=\top\mid{\sf pred}\mid{\sf
body}\wedge{\sf body}\mid\exists var.{\sf body}$ $\displaystyle{\sf upred}$
$\displaystyle::=\text{an uninterpreted predicate applied to terms}$
$\displaystyle\phi$ $\displaystyle::=\text{a formula whose terms and
predicates are interpreted over }\mathcal{A}$ $\displaystyle var$
$\displaystyle::=\text{a variable}$

A clause where the head is a formula $\phi$ is called a query or a goal
clause. The terminology “fact clause” is used for a clause whose head is an
uninterpreted predicate and body is a formula $\phi$.

It is easy to see that in Theorem 14, if we guarantee that the formulae
$\phi_{i}$ are formulae whose terms and predicates are interpreted over
$\mathcal{A}$ then all clauses of the form

$\phi_{i}({\overline{x}})\rightarrow\mu_{i}({\overline{x}})$

are constrained Horn clauses, hence:

$\begin{array}[]{rl}CH_{N}=\\{&\phi_{i}({\overline{x}})\rightarrow\mu_{i}({\overline{x}})\mid
i\in\\{1,\dots,n\\}\\}\\\
\cup\\{&(\mu_{i}({\overline{x}})\wedge\mu_{j}({\overline{y}}))\sigma\rightarrow\mu_{k}({\overline{z}})\mid
C_{k}({\overline{z}})\text{ is obtained by a resolution }\\\ &\hskip
42.67912pt\text{ inference in }{\cal I}_{P}\text{ from
}C_{i}({\overline{x}})\text{ and }C_{j}({\overline{y}})\text{ with m.g.u.\
}\sigma\\}\\\
\cup\\{&\mu_{i}({\overline{x}})\sigma\rightarrow\mu_{k}({\overline{z}})\mid
C_{k}({\overline{z}})\text{ is obtained by a factorization inference }\\\
&\hskip 42.67912pt\text{ in }{\cal I}_{P}\text{ from
}C_{i}({\overline{x}})\text{ with m.g.u.\ }\sigma\\}\end{array}$

is a set of constrained Horn clauses.