Probabilistic abstract interpretation is a theory used to extract particular properties of a computer program when it is infeasible to test every single inputs. In this paper we apply the theory on neural networks for the same purpose: to analyse density distribution flow of all possible inputs of a neural network when a network has uncountably many or countable but infinitely many inputs. We show how this theoretical framework works in neural networks and then discuss diferent abstract domains and corresponding Moore-Penrose pseudo-inverses together with abstract transformers used in the framework. We also present experimental examples to show how this framework helps to analyse real world problems.
In recent years, deep neural networks has been regarded as an essential technique for machine learning since the work of deep learning is being progressed [1, 2] and have been playing in a big role in many industries in real world. However, a major problem of it is that it is dificult to interpret how neural networks deal with information and derive their decisions, especially when layers are getting deeper. Interpreting neural networks is important because in some application areas cost of mistakes is intolerable. Our approach aims at making use of the theory of probabilistic abstract interpretation to analyse density distribution flow of possible inputs of a neural network and to make sure the system is safe and under controlled.
Research on interpreting neural networks has been carried on for years. One approach to do is through rule extraction algorithms [3]. Activation Maximisation is another approach to interpret model prediction by only looking at its relationships with input, disregarding the inner process [4]. A further development of the technique is to add a decoder on it [5]. In the same year Bazen et al. used Taylor decomposition explain model’s decision by decomposing output as a sum of relevance scores [6], and Landecker et al. decomposed the model prediction by back-propagating relevance in reverse direction, progressively redistributing the prediction score until the input is reached [7]. Bach et al. further introduced the Layer-wise Relevance Propagation explanation framework [8]. Another measurement is to use sensitivity analysis to quantify the importance of each input variable [9]. In 2015 Zilke proposed DeepRED, by extending a decompositional algorithm CRED [10]. Jacobsson [12] and Wang [13] have proposed algorithms of understanding recurrent neural networks. In 2018 Zhang et al. and Zhou et al. respectively proposed methods to interpret convolutional neural networks [14, 15, 16]. Zeiler et al. instead used approach of layer activation visualisation with algorithm of Deconvnets to understand CNN [17]. Bau et al. proposed Network Dissection framework which well quantifies the interpretability of latent representations of CNN [18]. In the mean time, the attacks and defenses from adversarial examples to neural networks are frequently studied [19].
Program analysis, on the other hand, is a research area which focuses on using mathematical theory and formal methods to automatically analyse the behavior of a computer program regarding a property side →− is the concrete domain and the right hand side #→−− # # is the abstract domain. such as safety, correctness, robustness and liveness [20]. In particular, abstract interpretation is a theory of approximating semantics of a computer program based on order theory, especially lattices [21, 23]. In recent years, probabilistic program analysis has been introduced to analyze quantitative aspect of computer programs. Probabilistic abstract interpretation correspondingly is the framework to lift classical abstract interpretation to the probabilistic setting [24, 25, 26, 27].
In 2018 SRILAB proposed 2 analyzer that uses abstract interpretation to over-approximate a range of concrete values into an abstract domain and checks whether this abstract domain holds the expected result, and which will prove every single input over-approximated by this abstract domain also holds this result [28]. Later [29] proposed a new abstract domain which combines floating point polyhedra with intervals. Its performance was compared to Reluplex which is a former property verification technique extending the simplex algorithm to support ReLU constraints [30]. Abstract interpretation is also bridged with gradient-based optimization and can be applied on training neural networks [31]. In this paper, we take theory of probabilistic abstract interpretation to analyse density distribution lfow of all possible inputs of a neural network, when the network has uncountably many or countable but infinitely many possible inputs. We also see that in particular situations probabilistic abstract interpretation has stronger features than classical ones. Section 2 gives a brief background of probabilistic abstract interpretation theory. In Section 3 we introduce how to apply the theory on neural networks, and discuss diferent choices of abstract domains for diferent purposes, together with corresponding Moore-Penrose pseudo inverses and abstract domains. In Section 4 we show in experiments how the framework helps in real world problem. Section 5 gives a conclusion and future works.
In this section we give a brief introduction of probabilistic abstract interpretation theory originally
introduced in program analysis. Probabilistic abstract interpretation is considered as a quantitative
version of the classical abstract interpretation, commonly to give a not safe but a more average case
scenario, while the classical framework keeps safe but might be not precise enough and therefore
addressing a worst case scenario [20, 21, 25, 33, 26]. In probabilistic framework, instead of forming a
Galois connection in which classical framework does, we take a Moore-Penrose pseudo-inverse.
Definition 1. Let and # be two finite-dimensional vector (Hilbert) spaces and : → # a linear
map. Then the linear map : # → is the Moore-Penrose pseudo-inverse of A if (i) ∘ = (ii)
∘ = , where and denote orthogonal projections onto the ranges of and .
As shown in Figure 1, is the original function in concrete domain, which can be a step in a computer
program. Based on , we further consider functio→n− in probability domain and function # in abstract
domain respectively. Given in concrete domain
we lift t→o− which is a mapping from a distribution to a distribution in probabilistic domain
(
# = ′ where we have Moore-Penrose pseudo-inverse as connections between concrete and abstract domains. # is also called the abstract transformer. Defining an appropriate abstract domain and formalising an appropriate abstract transformer is crucial to performance of this analysis framework. Proposition 1. An abstract transformer of a composition of functions is a composition of abstract transformers of each function, that is
if = ′ ∘ ′′, then # = ′# ∘ ′′#
In this section we discuss how to apply theory of probabilistic abstract interpretation on neural networks. In principle, any neural network is a non-linear function which can be simulated by a computer program, thus any analysis framework working on a computer program can work on a neural network.
A typical layer in a feed-forward neural network can be expressed as an afine transformation followed by a non-linear function, or more specifically can be for example in form of
+1 = ( + ) where is the layer number, is the input of the layer, +1 is the output, and are the weights of afine transformation, and is one example of choices of activation functions. We use these notations instead of to avoid ambiguity from in abstract interpretation. To construct a probabilistic abstract interpretation, →,− and # need to be considered. In this case : R → R is the forward propagation function. We lift : R → R up into probabilistic domain to b→e− : (R) → (R) which is
(+1) →=−−− − →(− () +→− ) where () is probability distribution of . Then from→− we can construct the abstract transformer # which is
#(+1) = #( ##() + #) In neural networks it is very common for a layer to be a composition of multiple functions. A typical case will be an afine transformation followed by a non-linear activation function. To obtain the abstract transformer, by definition of Moore-Penrose pseudo-inverse we can have abstract transformer for Af and abstract transformer for and by Proposition 1 we can have →−−
Af # = ′Af
# = →−−−′′− ′
(Af ∘ )# = Af # ∘ #
In probabilistic abstract interpretation, each possible value a neuron has is with a corresponding
probability. A prior distribution initialisation is needed to be given in input space. We use tensor
(
R− and we hav→e− : (R2) → (R2) In abstract domain, suppose we first only discuss the inputs in integers 11, 12 ∈ N such that in Fig. 2. In concrete domain we have : R and we set both activation functions as ReLU. We take the abstract domain to be {R+, 0, R− }, shown
Given a simplest MLP, with two layers and five neurons, with parameters shown below. We use notations to represent neuron values in layer . Let inputs to be real values such that 11, 12 ∈ [− 3, 3], 1 = ︂( 1 1
︂) ⎝ ⎛1 0 0 0 0 0 0 0 0 · · ·
⎜0 1 0 0 0 0 0 1 0 · · · .
. ... ⎟⎠⎟ ∈ R13× 49
(12, 22) = ( 1(11, 21) + 1)
(2) →=−−− −→−(−Af 1((11) ⊗ (21)))
11, 21 ∈ [− 3, − 2, − 1, 0, 1, 2, 3]
(11) = (21) = (3/7, 1/7, 3/7)
and initialise input space with uniform distribution, we have
and we can have
(2) = #(Af 1#((3/7, 1/7, 3/7) ⊗ (3/7, 1/7, 3/7))))
with probability 3/7, and zero probability to have other outcomes. To be more specific, we have
That is, after first layer, we will have (21 = 0, 22 = 0) with probability 4/7, and (21 ∈ R+, 22 ∈ R+)
product to combine all probability distributions for every single neurons in input space to form an
overall distribution representing the input layer. That is, for any two independent neurons,
(11 × 21) = (11) ⊗ (21)
where ⊗ is notation of tensor product. Therefore, the abstract transformer for the first layer 1# is
(Af ∘ )#(1) = #( 1#((11) ⊗ ... ⊗ (1)) + 1#)
(
# = ⎜⎜⎜⎜10 10 01 10 10 01 00 00 00⎟⎟⎟⎟ ∈ R9× 9
Then to make the case more general if we expand the input domain into reals 11, 12 ∈ R such that
we can have
and
lim R× (
Af 1# = ′Af 1 # = →−−−′′− ′ ′ ∈ l→im∞ R9× which classifies concrete points in Real space into nine categories of abstract domain, and which maps nine categories of abstract domain back to concrete domain. Hence we have ∈ li→m∞ R× 9 Af 1# = ′Af 1
→−− Therefore # = ⎜⎜⎜⎜10 10 01 10 10 01 00 00 00⎟⎟⎟⎟ ∈ R9× 9 (2) = #(Af 1#((1/2, 0, 1/2) ⊗ (1/2, 0, 1/2)))) = (︀ 0 0 0 0 1/2 0 0 0 1/2)︀ = ︂( 11
12)︂
1–14
(
That is, after first layer, we will have (21 = 0, 22 = 0) with probability 1/2, and (21 ∈ R+, 22 ∈ R+)
given and fixed. Let Convolutional neural network in principle is also a special case of fully-connected layers, except that many weights are zeros. We illustrate a simple example of applying abstract interpretation on convolutional layer. Let the input space ∈ R4× 4, the convolution filter ∈ R2× 2, and the output space then is ∈ R(4− 2+1)× (4− 2+1) = R3× 3. As a well-trained model, the weights of is already To express the convolution computation in formal mathematical expression, we can have where = ⎜ 0 0 0 0 0
11 12 Convolutional layers. For simplicty we let be zero vector, and let : R16 → R
9 We again concern the positiveness/negativeness, which in computer vision application is the darkness of pixels. The choice of convolution filter is typically a simple version of border detection filter. Following the ReLU function, we can let abstract domain be {R− , 0, R+}. In concrete domain we have (1, ..., 9) = ( (1, ..., 16) + ) To lift up to probability domain we hav→e− : (R16) → (R9) suppose we initialise the input space with uniform distribution over R, that is, () = (1/2, 0, 1/2).
() →=−−− − →(−Af ((1) ⊗ ... ⊗ (16))) Concretely we can see after convolution each entry has probability 1/2 to be negative and 1/2 to be positive. Therefore, applying ReLU function
() = (0, 1/2, 1/2) the output will have probability 1/2 to be 0 and probability 1/2 to be positive consequently, as ReLU will transform all negative values into zero.
In 2018, Gehr et al introduced 2, an analyzer which can automatically prove properties, especially safety and robustness, for convolutional neural networks based on classical abstract interpretation [28]. 2 has found a general way to define abstract domain and abstract transformer of diferent types of layers, including fully-connected layer, Convolutional layer and max-pooling layer. It defines suitable abstract domains and represents neural network layers as CAT functions, and hence defines abstract transformers which can be applied and computed on abstract elements in a very general way. The formal definitions and details can be found in [28].
It uses a shape of Zonotope as an abstract domain. In probabilistic framework, we can also follow this 2 → R 2 () = ︂( 2 − 1
︂) 0 1 with input space X expressed by zonotope 1 : [− 1, 1]3 → R2 :
1( 1, 2, 3) = (1 + 0.5 1 + 0.5 2, 2 + 0.5 1 + 0.5 3) followed by a ReLU transformation, shown in Figure 3 and 4. We illustrate this zonotope approximation ifrst in integer space and then generalise it into real space.
We first define abstract transformer for probabilistic framework,
#, together with Moore-Penrose
pseudo-inverse functions and in integer space. In concrete domain, we have overall 4 input points
= {(
4 ⎛ 1 1 1 1 1 1 1 ⎞ ⎜⎜ 01⎟⎟ ⎛ 1 ⎞
14 14 41 14 14 41 14 ⎜ 4 ⎟ 41 ((())) = ⎜⎜ 41 14 41 14 41 41 41 ⎟⎟ ⎜⎜0⎟⎟ = ⎜⎜ 41 ⎟⎟ ⎝ 144 144 441 144 144 441 144 ⎠ ⎜⎜⎜⎝ 4114 ⎟⎟⎟⎠ ⎝ 414 ⎠ 0 (42) (43) (44) (45)
The Integer space may be a special scenario. More generally we have to expand into Real space. Let’s ifrst look at the linear transformation from 1 to 2. Suppose in concrete domain we have N diferent points in arbitrary positions = {1, 2, ..., }, and is over-approximated by 1. If we lift up into probability space with uniform distribution we have () = { 1 , 1 , ..., 1 }. In abstract domain, particularly we can also see during linear transformation the distribution over input space does not change, where each point in X corresponds to a point in f(X) and vice versa. Therefore # : (R2) → (R2) Similarly the abstract transformer for ReLU is # : (R2) → (R2) # = →−−−′′− ′ = ′′′ and hence # : (R2) → (R2) and s.t. 1 ̸= 1 ∧ 2 ̸= 2, th→e−n−− − : (R2) → (R2) In ReLU transformation, we have to consider ( ()). We claim that if ∀, ∈ ( ()) Otherwise, suppose if ∃ and only ∃ a pair , ∈ ( ())( < ) s.t. 2 = 2, then →−− − − = ⎜⎜⎜⎜ .. .. .. 1. .. .. 1. .. .. .. ⎟⎟⎟⎟ ∈ R(− 1)× which can be obtained by eliminating the th row from identity matrix and assi→g−n−− − = 1. That is with all entries are 1 . Now we can let the same very large number lim→∞ to be the number of all real points contained in 2, so As it is linear transformation, again we hav→e− : (R2) → (R2) ∈ li→m∞ R× ∈ li→m∞ R× ′ = , ′ =
′′ = ′, ′′ = ′ with 2 in th entry. Then with an entry 1 in each column in corresponding position and other entries are all zeros. And we know in mathematics there are infinitely many points in Real space contained in 1, but we can regard this as a very large number and let it be lim→∞ . Then, we can have with an entry 1 in each column in corresponding position and other entries are all zeros. And ⎛ 1 ⎞
1 ⎜ ⎟ ⎜⎜ . ⎟⎟ ⎜⎜ . ⎟⎟ ⎜⎝ . ⎠⎟ 1 ⎛ 1 ⎞
1 ⎜⎜⎜ . ⎟⎟⎟ ⎜⎝ . ⎠⎟ 1 →−− − − ⎜⎜⎜⎜ .. ⎟⎟⎟⎟ = ⎜⎜⎜⎜ 2. ⎟⎟⎟⎟ ′′ ∈ li→m∞ R× (− 1) ′′ ∈ li→m∞ R(− 1)× We see that in Real space we encounter problem of infinity - since there are infinitely many points in any closed area in Real space, the dimensions of both input space and abstract element tends to infinitely large, and hence we are forced to handle vectors and matrices in dimension of infinity. We always wish to avoid this. A possible approximation is to use grids. That is, in former example, instead of considering space R2, we consider Z2, where gives size of grids to be chosen. For example, if we let to be 0.01, then the grid size is 0.01 × 0.01, which means we will have 100 × 100 points in a closed space bounded by a Box of size 1 × 1(regardless of points on boundary lines - we could have 101 × 101 points more specifically). In this way, each point represents the local probability of neighbour area, which still shows probability density distribution of the space. For convenience we always let − to be one of lines of grids, which will determine position of the whole grids. Now if we consider 1 in Z2, we have in total 30301 points in this abstract element. That is, recall the notation used in last subsection, instead of having lim→∞ points, we now have = 30301. Same as the input space in Z2. No matter what is, is finite and computable. Therefore we have : (0.01Z2) → (0.01Z2)
∈ R× = R30301× and so on for . As we know that any linear transformation in R2 is a bijective mapping, and Z2 ⊂ R2, hence any linear transformation in Z2 is also a bijective mapping. So we can have →− : ( Z2) → ( Z2)
→− () = Similarly 2 in ( Z2) contains 60401 points, so and so on for ′. Then we have # : ( Z2) → ( Z2) ′ ∈ R× = R60401×
# = →′− = ′ with all entries are 1− 1 . Therefore Obviously if ∃ exclusive pairs , ∈ ( ()) s.t. 2 = 2, then and if let → we have
Similar for # that we can now replace lim→∞ by finite and computable numbers. The
reason 2 takes zonotopes as abstract domain is that it is concerning robustness of a neural network,
and having a sound yet precise abstract element which over-approximates input space is a good way to
prove robustness. In probabilistic abstract interpretation, we usually have a diferent aim. Probabilistic
abstract interpretation concerns more about density distribution of input space and its change through
propagation of a neural network. Therefore, it is more meaningful to use other abstract domains to
reach the purpose. Following grid approximation, using a more sparse grids as an abstract domain is a
fair choice. In this context let 1 in 0.01Z2 be input space, i.e., = { ∈ 1 | ∈ 0.01Z2)}. Then we
let the abstract domain to be the space in Z2. We can choose diferent shapes of grids. As an instance,
we choose the squares. That is, we abstract 10,000 points in each 1 × 1 square in 0.01Z2 into one
single point in the centre of the square, and the value of probability of which is the sum of all values of
probabilities of 10,000 points. Say if we consider the coordinates ∈ (
In this section we give an example which takes MNIST hand-written digit classifier to illustrate analysis of probabilistic abstract interpretation on convolutional neural network.
We obtain an open-source dataset ‘MNIST Digit Dataset’ from Kaggle https://www.kaggle.com/competitions/digit-recognizer. The dataset contains about 40,000 handwritten images of digits. Each image is 28 pixels in height and 28 pixels in width, for a total of 784 pixels in total. Each pixel has a single pixel-value associated with it, indicating the lightness or darkness of that pixel, with higher numbers meaning darker. This pixel-value is an integer between 0 and 255, inclusive.
We design our model to be an eight-layer convolutional neural network, comprising of two 28 × 28 × 32 convolutional layers with 5 × 5 filter followed by a 2 × 2 max-pooling layer, and then another two 14 × 14 × 64 convolutional layers with 3 × 3 filter followed by a 2 × 2 max-pooling layer, and finally two dense layers, respectively. In total the network contains 887,530 parameters. We choose RMSprop as our Optimizer and categorical cross entropy as our Loss Function. In final epoch of training, our model achieved metrics 0.8917 and loss 0.3446.
An input image has 784 pixels and each pixel has 256 pixel values. So there are 256784 possible input images and we cannot exhaustively run them. We take grids approximation as our abstract domain. For each pixel, we classify its pixel-value into simply two categories, being value of 0 as dark and 255 as bright respectively. we also combine a neighborhood of 7 × 7 pixels with the same pixel-value, that is, we divide an image into 16 groups of pixels. A grid in this case is 16-dimensional, with each dimension has two choices of values. Therefore in total we have 216 grids in this approximation. It shows that for example the network will more likely recognize a bright top-left corner as a feature of digit ‘3’, and will more likely recognize a bright bottom-right corner as a feature of digit ‘2’ or ‘9’.
We can sample density initialisation of inputs from training set. In this approximation we have 216 grids. We approximate each of training image into corresponding grid and calculate sample probability of each grid with respect to the training set. The prediction of a high probability grid is more likely to occur. 4.5. Evaluation [28] gives an example of classical abstract interpretation analyzer to prove robustness against brightening attack on MNIST digit classifier. The analyzer is able to prove whether a network does correct classification under attack which perturbs an image by changing all pixels above a particular threshold to the brightest possible value. In this case, probabilistic abstract interpretation aims for diferent purpose. It (i)extracts features of the network and (ii)shows probability density flow of all possible inputs towards prediction.
We have discussed applying theory of probabilistic abstract interpretation on various kinds of neural network layers. We can see probabilistic abstract interpretation can give information on density distribution flow of possible inputs, which in particular cases is an advantage comparing to classical abstract interpretation analysis framework that is sometimes sound but not precise enough. During the discussion we can also see that problems remained in our approach. The examples we illustrated were mostly in low dimension, but in neural networks it is very common to be in very high dimensions. Secondly, we should discuss more kinds of abstract domains and abstract transformers, in addition to grids approximation, in order to fit diferent application situations. We remain these as future works.