Neural Network Verification for the Masses (of AI graduates)

TL;DR

This paper discusses the importance of verification in AI, highlights the challenges faced in integrating verification tools into AI education, and shares experiences from a new university lab engaging MSc students in verification projects.

Contribution

It introduces LAIV, a new lab at Heriot-Watt University, and reports on its efforts to incorporate verification into AI MSc programs, revealing challenges and future directions.

Findings

Verification tools face limitations due to programming language constraints.

Integrating verification into AI education presents practical challenges.

Future work aims to improve verification methods and teaching materials.

Abstract

Rapid development of AI applications has stimulated demand for, and has given rise to, the rapidly growing number and diversity of AI MSc degrees. AI and Robotics research communities, industries and students are becoming increasingly aware of the problems caused by unsafe or insecure AI applications. Among them, perhaps the most famous example is vulnerability of deep neural networks to ``adversarial attacks''. Owing to wide-spread use of neural networks in all areas of AI, this problem is seen as particularly acute and pervasive. Despite of the growing number of research papers about safety and security vulnerabilities of AI applications, there is a noticeable shortage of accessible tools, methods and teaching materials for incorporating verification into AI programs. LAIV -- the Lab for AI and Verification -- is a newly opened research lab at Heriot-Watt university that engages AI and Robotics MSc students in verification projects, as part of their MSc dissertation work. In this paper, we will report on successes and unexpected difficulties LAIV faces, many of which arise from limitations of existing programming languages used for verification. We will discuss future directions for incorporating verification into AI degrees.

Equations

$$potential(\vec{w},\vec{x})=z=(\sum _{i=1}^n{w}^{(i)}{x}^{(i)})+b$$

$$\vec{z}=W\cdot \vec{x}+\vec{b}$$

$$\vec{y}=\varphi (x)={\varphi }_L(...{\varphi }_2({\varphi }_1(\vec{x}))$$

$$min||\vec{r}|{|}_{p}suchthat\vec{y}=f(\vec{x})\ne f(\overrightarrow{x+r}),$$

$$S(x)=\{\begin{array}{ll}1,& \text{if }x\ge 0\\ 0,& \text{otherwise}\end{array}$$

Full text

Despite of the growing number of research papers about safety and security vulnerabilities of AI applications, there is a noticeable shortage of accessible tools, methods and teaching materials for incorporating verification into AI programs.

LAIV – the Lab for AI and Verification – is a newly opened research lab at Heriot-Watt university that engages AI and Robotics MSc students in verification projects, as part of their MSc dissertation work. In this paper, we will report on successes and unexpected difficulties LAIV faces, many of which arise from limitations of existing programming languages used for verification. We will discuss future directions for incorporating verification into AI degrees.

1 Introduction

AI applications have become pervasive: from mobile phones and home appliances to autonomous cars and stock markets – we are served by a range of intelligent algorithms, of which one prominent group is represented under an umbrella term neural networks. In the recent past, neural networks have been shown to match a human-level performance in specific domains such as speech recognition and natural language processing [5], image classification [9] and reinforcement learning [7], winning their prominent place among tools used in both research and industry.

It comes at little surprise then, that increasing number of undergraduate and postgraduate students choose AI and machine learning as their specialism. This global trend is reflected in the university degrees. In partnership with Edinburgh University, Heriot-Watt university is a home for National Robotarium111https://www.edinburgh-robotics.org/robotarium, the Doctoral Training Center *“Edinburgh Center for Robotics”*222https://www.edinburgh-robotics.org/, Robotics Lab333http://www.macs.hw.ac.uk/RoboticsLab/ and a number of large research projects. Over a dozen of AI and Robotics MSc degrees have been opened at Heriot-Watt, with specialisms ranging from general AI and Robotics degrees to specialised degrees such as “Robot Human Interaction” and “Speech with Multimodal Interaction”. Students undertake courses covering both symbolic and statistical AI, with topics ranging from AI planning languages to Bayesian learning and deep neural networks.

With the growing number of AI applications, there is also a growing concern that only a small proportion of them are verified to be trustworthy, safe and secure. This concern stimulated recent research in AI verification generally and neural network verification in particular. Research in neural network verification splits into two main groups of research questions:

• •

Concerning properties of learning algorithms in general: e.g. how well does a given learning algorithm perform? do trained neural networks generalise well to classify yet unseen data? The answers include proofs of properties of generalisation bounds, equality of neural networks, properties of neural network architectures. Good examples are [1, 2]. Usually, these verification projects are conducted in interactive theorem provers (ITPs), such as Coq [4], as they benefit from Coq’s rich higher-order language and well-developed proof libraries. Unfortunately, Coq as a language does not offer machine learning support comparable to e.g. Python. Also, compared to automated provers, proof automation is rather limited in ITP.

• •

Concerning specific neural network applications or their specific deployment: e.g. given a trained neural network, is it robust to adversarial attacks [6, 17]?

Adversarial attacks in this setting are usually given by adversarial examples, which are in turn given by non-random small-scale perturbations of an input data on which the neural network was trained. These perturbations lead the neural network to output a wrong classification or regression result [18].

Example 1 (Adversarial attack)

Figure 1 shows how a seemingly insignificant perturbation to the original image causes neural network to missclassify the image. It uses the MNIST data set [19], a famous benchmark data set for hand-written digit recognition.

Adversarial attacks were successful at manipulating all kinds of neural networks, including recurrent [14] and convolutional [15] neural networks. In addition, adversarial examples were successfully crafted for all domains in which neural networks have been applied. See e.g. [16] for a comprehensive survey.

The second kind of verification projects usually uses Python for the machine learning part and SMT solvers (such as Z3 [13]) for verification component, and often relies on Python’s Z3 API. Thanks to this combination, these projects benefit from both comprehensive machine learning libraries of Python and the automation offered by Z3. Among disadvantages of this framework is fragility of code conversion between Python and Z3, and limitations on the generality of neural network properties that can be expressed in this setting.

Despite of the growing volume of research and the growing industrial awareness, verification is not routinely taught as part of AI and Robotics BSc or MSc degrees. As a result, postgraduate and undergraduate students increasingly choose verification-related subjects for their dissertations. Thus, in the 2018-2019 MSc intake, we saw a surging interest from AI and Robotics MSc students in taking up verification projects as part of their MSc dissertations. LAIV – Lab for AI and Verification444LAIV webpage: www.LAIV.uk – was founded in order to support AI, Robotics and Data Science MSc students venturing into verification field for their dissertations. It provides additional support in the forms of seminars and reading groups and thus compensates for absent verification courses in the MSc degrees.

In this paper, we reflect on the design space of programming languages and tools available for AI and machine learning specialists and students who want to master neural network verification in a lightweight manner, i.e. not as part of their main specialism. Starting with some necessary background definitions in Section 2, we proceed with introducing, by means of an easy running example, three verification methods:

• •

automated verification of neural networks via Python’s Z3 API (Section 3),

• •

interactive and functional approach to neural network verification in Coq (Section 4), and

• •

hybrid approach via $F^{*}$ [11], a novel functional language with capacity to delegate some theorem proving to Z3 (Section 5).

We reflect on advantages and disadvantages of these approaches, both in terms of verification methodology and student experience. Finally, in Section 6 we conclude and outline some future directions.

2 Background: Neural Networks and their Robustness

The standard feed-forward neural network (also called multi-layer perceptron) is composed of an input layer, an output layer and a varying number of hidden layers (Figure 2). Each layer consists of several elements called neurons. Each neuron’s potential is the weighted sum of its inputs from the previous layer plus a bias $b\in\mathbb{R}$:

[TABLE]

$w^{(i)}$ denotes the $i$-th component of the weight vector associated with the $i$-th component of the input vector $\vec{x}$. The $potential(\vec{w},\vec{x})$ (also denoted as $z\in\mathbb{R}$) serves as in input to the activation function $\phi(\cdot)$. The activation of the neuron is given by $a=\phi(z)\in\mathbb{R}$. So, a single neuron in any layer takes the two vectors $\vec{w}$ and $\vec{x}$ as inputs, adds a bias $b$ to it and passes the result through the activation function. Since each layer consists of a varying number of such neurons, the outputs of a single layer can be written as

[TABLE]

where $\cdot$ denotes the standard matrix multiplication, $\vec{z}\in\mathbb{R}^{m}$, $\vec{x}\in\mathbb{R}^{n}$, $b\in\mathbb{R}^{n}$ and $W\in\mathbb{R}^{m\times n}$. The values returned by the last layer, the output layer, are denoted by $\vec{y}$. In the classification setting described here, $\vec{y}\in\mathbb{R}^{c}$, where c denotes the number of classes. Then a neural network can be represented as:

[TABLE]

where $\phi_{i}$, $i=1,...,L$, denotes the activation in the $i$-th layer of the neural network and $\vec{x}$ denotes the input to the first hidden layer; see also Figure 2.

Research from [18] shows that neural networks are vulnerable to adversarial attacks. These are non-randomly perturbed inputs to the network so that the wrong class label is predicted, see Figure 1. Regardless of the nature of the attack all methods for generating adversarial examples try to change the output $\vec{y}$ of a neural network. For example, in the setting of image classification, this is done by adding a vector $\vec{r}\in\mathbb{R}^{n}$ to the input $\vec{x}\in\mathbb{R}^{n}$ of the neural network, while keeping $||\vec{r}||_{p}$ as small as possible with respect to a user specified $p$-norm555$p$-norm: $||\vec{x}||_{p}=(\sum_{i=1}^{n}||x_{i}||^{p})^{\frac{1}{p}}$:

[TABLE]

where $\vec{y}$ denotes the true class of the input $\vec{x}$ and $f(\cdot)$ denotes the neural network in general.

In the following sections, we will illustrate the available verification methods using a toy running example – the famous “and-gate” Perceptron by [12]:

Example 2 (Perceptron)

The training set is given by the truth values of the logical connective and, see Figure 3.

The Perceptron is trained to approximate a suitable linear function, e.g. $out_{and}(A,B)=b_{and}+w_{A}\times A+w_{B}\times B$, given numbers $A$ and $B$ as inputs. E.g. $-0.9+0.5A+0.5B$ would be a suitable solution. Sometimes with the Perceptron, we use an activation function $S$ given by a threshold function:

[TABLE]

In the next few sections we assume a verification scenario in which we prove that, subject to certain constraints on values of $A$ and $B$, the Perceptron will output “correct” value for and. For example, we may want to prove that it always outputs $1$, when the input values of $A$ and $B$ are greater than $0.7$ (the $0.3$ slack will model the region in which an adversarial manipulation may occur).

3 Z3 API in Python and Its Limitations

Typically, AI students are well-versed in Python. Thus, the most accessible method of neural verification for them is the method based on Z3 API in Python. It can give rather quick results, without adding an additional burden of learning a new programming language. Learning Z3 syntax is a hurdle but not a major challenge, as first-order logic is usually taught in AI courses. Moreover, Z3 API can be used irrespective of the Python library in which the students implement their networks. The Python/Z3 verification workflow will generally comprise of the following steps:

• •

Implement the neural network in Python.

Example 3

We define in Python the Perceptron given in Figure 3, and use the and training set to train it; see the code snippet in Figure 4. Python computes a suitable Perceptron model with weights

[-0.18375655 0.19388244 0.19471828],

i.e. computing $b_{and}=-0.18375655$, $w_{A}=0.19388244$, and $w_{B}=0.19471828$.

• •

Prove it is robust for a given output class:

Define its robustness region: e.g., assume $1$ is the desired output given the input array that contains real values in the region $[0.7;1.5]$; cf. conditions cond1 and cond2 in Figure 5. 2. 2.

Define a step function (“the ladder”) to generate a finite number of adversarial examples in this region (the finiteness condition is needed to ensure Z3 termination). See e.g. lines 9-13 in Figure 5. 3. 3.

Prove that the ladder is “covering”, i.e. guarantees that no adversarial example exists in this region if no adversarial example is found for the ladder. These proofs are “pen and paper”. 4. 4.

Take the set of adversarial examples generated by Z3 and run them through the Perceptron. If no misclassification is detected – we have proven the Perceptron robust for the given output, region and ladder.

The shown toy example code can be adapted straightforwardly for arbitrary complex neural network implementation. Indeed, exercises that follow this simple methodology will be introduced in the academic year 2019-20 in the standard course of Data Mining and Machine Learning for MSc students with AI specialisms at Heriot-Watt University. Simplicity of use is thus the first benefit of choosing Z3 Python API.

This methodology has been used in complex extensions, including e.g. [6, 17]. There, deep convolutional neural networks were verified via Z3 Python API, and featured generation of adversarial examples using more sophisticated Z3 conditions, that describe in finer detail the functions used in the hidden layers. Potential for use in state-of-the-art, industrial scenarios is thus the second benefit of this verification methodology.

LAIV already has experience of supervising MSc projects [8, 10] that are devoted to the systematic study of properties of neural networks considered in [6]. The Deep Learning Verification (DLV) software that accompanies [6] is complex enough to provide sufficient challenge for strong MSc students in their independent projects. For the same reasons, such projects may not be suitable for an average student who may be easily discouraged by the need to debug and understand the complex Python/Z3 code.

At the same time, we see several drawbacks, in the long term, for taking Z3-Python API approach as the main and only methodology for teaching neural network verification:

• •

Z3 has no direct access to Python’s objects, which is due to a big difference in syntax and semantics of Python and Z3 as programming languages.

Example 4

We return to the Perceptron defined in Example 2. Looking at lines 1-13 of Figure 5 we first see the code that defines constraints for Z3 models and does not directly refer to the Perceptron defined in Figure 4. Lines 15-19 pass these constraints to Z3 and obtain the model. Then lines 21 and 22 show the backwards translation of Z3 models into floating-number vectors that are acceptable by Python. The rest of the code in that Figure merely tests the generated vectors using Python’s objects.

Such methodology, irrespective of sophistication of the neural networks and the verification conditions involved, cannot in principle be extended to verification scenarios that state and prove properties of the implemented neural networks directly. Therefore, the use of Z3 API in Python will always be restricted to first generating some data (subject to constraints) via Z3, and then testing that data using the Python’s objects. Such style of verification, due to the indirect connection between the object we verify and the verification conditions we formulate, will itself be prone to errors666Which will very likely occur rather often if this becomes a routine methodology used by masses of AI specialists that graduate from the universities..

• •

This methodology will inherently suffer from fragility of conversion between symbolic objects that represent real numbers in Z3 and Python’s floating point numbers.

Example 5

Changing the line 21 in Figure 5 to

r = [simplify(m.evaluate(X[i])).as_decimal(10) for i in range(2)]

will cause an error:

ValueError: could not convert string to float: ’0.9500000000?’

Ultimately, if this methodology is used in mass production, all sorts of bugs such as above may become an impediment to both soundness and productivity of neural network verification.

• •

Finally, the penultimate item in the methodology described above, the “pen and paper” proof of adequacy of the chosen region and ladder, will not scale well for industrial uses. Manual proofs require an additional production time and are themselves prone to error777The pen and paper proof is missing in  [6]..

4 ITP Approach to Neural Network Verification

An alternative approach, that would resolve all three shortcomings identified in the previous section, is the ITP approach, as advocated in e.g. [1, 2]. It amounts to first defining neural networks directly in Coq, and then proving properties about these definitions directly, thus avoiding programming in Python at the verification stage. Automating translation from Python classes into Coq definitions at the pre-processing stage is possible, and was done in [1]. This translation phase is however not an essential part of the verification process.

Example 6

Figure 6 shows the Perceptron (of Example 2) defined in Coq as a record type. We use notation that is very close to [2]. We note that, in addition to direct declaration of types for outputs, weights, bias and potential, the type already allows us to also assert some additional properties: e.g. that the output must be binary, bias must be positive, and weights must be in range $[-1,1]$, the latter is defined by a boolean function WeightInRange. The types nat and Q are natural and rational numbers respectively. Rational numbers are taken here instead of the real numbers, due to complications one would need to face when working with real numbers in Coq (cf. e.g. [3]).

The following is an example of a concrete Perceptron (of type Neuron) that satisfies the above definition:

⬇

1Lemma Perceptron : Neuron.

2Proof.

3 apply (MakeNeuron [1%nat] [2#10; 2#10] (2#10) 1); simpl; auto.

4Qed.

It has output given by the list $[1]$ (this corresponds to $out_{and}$ of Example 2), weights $w_{A}$ and $w_{B}$ given by $[\frac{2}{10},\frac{2}{10}]$, bias $b_{and}$ – by ${\frac{2}{10}}$, and potential – by $1$. This roughly corresponds to the Perceptron computed by Python in Example 3, subject to rounding of Python floating numbers to rationals. Note that $b$ must be positive according to the Neuron record, the subtraction effect is incorporated via a slightly different threshold function computing $out_{and}$ (this is purely a matter of convenience).

One can then state and prove lemmas of varying degree of generality (note that the Neuron type of Figure 6 defines Perceptron’s in general, rather than any concrete Perceptron). For example, one may want to prove that, feeding any input of the correct type to a Perceptron, we always get the next output within a permissible range. Figure 7 shows a function that computes a neuron’s potential, and defines the notion of the “next output”. The Lemma then has a rather simple statement and proof [2]:

⬇

1Lemma NextOutput_Bin_List: forall (N: Neuron) (Inputs: list nat),

2 Bin_List(Output N) -> Bin_List (NextOutput N Inputs::Output N).

3Proof.

4 intros. simpl. split.

5 - unfold NextOutput. destruct (Qle_bool (Bias N) (NextPotential N Inputs)).

6 + simpl. reflexivity.

7 + simpl. reflexivity. - apply H.

8Qed.

To summarise the benefits of ITP approach to neural network verification:

• •

it makes definitions of neural networks, and all associated functions, fully transparent not just for the software engineer who works with the code, but also for the type checker, that certifies soundness of the code;

• •

it ensures that when proving properties of neural networks, we directly refer to their implementation in the same language as opposed to the indirect “testing” style of verification that we had to resort to in Python and Z3.

• •

we no longer need any “pen and paper proofs” in the verification cycle, as Coq’s language is rich enough to state lemmas of arbitrary generality;

• •

finally, we no longer have any problems with intra-language translation and type mismatch that was pertinent to the Z3 – Python API approach.

The Coq approach to neural network verification also has drawbacks, especially if we consider taking it as the main verification tool for AI and Robotics students. Firstly, there is a serious overhead arising from the need to learn Coq from scratch. For a student whose first and main programming language is Python, Coq has an unusual syntax, and requires a non-trivial degree of understanding of the associated logic and type theory for successful proof completion. If one day Coq and similar provers are introduced as compulsory element of AI degrees, this would become feasible. As it stands, immediate introduction of Coq-based neural network verification in classes or projects is not realistic.

Among other pitfalls of this approach are:

• •

real numbers are not as accessible in Coq as floating numbers are in Python. The rational numbers as used in all the running examples of this section are not a feasible substitute for real numbers in the long run, as many machine learning algorithms rely on real-numbered differentiable functions. Even a more sophisticated approach of [1] shies away from real numbers, an thus has to claim only working with “quantised” neural networks.

• •

Although Coq is in principle a programming language rather than just a prover, actual computations with its functions are problematic.

Example 7

Let us try to use the Perceptron definition given in Example 6, and define its next outputs given the input vector $[1,1]$:

⬇

1Definition Pp : nat :=

2 NextOutput Perceptron [1%nat; 1%nat].

Now trying to actually compute the number (using the command Compute (Pp).) gives a few hundreds lines of an output evaluating Coq functions (a snippet is shown in Figure 4), – something a Python programmer will be baffled with!

• •

An instance of the same problem of function evaluation arises in trying to prove adversarial robustness of individual neural networks (in the style of Python-Z3 approaches). Such verification will inevitably depend on evaluating functions and computing outputs of the networks.

Example 8

Continuing with the same Coq file, and attempting to prove the correctness of the output of the Perceptron defined in Example 6 given the input $[1,1]$ will result in the following lemma:

⬇

1Lemma sound: forall x y : nat, x = 1%nat -> y = 1%nat -> (NextOutput Perceptron [x ; y]) = 1%nat.

Its direct proof by simplification is unfortunately infeasible, for the reasons explained in Example 7.