Lab3: Neural Network Verification

This lab provides you basic understanding of neural network verification (NN-Verification).

Goals:

• understand NN-Verification as a tool
• know how to design specifications and use NN-Verifiation
• have a hands-on experience of running NN-Verification

Non-goals:

• this lab does not cover verification internals (e.g., verification algorithms)
• this is not a verification performance test (the verification you will run is not the fasest)

Section 0: Background

A motivating example

(a) People found that adding some noise can fool a NN:

(This image is borrowed from this blog)

(b) for this NN, the verification can check:

• given a NN and an image (the panda), is it true that...
• ...adding a small amount of noise...
• ...will not affect the NN's output (i.e., the predicated image label like "panda").

We can formally define the above property:

• given a NN (call it $f$) and an image (the panda), is it true that...
• ...$\forall x$ (for all images) that are generated by adding a bounded noise
  (e.g., only changing each pixel's RGB color channel at most by $\epsilon$) to the panda image...
• ...we always have $f(x) \to$ "panda" ($f$ is the NN).

(c) NN Verification guarnatees

given the above wanted property (which we call a specification) and the NN (the $f$), a NN verification can either say "pass", meaning the NN satisfies the property; or "fail", meaning the NN violates the preperty.

Section 1: Getting started

This is the same as Lab2. If you have done this, you can activate conda and skip this step.

Step 1: environment preparation

1. install conda or miniconda (see here)
2. $ conda create -n cs7670 python=3 : create an conda environment called "cs7670"
3. $ conda activate cs7670 : activate this environment
4. $ pip install d2l==1.0.0a1 : install necesssary packages from d2l (see d2l.ai)
5. $ pip install torch torchvision termcolor : install PyTorch and a color printing package
6. $ conda install ipykernel : install IPython kernel

Step 2: Lab3 preparation

• Click the GitHub Classroom link that I sent to you to clone the lab.

• Open a Linux terminal.

• Clone Lab repo to your local machine.

  $ cd ~  
  

$ git clone git@github.com:NEU-CS7670-labs/lab3-.git lab3

• check contents:

  $ cd ~/lab3; ls  
  // you should see
  adversarial_img_1.png   mnist.png   nn-verification.ipynb   nnveri.png  verifier.py
  
  

• start your lab3:

    $ cd ~/lab3 
    $ conda activate cs7670    # if you haven't
    $ jupyter-notebook
  
  

• This should open your default browser. Click the file named Lab3.ipynb.

Step 3: confirm environment works

from termcolor import colored

def info(msg):
    assert isinstance(msg, str)
    print(colored(msg, "magenta", attrs=['bold']))

info("Active environment should be cs7670:")
! conda info | grep 'active env'

Section 2: A toy problem

import math
import numpy as np
import matplotlib.pyplot as plt
import random
%matplotlib inline

2.1 The problem

The overall problem is to distinguish if a point (x1,x2) is in a circle. The center of the circle is (0.5, 0.5); the radius is 0.5.

Formally, "if inside the circle" is defined as if $(x_1-0.5)^2 + (x_2-0.5)^2 \le 0.5^2$.

We define a function that tells if a point is inside the circle.

def inside_circle(x):
    assert len(x) == 2
    return 1 if (x[0]-0.5) ** 2 + (x[1]-0.5) ** 2 <= 0.25 else 0

# to visualize the circle
def draw_circle():
    plt.axes()
    circle = plt.Circle((0.5,0.5), 0.5, fc='white',ec="black")
    plt.gca().add_patch(circle)
    plt.gca().set_aspect('equal')
    plt.xlim(0,1.5)
    plt.ylim(0,1.5)

draw_circle()

2.2 Train a NN to learn the problem

You will train a NN:

• given a point (x1,x2),
• your NN should return a score (a float).
• If the score is $\ge 0.5$, we say (x1,x2) is inside the circle;
• otherwise, we say it is outside.

# below we generate the training data randomly
# The training data include both positive and negative data

def gen_data(num):
    xs = []
    for i in range(num):
        x1 = random.uniform(0, 1.5)
        x2 = random.uniform(0, 1.5)
        xs.append((x1, x2))
    return np.array(xs)

xs = gen_data(2000)  # TODO: feel free to generate more data for training

# to visualize the circle (ground truth) and training data

def draw_data(xs):
    plt.scatter([x[0] for x in xs], [x[1] for x in xs], marker='.')
    
draw_circle()
draw_data(xs)

Exercise 1: train a feed-forward neural network with ReLU

• We will follow Lab2 training procedure (namely, d2l OO style)
• You should only use Linear and ReLU to define your network (a constraint introduced by our verifier)
• Notice that gen_data will only generate xs; you need to run insdie_circle() to get ground truth labels
• Feel free to generate more training data if you wanted/neede.
• At the end of the day, the expectation is a NN that takes a tensor of size 2 (the point (x1,x2)) and produces a tensor of size 1 (the score).

from d2l import torch as d2l
import torch
from torch import nn

class CircleData(d2l.DataModule):  #@save
    
    def __init__(self, xs, y_fn, batch_size=100):
        super().__init__()
        self.save_hyperparameters()
        
        self.batch_size= batch_size
        self.n = len(xs)
        ys = [y_fn(x) for x in xs]
        self.X = torch.as_tensor(xs, dtype=torch.float32)
        self.Y = torch.tensor(ys, dtype=torch.float32)
        self.dataset = torch.utils.data.TensorDataset(self.X, self.Y)
        
        
    def get_dataloader(self, train):
        return torch.utils.data.DataLoader(self.dataset, self.batch_size, shuffle=train)

class CircleModle(d2l.Module):
    
    def __init__(self):
        super().__init__()
        self.save_hyperparameters()

        # TODO: your code here

        
    def loss(self, y_hat, y):
        # TODO: your code here
        
       
        
    def configure_optimizers(self):
        # TODO: your code here
   

# Notice: below I follow d2l stype; feel free to remove and use whatever you like to train the model
# TODO: tuning hyperparameters for better accuracy

model = CircleModle()
data = CircleData(xs, inside_circle)  # create dataset
trainer = d2l.Trainer(max_epochs=100) # create trainer

trainer.fit(model, data)

# we will have your **trained** pytorch network in "nn_circle"
# TODO: replace None to your model
nn_circle = None 

2.3 Specification: if NN results make sense

Q: what's the "expected behavior"---which we call a specification---of this toy problem?

It should something like, "if a point is inside the circle, the NN should always return a value >=0.5".

Two partial correctness properties can be:

1. $\forall x \in ([0.7, 0.85], [0.7, 0.85]) \implies y\ge0.5?$ $y$ is the output of the NN.

2. $\forall x \in ([0.86, 0.9], [0.86, 0.9]) \implies y<0.5?$

(visually, this is what we mean:)

def draw_spec(x1_bound, x2_bound):
    plt.plot([x1_bound[0], x1_bound[1], x1_bound[1], x1_bound[0], x1_bound[0]],
         [x2_bound[0], x2_bound[0], x2_bound[1], x2_bound[1], x2_bound[0]])
    
draw_circle()
draw_spec([0.7,0.85], [0.7,0.85])
draw_spec([0.86,0.9], [0.86,0.9])

2.4 Check by testing

One approach is that we can test the two properties by

1. random generating many data points in side the targeted area
2. test if the NN output is what we expect

You will first try this approach:

# below are some code to randomly generate testing data

def gen_test(num, x1_bound, x2_bound):
    xs = []
    assert x1_bound[0] < x1_bound[1] and x2_bound[0] < x2_bound[1]
    for i in range(num):
        x1 = random.uniform(x1_bound[0], x1_bound[1])
        x2 = random.uniform(x2_bound[0], x2_bound[1])
        xs.append((x1, x2))
    return np.array(xs)

def net_test(net, testing_data):
    counterexamples = []
    pred_ys = list(map(net, torch.as_tensor(testing_data, dtype=torch.float32)))
    ys = [inside_circle(x) for x in testing_data]
    for i,x in enumerate(testing_data):
        if (pred_ys[i].data >= 0.5) != (ys[i] >= 0.5):
            counterexamples.append(x)
    return counterexamples
           

def check_ground_truth(x):
    with torch.no_grad():
        ret = nn_circle(torch.tensor(x))
    gt = inside_circle(x)
    info(f"net->{ret}; ground truth->{gt}")

Test A: check cases within circle

# this is testing data for one property
testing_data = gen_test(10, (0.7,0.85), (0.7,0.85))

# to visualize testing data
draw_circle()
draw_data(testing_data)

# testing!
ret = net_test(nn_circle, testing_data)
if len(ret) == 0:
    info("Pass! no violation found.")
else:
    info(f"Failed! failed cases: {len(ret)}/{len(testing_data)}")
    print(ret)

check_ground_truth([0.7, 0.7])
check_ground_truth([0.85, 0.85])

Test B: check cases outside circle

# this is testing data for the other property
testing_data = gen_test(10, (0.86,0.9), (0.86,0.9))

# to visualize testing data
draw_circle()
draw_data(testing_data)

# testing!
ret = net_test(nn_circle, testing_data)
if len(ret) == 0:
    info("Pass! no violation found.")
else:
    info(f"Failed! failed cases: {len(ret)}/{len(testing_data)}")
    print(ret)

check_ground_truth([0.86, 0.86])
check_ground_truth([0.9, 0.9])

Some questions:

• What did you see? Does your NN pass all tests?
• If it passes, try generate more test cases and see if it still passes.
• Do you have conficence that the two properties always hold for all possible testing data?
• How can we be sure that the properties hold then? (the anwer, of course, is NN-Verification)

Comments:

• the yes/no question can be hard to learn
• if your net doesn't work well, try to use a different "ground truth" function:
  • modify inside_circle function
  • return some continuous values that have a flavor of telling the distances from the center of the circle
  • still, the return values should give >=0.5 for points within the circle; <0.5 for others
• (we don't expect you to train a perfect net; if you can, that's awesome!)

Section 3: Introducing NN-Verification

# install the needed verification tools
!pip install auto-LiRPA
!pip install tqdm
from IPython.display import clear_output
clear_output()

from verifier import verify

3.1 Our verification interface: verify(net, x_spec, y_spec)

Next, we use NN-Verification to check if the network truely satisfies the expected properties. Here is the interface of the verificaiton:

ret = verify(net, x_specs, y_specs, counterexamples=None)

• inputs:
  • net: your pytorch network
  • x_spacs: the inputs' specification in the format of [ [x0_lb, x0_ub], [x1_lb, x1_ub] ] where x0_lb represents lowerbound for the first dimesion of input x (x0) and _ub means upper bound.
  • y_specs: the outputs' specification in the form of [ [y0_lb, y1_ub] ] (when the output of our NN is 1-dim)
  • counterexamples: if you want to know how your networks fails, you should call verify(..., counterexamples=list); the failed cases are stored in counterexamples.

Below is an simple example:

x_specs = [(0.45,0.55), (0.45,0.55)]
y_specs = [[0.5, 10]]         # y>=0.5, "10" here is an arbitrary large number

draw_circle()
draw_spec(x_specs[0], x_specs[1])

cases = []
ret = verify(nn_circle, x_specs, y_specs, counterexamples=cases)
print(ret)
print(cases)

NOTICE:

• The verifier we use is a toy one that I (Cheng) created for this lab.
• So, there might be bugs (the reason why we need "verification"!).
• When you encounter error messages from verifier, plesae let me (c.tan@northeastern.edu) know.
• You will also realize later that this verifier lacks supports some common specifications (you will see what I mean in Exercise 4)

3.2 Verification results: "verified" or "unsafe"?

What's the output of the verification?

• If it is "verified", convince yourself that the network give >=0.5 for all points within x_specs (probably by trying many inputs)
• If it is "unsafe", verification will give some counterexamples. Try to inference them to convince yourself that the net indeed fails the specification

# TOOD: try inference and convince yourself
check_ground_truth([0.5, 0.5])

Exercise 2: verify if the two specifications pass

Next, let's check the two properties:

1. $\forall x \in ([0.7, 0.85], [0.7, 0.85]) \implies y\ge0.5?$ $y$ is the output of the NN.

2. $\forall x \in ([0.86, 0.9], [0.86, 0.9]) \implies y<0.5?$

Verification A: check cases within circle

x_specs = [(0.7,0.85), (0.7,0.85)]
y_specs = [[0.5, 10]]          

draw_circle()
draw_spec(x_specs[0], x_specs[1])

# Check if this specification hold for your net
# TODO: your code here

# TODO: test if your fail any case
check_ground_truth([0.7562, 0.7562])

Verification B: check cases outside circle

x_specs = [(0.86,0.9), (0.86,0.9)]   
y_specs = [[-10, 0.5]]           

draw_circle()
draw_spec(x_specs[0], x_specs[1])

# Check if this specification hold for your net
# TODO: your code here

# TODO: test if your fail any case
check_ground_truth([0.8600, 0.8600])

Section 4: robustness of an image classification network

4.1 MNIST dataset

MNIST is a dataset of handwritten digits.

MNIST has:

• input or images (the x): an array (tensor really) of size (28,28)
  • meaning, there are 28x28 cells
  • each cell is a foat number
  • the meaning of each cell is a gray level for a pixel
• output or label (the y): an integer $\in [0,9]$, representing which digit the image represents

MNIST examples are:

(the above fig is borrowed from this page)

# install package
!pip install torchvision
clear_output()

# prepare MNIST dataset
import torchvision

# download MNIST dataset
class MNISTData(d2l.DataModule):  #@save
    
    def __init__(self, batch_size_train, batch_size_test):
        super().__init__()
        self.save_hyperparameters()
        
        # training dataset
        self.train_loader = torch.utils.data.DataLoader(
          torchvision.datasets.MNIST('/tmp/', train=True, download=True,
                                     transform=torchvision.transforms.Compose([
                                       torchvision.transforms.ToTensor(),
                                       torchvision.transforms.Normalize(
                                         (0.1307,), (0.3081,))
                                     ])),
          batch_size=batch_size_train, shuffle=True)
        
        # should be used for test, but we used for validation (for simplicity)
        self.test_loader = torch.utils.data.DataLoader(
          torchvision.datasets.MNIST('/tmp/', train=False, download=True,
                                     transform=torchvision.transforms.Compose([
                                       torchvision.transforms.ToTensor(),
                                       torchvision.transforms.Normalize(
                                         (0.1307,), (0.3081,))
                                     ])),
          batch_size=batch_size_test, shuffle=True)
        
        
    def get_dataloader(self, train):
        if train:
            return self.train_loader
        else:
            return self.test_loader
        
mnist_data = MNISTData(batch_size_train = 64, batch_size_test = 1000)

# Now, let's take a look at MNIST's input and output
def plot_mnist(x):
    plt.imshow(x.view(-1,28,28).numpy().squeeze(), cmap='gray_r');
    
dataiter = iter(mnist_data.train_loader)
images, labels = dataiter.next()

plot_mnist(images[0])
print(labels[0])

4.2 classifying MNIST

Exercise 3: train a net to classify MNIST

Next, let's train a NN that recognizes different nubmers! Again,

• we will follow Lab2 training procedure (namely, d2l OO style).
• You should only use Linear and ReLU to define your network (a constraint introduced by our verifier)

class MNISTModle(d2l.Module):
    
    def __init__(self):
        super().__init__()
        self.save_hyperparameters()
        
        # [TODO: your code here]
        # self.net should takes in 
        #  a 1D-tensor of 784 and 
        #  produces 1D-tensor of size 10
        self.net = None

        
    def forward(self, X):
        # notice that we need to transform 2D-tensor to 1D-tensor
        # namely, (28,28) => (784)
        y = nn.Flatten()(X)
        y = self.net(y)  # you should define this self.net
        y = nn.Softmax(dim=1)(y)
        return y
        
    def loss(self, y_logits, y):
        # [TODO: your code here]
        # [hint: check out NLLLoss in pytorch]
  

    def configure_optimizers(self):
        # [TODO: your code here]
 

# Tain!
mnist_model = MNISTModle()  # create your model
# dataset is  mnist_data 
trainer = d2l.Trainer(max_epochs=10) # create trainer

trainer.fit(mnist_model, mnist_data)

4.3 Test your MNIST net

Notice: this is not a comprehensive testing on the testing dataset (as in classic ML procedure)

dataiter = iter(mnist_data.test_loader)
images, labels = dataiter.next()

plot_mnist(images[0]);
print(labels[0])

test_num=10
for i in range(test_num):
    y_hat = mnist_model(images[i]).argmax(1)
    info(f"Your pridiction is {y_hat} ==? {labels[i]}")

4.4 Robustness of a MNIST net

For image classification problems, we call a network "robust" when changing the input image slightly will not affect the output (the label) of the network.

For example, your MNIST net should not change labels from "1" to "9" because of a minor change on one pixel.

Next, let's see if your trained net is robust.

# focus on one image
dataiter = iter(mnist_data.test_loader)
images, labels = dataiter.next()
the_chosen_one = images[0]
ground_truth = labels[0]

plot_mnist(the_chosen_one)
print(ground_truth)

# image robustness
x = nn.Flatten()(the_chosen_one)

def perturb_one_pixel(pixel_pos, delta):
    assert pixel_pos >=0 and pixel_pos < 28*28
    assert delta > 0
    
    x_lower_bound = torch.clone(x)
    x_lower_bound[0,some_pixel] -= delta   # we change the value of one pixel on the pic
    x_upper_bound = torch.clone(x)
    x_upper_bound[0,some_pixel] += delta   # we change the value of one pixel on the pic
    
    return x_lower_bound, x_upper_bound

x_lb, x_ub = perturb_one_pixel(5, 0.5)

# visualize the difference
plot_mnist(x_ub)

# testing if net still works
info(f"lower bound image:  {mnist_model.net(x_lb).argmax(1)}")
info(f"upper bound image:  {mnist_model.net(x_ub).argmax(1)}")

Excersize 4: verifying MNIST robustness

Next, you will verify that:

• all images that in-btween x_lb and x_ub will be predicted correctly

(a) prepare x_specs

# you need to define x_specs
# notice that for MNIST, the x_specs should be 
#  - a list of size 784
#  - each element in the list is a 2-tuple with the (lower bound, upper bound) of this pixel
#  - in fact, all pixels' lower/upper bound will be the same, **except** the pixel your perturb
# TODO: your code here
# [hint: "torch.transpose()" and "tensor.tolist()" can be useful]

# print x_specs
assert isinstance(x_specs, list)
assert len(x_specs) == 28*28
assert len(x_specs[0]) == 2
x_specs

(b) prepare y_specs

For robustness, the canonical output specification should be:

• given the net output is a 10D-tensor (the logits) y,
• the ground truth label (say, 6) should always have the largest value...
• ...namely, y[6] > all others or y.argmax(1) == 6

However, our verify() interface does not suppor such expression.

So, you will use an interactive approach to make sure your network is robust for x_specs. It works as follows:

1. You will inference the lower and upper bound inputs (the x_lb and x_ub)
2. Gather the logits (10D-tensor) of the two.
3. Based on the logits, you will design a y_specs (see "3.1 Our verification interface: verify(net, x_spec, y_spec)").
4. You should design your y_specs that follows:
   • the lower bound for the ground truth label is greater than the upper bound of other dimensionts.
     For example, if the ground truth is label 6, then y_specs[6][0] (lower bound of 6th dim) should be greater than y_specs[i][1] where i!=6.
   • For each dimension in y_specs, the (lower_bound, upper_bound) should cover your network's outputs.
     In other wrods, we don't want verification rejects because of the "range" of some dimension is too narrarow.
   • (You may need to play with it to create some wanted y_specs)
5. Note that this y_specs is not general; it is specific for your network and the x_lb and x_ub.

a starting point of creating y_specs

A starting point is to create the y_specs by getting the outputs of x_lb and x_ub, and then use the average of each dimensions minus/plus some epsilon.

Then, you need to "fine tune" the y_specs to make sure the ground truth label's lower bound is higher than the upper bounds of the others.

# inference the nets for x_lb and x_ub
with torch.no_grad():
    y_lower = mnist_model.net(x_lb)
    y_upper = mnist_model.net(x_ub)

# get avg output
y_avg_specs = (y_lower + y_upper) / 2.0

# a starting point of y_specs
epsilon = 0.01
y_specs = []
for i in range(len(y_avg_specs[0])):
    y_specs.append([y_avg_specs[0,i].item() - epsilon,
                    y_avg_specs[0,i].item() + epsilon])

# TODO: design your y_specs
y_specs

(c) verify!

# verify specifications (x_specs, y_specs) for your mode (mnist_model.net)
# TODO: your code here

cases = [] # for conterexamples

# check if the result makes sense

if len(cases) > 0:
    case1 = cases[0]
    plot_mnist(case1)
    info(f"prediction output: {mnist_model.net(case1).argmax(1)}")

Challenge 1: verify more complex specification

The above verification is "toy" because we only perturb one pixel.

Below is a much more challenging task by perturbing many pixels all at once.

def perturb_all_pixels(x, delta):
    assert delta > 0
    
    x_lower_bound = torch.clone(x)
    x_upper_bound = torch.clone(x)
    for i in range(len(x[0])//2):
        x_lower_bound[0, i] -= delta   # we change the value of one pixel on the pic
        x_upper_bound[0, i] += delta   # we change the value of one pixel on the pic
    
    return x_lower_bound, x_upper_bound

# creating challenging x_specs
x = nn.Flatten()(the_chosen_one)
x_lb, x_ub = perturb_all_pixels(x, 1)

plot_mnist(x_ub)

Exercise 5: verify the challenging spec (the new x_lb and x_ub)

• Use the new x_lb and x_ub to construct x_spec
• Design you new y_spec
• Check if your network is robust to the new specification

# TODO: your code here