README.md 2.7 KB
Newer Older
1 2
This repository provide all the necessary material
for PFIA 2020 tutorial
Julien Girard's avatar
Julien Girard committed
3 4
"Formal verification of deep neural networks".

5 6
The main file is a jupyter notebook `tutorial.ipynb`,
slides for the first
Julien Girard's avatar
Julien Girard committed
7 8
part of the tutorial are under `doc/slides.pdf`.

9 10
There are several dependancies to install.
For convenience, a Docker image
Julien Girard's avatar
Julien Girard committed
11 12
is provided.

GIRARD-SATABIN Julien's avatar
GIRARD-SATABIN Julien committed
13
### Install the tutorial environment within a Docker image (recommended)
Julien Girard's avatar
Julien Girard committed
14

15 16 17 18 19 20 21
The Dockerfile contains all dependencies for running the
tutorial. If you want to regenerate the training data and
retrain the network by yourself, you will need to install
the `torch` python package.

During build, about 300MB of data will be downloaded.

Julien Girard's avatar
Julien Girard committed
22 23
#### Build Docker image
1. Install Docker
GIRARD-SATABIN Julien's avatar
GIRARD-SATABIN Julien committed
24 25 26 27 28 29 30 31
    1. on Windows or macOS, install Docker Desktop
    1. on Linux systems, install the Docker toolbox:
        * on Debian/Ubuntu, `sudo apt-get update && sudo apt-get install docker`
        * on Archlinux, `sudo pacman -Syu docker`
        * Don't forget to add your user to the `docker` group if you want
        to run the container as non-root:
        `sudo groupadd docker && sudo usermod -aG docker $USER`
        (you will need to log off for this change to exist)
Julien Girard's avatar
Julien Girard committed
32 33 34 35 36 37 38 39 40 41 42 43 44 45
1. Change directory at the root of this repository
1. Build the docker image: `docker build -t pfia .`. Be advised,
   building the image may take several minutes depending on your internet
   speed and your machine.

#### Run the tutorial environment
Type `docker run -tp 8888:8888 pfia` to launch the image.
Then click on one of the URL on your terminal, it
will open a window in your web browser. Double-click on "tutorial.ipynb" and
you are good to go :)

### Install dependencies manually

* python dependencies:
GIRARD-SATABIN Julien's avatar
GIRARD-SATABIN Julien committed
46
  `pip install -r requirements.txt && pip install jupyter`
Julien Girard's avatar
Julien Girard committed
47 48 49
* ISAIEH:
  * install the ocaml opam build system
  [available here](https://opam.ocaml.org/doc/Install.html)
GIRARD-SATABIN Julien's avatar
GIRARD-SATABIN Julien committed
50
  * system dependencies are `m4`, `gmp`, `g++`, `gcc`, `cmake`, `make`
Julien Girard's avatar
Julien Girard committed
51 52
  * install command `git clone https://git.frama-c.com/pub/isaieh.git && cd isaieh && opam init --disable-sandboxing && opam install -y . && eval $(opam env) && dune build`.
* Z3: your linux distribution should have a package (named z3), check
GIRARD-SATABIN Julien's avatar
GIRARD-SATABIN Julien committed
53
  [here](https://github.com/Z3Prover/z3) for detailed installation instructions
Julien Girard's avatar
Julien Girard committed
54 55 56 57 58 59 60 61 62
* Marabou: either get the static binary with
  `wget https://aisafety.stanford.edu/marabou/marabou-1.0-x86_64-linux.zip`,
  or compile from [source](https://github.com/NeuralNetworkVerification/Marabou)
* PyRAT comes as a precompiled binary that requires Python 3.7.6

When everything is installed, `jupyter notebook tutorial.ipynb` should
open the tutorial notebook in your web browser.

### Authors
GIRARD-SATABIN Julien's avatar
GIRARD-SATABIN Julien committed
63 64 65 66 67
* Julien Girard-Satabin
* Guillaume Charpiat
* Zakaria Chihani
* Augustin Lemesle
* Marc Schoenauer