Initial commit: added skeleton

README.md

@@ -0,0 +1,53 @@
+# ReliableAI 2022 Course Project
+
+This is the project for Reliable and Trustworthy Artificial Intelligence course at ETH Zurich.
+
+## Folder structure
+In the directory `code` you can find several files. 
+File `networks.py` and `resnet.py` contain encodings of fully connected, convolutional and residual neural network architectures as PyTorch classes.
+The architectures extend `nn.Module` object and consist of standard PyTorch layers (e.g. `Linear`, `Flatten`, `ReLU`, `Conv2d`). Please note that first layer of each network performs normalization of the input image. 
+File `verifier.py` contains a template of verifier. Loading of the stored networks and test cases is already implemented in `main` function. If you decide to modify `main` function, please ensure that parsing of the test cases works correctly. Your task is to modify `analyze` function by building upon DeepPoly convex relaxation. Note that provided verifier template is guaranteed to achieve **0** points (by always outputting `not verified`).
+
+In folder `nets` you can find 10 neural networks (3 fully connected, 4 convolutional, and 3 residual). These networks are loaded using PyTorch in `verifier.py`.
+You can find architectures of these networks in `networks.py`.
+Note that for ResNet we prepend Normalization layer after loading the network (see `get_net` function in `verifier.py`).
+Name of each network contains the dataset the network is trained used on, e.g. `net3_cifar10_fc3.pt` is network which receives CIFAR-10 images as inputs.
+In folder `examples` you can find 10 subfolders. Each subfolder is associated with one of the 10 networks. In a subfolder corresponding to a network, you can find 2 example test cases for this network. 
+As explained in the lecture, these test cases **are not** part of the set of test cases which we will use for the final evaluation, and they are only here for you to develop your verifier. 
+
+## Setup instructions
+
+We recommend you to install Python virtual environment to ensure dependencies are same as the ones we will use for evaluation.
+To evaluate your solution, we are going to use Python 3.7.
+You can create virtual environment and install the dependencies using the following commands:
+
+```bash
+$ virtualenv venv --python=python3.7
+$ source venv/bin/activate
+$ pip install -r requirements.txt
+```
+
+## Running the verifier
+
+We will run your verifier from `code` directory using the command:
+
+```bash
+$ python verifier.py --net {net} --spec ../examples/{net}/img{test_idx}_{eps}.txt
+```
+
+In this command, `{net}` is equal to one of the following values (each representing one of the networks we want to verify): `net1, net2, net3, net4, net5, net6, net7, net8, net9, net10`.
+`test_idx` is an integer representing index of the test case, while `eps` is perturbation that verifier should certify in this test case.
+
+To test your verifier, you can run for example:
+
+```bash
+$ python verifier.py --net net1 --spec ../examples/net1/img1_0.0500.txt
+```
+
+To evaluate the verifier on all networks and sample test cases, we provide the evaluation script.
+You can run this script using the following commands:
+
+```bash
+chmod +x evaluate
+./evaluate ../examples
+```

code/evaluate

@@ -0,0 +1,13 @@
+#!/bin/bash
+
+rm $1/res.txt
+for net in {1..10}
+do
+	echo Evaluating network net${net}...
+	for spec in `ls $1/net${net}/`
+	do
+		echo ${spec}
+		res=$(python verifier.py --net net${net} --spec $1/net${net}/${spec})
+		echo net${k}_${net},$spec,$res >> $1/res.txt
+	done
+done

code/networks.py

@@ -0,0 +1,129 @@
+import torch
+import torch.nn as nn
+from resnet import ResNet, BasicBlock
+
+class Normalization(nn.Module):
+
+    def __init__(self, device, dataset):
+        super(Normalization, self).__init__()
+        if dataset == 'mnist':
+            self.mean = torch.FloatTensor([0.1307]).view((1, 1, 1, 1)).to(device)
+            self.sigma = torch.FloatTensor([0.3081]).view((1, 1, 1, 1)).to(device)
+        elif dataset == 'cifar10':
+            self.mean = torch.FloatTensor([0.4914, 0.4822, 0.4465]).view((1, 3, 1, 1)).to(device)
+            self.sigma = torch.FloatTensor([0.2023, 0.1994, 0.201]).view((1, 3, 1, 1)).to(device)
+        else:
+            assert False
+
+    def forward(self, x):
+        return (x - self.mean) / self.sigma
+
+
+class FullyConnected(nn.Module):
+
+    def __init__(self, device, dataset, input_size, input_channels, fc_layers, act='relu'):
+        super(FullyConnected, self).__init__()
+
+        layers = [Normalization(device, dataset), nn.Flatten()]
+        prev_fc_size = input_size * input_size * input_channels
+        for i, fc_size in enumerate(fc_layers):
+            layers += [nn.Linear(prev_fc_size, fc_size)]
+            if i + 1 < len(fc_layers):
+                if act == 'relu':
+                    layers += [nn.ReLU()]
+                else:
+                    assert False
+            prev_fc_size = fc_size
+        self.layers = nn.Sequential(*layers)
+
+    def forward(self, x):
+        return self.layers(x)
+
+
+class Conv(nn.Module):
+
+    def __init__(self, device, dataset, input_size, input_channels, conv_layers, fc_layers, n_class=10):
+        super(Conv, self).__init__()
+
+        self.input_size = input_size
+        self.n_class = n_class
+
+        layers = [Normalization(device, dataset)]
+        prev_channels = input_channels
+        img_dim = input_size
+
+        for n_channels, kernel_size, stride, padding in conv_layers:
+            layers += [
+                nn.Conv2d(prev_channels, n_channels, kernel_size, stride=stride, padding=padding),
+                nn.ReLU(),
+            ]
+            prev_channels = n_channels
+            img_dim = img_dim // stride
+        layers += [nn.Flatten()]
+
+        prev_fc_size = prev_channels * img_dim * img_dim
+        for i, fc_size in enumerate(fc_layers):
+            layers += [nn.Linear(prev_fc_size, fc_size)]
+            if i + 1 < len(fc_layers):
+                layers += [nn.ReLU()]
+            prev_fc_size = fc_size
+        self.layers = nn.Sequential(*layers)
+
+    def forward(self, x):
+        return self.layers(x)
+
+
+class NormalizedResnet(nn.Module):
+
+    def __init__(self, device, resnet):
+        super(NormalizedResnet, self).__init__()
+
+        self.normalization = Normalization(device, 'cifar10')
+        self.resnet = resnet
+
+    def forward(self, x):
+        x = self.normalization(x)
+        x = self.resnet(x)
+        return x
+
+
+def get_net_name(net):
+    net_names = {
+        'net1': 'net1_mnist_fc1.pt',
+        'net2': 'net2_mnist_fc2.pt',
+        'net3': 'net3_cifar10_fc3.pt',
+        'net4': 'net4_mnist_conv1.pt',
+        'net5': 'net5_mnist_conv2.pt',
+        'net6': 'net6_cifar10_conv2.pt',
+        'net7': 'net7_mnist_conv3.pt',
+        'net8': 'net8_cifar10_resnet_2b.pt',
+        'net9': 'net9_cifar10_resnet_2b2_bn.pt',
+        'net10': 'net10_cifar10_resnet_4b.pt',
+    }
+    return net_names[net]
+
+def get_network(device, net):
+    if net == 'net1':
+        return FullyConnected(device, 'mnist', 28, 1, [50, 10])
+    elif net == 'net2':
+        return FullyConnected(device, 'mnist', 28, 1, [100, 50, 10])
+    elif net == 'net3':
+        return FullyConnected(device, 'cifar10', 32, 3, [100, 100, 10])
+    elif net == 'net4':
+        return Conv(device, 'mnist', 28, 1, [(16, 3, 2, 1)], [100, 10], 10)
+    elif net == 'net5':
+        return Conv(device, 'mnist', 28, 1, [(16, 4, 2, 1), (32, 4, 2, 1)], [100, 10], 10)
+    elif net == 'net6':
+        return Conv(device, 'cifar10', 32, 3, [(16, 4, 2, 1), (32, 4, 2, 1)], [100, 10], 10)
+    elif net == 'net7':
+        return Conv(device, 'mnist', 28, 1, [(16, 4, 2, 1), (64, 4, 2, 1)], [100, 100, 10], 10)
+    elif net == 'net8':
+        return ResNet(BasicBlock, num_stages=1, num_blocks=2, in_planes=8, bn=False, last_layer="dense")
+    elif net == 'net9':
+        return ResNet(
+            BasicBlock, num_stages=2, num_blocks=1, in_planes=16,
+            bn=True, last_layer="dense", stride=[2, 2, 2])
+    elif net == 'net10':
+        return ResNet(BasicBlock, num_stages=2, num_blocks=2, in_planes=8, bn=False, last_layer="dense")
+    assert False
+