91 lines
2.7 KiB
Markdown
91 lines
2.7 KiB
Markdown
This repository provide all the necessary material
|
|
for the practical session of SETI Master - AI section.
|
|
|
|
The main file is a jupyter notebook `code/tutorial.ipynb`, slides for the first
|
|
part of the tutorial are under `doc/slides.pdf`.
|
|
|
|
There are several dependancies to install.
|
|
|
|
# Getting started
|
|
* We suppose python3.9 is installed and pip
|
|
* First we can move into code folder
|
|
```
|
|
cd code
|
|
```
|
|
* We recommend creating a dedicated environment for the tutorial, using for instance virtualenv. If virtualenv is not installed run:
|
|
```
|
|
python3.9 -m pip install virtualenv
|
|
```
|
|
Afterwards you can create the virtualenv using:
|
|
```
|
|
virtualenv ~/.virtualenvs/tuto_seti
|
|
```
|
|
consider adding `-p /usr/bin/python3.9` pointing to your python version if you have multiple python installed.
|
|
Then activate the environment using
|
|
```
|
|
source ~/.virtualenvs/tuto_seti/bin/activate
|
|
```
|
|
|
|
* Once in this venv, we can install python dependencies needed for this tutorial with :
|
|
```
|
|
jupyter notebook tutorial.ipynb
|
|
```
|
|
|
|
# Tools installation
|
|
|
|
* **Z3**: your linux distribution should have a package (named z3):
|
|
```
|
|
sudo apt install z3
|
|
```
|
|
Otherwise check [here](https://github.com/Z3Prover/z3) for a detailed installation instruction
|
|
|
|
|
|
* **ISAIEH** can be found compiled in the `bin` folder.
|
|
|
|
* **Marabou** can be found compiled in the `bin` folder.
|
|
|
|
* **PyRAT** comes as a precompiled binary in this repository that requires Python 3.9
|
|
|
|
When everything is installed, `jupyter notebook tutorial.ipynb` should open the tutorial notebook in your web browser.
|
|
|
|
## In case compiled version does not work
|
|
|
|
* **ISAIEH**: The next is to install dependencies for ISAIEH, which we will use:
|
|
* install the ocaml opam build system with:
|
|
```
|
|
sudo apt install opam
|
|
```
|
|
* Additional system dependencies with `m4` and `gmp` are needed at minimum.
|
|
Install them using
|
|
```
|
|
sudo apt install m4 libgmp3-dev
|
|
```
|
|
on a Debian-like.
|
|
* Finally we can install ISAIEH with
|
|
```
|
|
git clone https://git.frama-c.com/pub/isaieh.git && cd isaieh && opam init --disable-sandboxing && opam install -y . && eval $(opam env) && dune build
|
|
```
|
|
|
|
* **Marabou** can be compiled from [source](https://github.com/NeuralNetworkVerification/Marabou) using:
|
|
```
|
|
sudo apt install cmake libboost-all-dev
|
|
```
|
|
```
|
|
git clone https://github.com/NeuralNetworkVerification/Marabou
|
|
cd Marabou
|
|
mkdir build
|
|
cd build
|
|
cmake ..
|
|
cmake --build .
|
|
```
|
|
If this does not work an older version binary can be downloaded with
|
|
```
|
|
wget https://aisafety.stanford.edu/marabou/marabou-1.0-x86_64-linux.zip
|
|
```
|
|
|
|
### Authors
|
|
- Augustin Lemesle
|
|
- Julien Girard-Satabin
|
|
- Guillaume Charpiat
|
|
- Zakaria Chihani
|
|
- Marc Schoenauer
|