Skip to content

Commit

Permalink
Repository refactoring and ghub workflow (#3)
Browse files Browse the repository at this point in the history
* Repo refactor, update of readme and tuto

- source code in airobas/ folder
- update of dependencies in pyproject.toml
- basic github workflow to install lib and dependencies and run pipeline tests
- update of read me content
  • Loading branch information
g-poveda authored Aug 1, 2024
1 parent 8da8625 commit 420d573
Show file tree
Hide file tree
Showing 42 changed files with 371 additions and 228 deletions.
29 changes: 29 additions & 0 deletions .github/workflows/python-package.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
name: Python package

on: [push, pull_request]

jobs:
build:

runs-on: ubuntu-latest
strategy:
matrix:
python-version: ["3.9", "3.10"]

steps:
- uses: actions/checkout@v3
- name: Set up Python ${{ matrix.python-version }}
uses: actions/setup-python@v5
with:
python-version: ${{ matrix.python-version }}
cache: "pip"
cache-dependency-path: pyproject.toml
- name: Install dependencies
run: |
python -m pip install --upgrade pip
pip install .
pip install onnxruntime
pip install pytest
- name: Test with pytest
run: |
pytest tests/
19 changes: 19 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
# Mac
.DS_Store

# IDE
.*/

# Python
__pycache__/
.python-version

# Temp files
*.tmp

# Build files
build/
dist/
# don't update locally created images and dump file
tutorials/dump.txt
tutorials/rosenbrock_images/*.png
59 changes: 25 additions & 34 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@

## Introduction

**What is Airobas?** `A(i)robas` is a library that combines verification tool for neural network into a pipeline.
**What is Airobas?** `A(i)robas` is a library that allows the combinaison of verification tools for neural network into a pipeline.

It provides functionalities to:

– load input data and models,
Expand All @@ -11,39 +12,33 @@ It provides functionalities to:
to be as generic as possible and highly parametrizable regarding property
definition,

– design customized verification pipeline,
– design a customized verification pipeline,

– run verification with a default set of empirical and formal methods e.g., at-
tacks using the [cleverhans](https://github.com/cleverhans-lab/cleverhans) library, incomplete verification using LiRPA-based
functionalities implemented in [decomon](https://github.com/airbus/decomon) etc.,
– run verification with a default set of empirical and formal methods e.g., adversarial attacks using the [cleverhans](https://github.com/cleverhans-lab/cleverhans) library, incomplete verification using LiRPA-based
functionalities implemented in the Airbus open-source library [decomon](https://github.com/airbus/decomon) etc.,

– append new verification functions or link the code to open-source libraries
of one’s choice
– append new verification functions or link the code to the open-source libraries of one’s choice

We believe that Airobas is a complementary tool to existing libraries for the certification of neural networks.
This open source code is a support to our publication ["Surrogate Neural Networks Local Stability for
Aircraft Predictive Maintenance"](https://arxiv.org/abs/2401.06821)
We believe that Airobas is a complementary tool to existing libraries for the robustness verification of neural networks.
This open source code is a complement to the publication ["Surrogate Neural Networks Local Stability for
Aircraft Predictive Maintenance"](https://arxiv.org/abs/2401.06821) which was peer-reviewed and accepted at the 29th International Conference on Formal Methods for Industrial Critical Systems ([FMICS2024](https://fmics.inria.fr/2024/)).

**Complete Verification Pipeline for Stability**

The state-of-the-art property verification of neural networks is currently divided into three
families of methods. They all take as input test points and a trained model and return
for every test point if the property is violated or verified.
- Firstly, there are the ’no/maybe’ methods (block A), such as [adversarial attacks](https://github.com/cleverhans-lab/cleverhans). Essentially, these methods rely on the search for counterexamples that would
contradict the stability property. If no counterexample is found, no conclusion can
be drawn.
- Secondly, there are the ’yes/maybe’ (block B) methods, such as the affine bounds
implemented in the [Decomon library](https://github.com/airbus/decomon). Here, the outputs of a network are
bounded. If the bounds found are within the stability bounds, then the property
is verified. If the bounds are too loose and exceed the required stability interval,
no conclusion can be drawn. So far, these methods called incomplete methods are
partial in the sense that they do not provide an absolute solution to the question of
a network’s stability but are generally fast.
- The last family of methods corresponds to the ’yes/no’ complete methods (block C). Examples include [SMT](https://github.com/NeuralNetworkVerification/Marabou) or [MILP](https://gurobi-machinelearning.readthedocs.io/en/stable/index.html) solvers, which provide an exact answer
at the cost of significant computation time.
Verification techniques for neural networks take test points, a trained model and a given property (robustness, stability, monotonicity etc.) as input and return for every test point an assessment of whether or not the property is violated or verified.

The current state-of-the-art mainly encaompasses three families of methods:

- The ’no/maybe’ methods (Family of techniques 'A' in paper): e.g. [adversarial attacks](https://github.com/cleverhans-lab/cleverhans). These methods essentially rely on the search for counterexamples that contradict the targeted property. If no counterexample is found, no conclusion can be drawn on the model output w.r.t to the targeted property.

- The ’yes/maybe’ methods (Family of techniques 'B' in paper): e.g. the affine bounds generation methods implemented in the [decomon library](https://github.com/airbus/decomon). These techniques intend to bound the output values of a network. If the derived bounds respect the property, it is verified. If the bounds exceed it, no conclusion can be drawn. It can then either mean that the propety is violated or that the derived bounds are too loose. These methods are commonly refered to as 'incomplete' (since they can guarantee the property is respected but not that it is violated). They are however generally faster than 'complete' methods (see next).

- The ’yes/no’ methods (Family of techniques 'C' in paper): e.g., [SMT](https://github.com/NeuralNetworkVerification/Marabou), [MILP](https://gurobi-machinelearning.readthedocs.io/en/stable/index.html) solvers etc. They can guarantee that the neural network output resepct or not the targeted property, at the cost of significant computation time. They are commonly refered to as 'complete' techniques.

Here is an example of NN verification pipeline:

<div align="center">
<img src="https://github.com/airbus/Airobas/blob/main/docs/pipeline_plusnumbers_plusletters.png" width="75%" alt="pipeline" align="center" />
<img src="https://github.com/airbus/Airobas/blob/main/docs/pipeline.png" width="75%" alt="pipeline" align="center" />
</div>


Expand All @@ -53,15 +48,11 @@ Quick version:
```shell
pip install .
```
For more details, see the [online documentation](https://airbus.github.io/airobas/main/install).

## Examples

Notebooks providing examples of the use of the library are available in the "tutorials" folder:

- Use case "Aircraft braking distance estimation" [![Open In Colab](https://colab.research.google.com/assets/colab-badge.svg)](https://colab.research.google.com/github/airbus/Airobas/blob/main/tutorials/braking_distance_estimation_verification.ipynb)

## Documentation

The latest documentation is available [online](https://airbus.github.io/airobas).

## Examples

Some educational notebooks will be available *soon*.
- Use case "NN surrogate for Rosenbrock function" [![Open In Colab](https://colab.research.google.com/assets/colab-badge.svg)](https://colab.research.google.com/github/airbus/Airobas/blob/main/tutorials/rosenbrock_verification.ipynb)
File renamed without changes.
File renamed without changes.
4 changes: 2 additions & 2 deletions blocks_hub/adv_block.py → airobas/blocks_hub/adv_block.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
from cleverhans.tf2.attacks.fast_gradient_method import fast_gradient_method
from cleverhans.tf2.attacks.projected_gradient_descent import projected_gradient_descent

from blocks_hub.meta_block import MetaBlock
from verif_pipeline import (
from airobas.blocks_hub.meta_block import MetaBlock
from airobas.verif_pipeline import (
BlockVerif,
BlockVerifOutput,
DataContainer,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
import numpy as np
from decomon.models import clone

from verif_pipeline import BlockVerif, BlockVerifOutput, StatusVerif
from airobas.verif_pipeline import BlockVerif, BlockVerifOutput, StatusVerif


def check_SB_unsat(y_pred_min, y_pred_max, y_min, y_max):
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,31 +6,27 @@
import numpy as np
from gurobi_ml import add_predictor_constr

from blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_utils import (
create_object_bounds,
)
from blocks_hub.mip_blocks_lib.commons.formula import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_utils import create_object_bounds
from airobas.blocks_hub.mip_blocks_lib.commons.formula import (
GT,
LT,
NAryConjFormula,
StateCoordinate,
VarConstConstraint,
)
from blocks_hub.mip_blocks_lib.commons.neural_network import (
from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import (
InputBoundsNeuralNetwork,
NeuralNetwork,
)
from blocks_hub.mip_blocks_lib.commons.parameters import (
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import (
ParamsBoundComputation,
ParamsBoundComputationEnum,
)
from blocks_hub.mip_blocks_lib.commons.utilities.evaluate import evaluate, random_input
from blocks_hub.mip_blocks_lib.linear.verification_formula.verification_constraints import (
get_callback_specific,
from airobas.blocks_hub.mip_blocks_lib.commons.utilities.evaluate import evaluate, random_input
from airobas.blocks_hub.mip_blocks_lib.linear.verification_formula.verification_constraints import (
get_output_constrs,
get_output_constrs_specific,
)
from verif_pipeline import (
from airobas.verif_pipeline import (
BlockVerif,
BlockVerifOutput,
DataContainer,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@
import numpy as np
from maraboupy import Marabou, MarabouCore
from maraboupy.MarabouNetwork import MarabouNetwork # (pip install maraboupy)
from tensorflow.keras.layers import Activation, Dense, Input
from tensorflow.keras.layers import Activation, Dense
from tensorflow.keras.models import Sequential

from verif_pipeline import (
from airobas.verif_pipeline import (
BlockVerif,
BlockVerifOutput,
DataContainer,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

import numpy as np

from verif_pipeline import (
from airobas.verif_pipeline import (
BlockVerif,
BlockVerifOutput,
DataContainer,
Expand Down
File renamed without changes.
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,15 @@

from tensorflow.python.keras.models import Model # , Sequential, load_model

from blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_interface import (
BoundComputation,
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_interface import (
BoundComputation
)
from blocks_hub.mip_blocks_lib.commons.bounds_propagation.linear_propagation import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.linear_propagation import (
Bounds,
compute_bounds_linear_propagation,
)
from blocks_hub.mip_blocks_lib.commons.layers import Linear, Relu
from blocks_hub.mip_blocks_lib.commons.neural_network import (
from airobas.blocks_hub.mip_blocks_lib.commons.layers import Linear, Relu
from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import (
NeuralNetwork,
neural_network_to_keras,
)
Expand Down
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
from abc import abstractmethod

from blocks_hub.mip_blocks_lib.commons.bounds_propagation.linear_propagation import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.linear_propagation import (
compute_bounds_linear_propagation,
)
from blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds

from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds

def default_propagation(neural_network: NeuralNetwork):
compute_bounds_linear_propagation(
Expand Down
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
from blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_interface import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_interface import (
BoundComputation,
)
from blocks_hub.mip_blocks_lib.commons.bounds_propagation.linear_propagation import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.linear_propagation import (
compute_bounds_linear_propagation,
)
from blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds
from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds


def default_propagation(neural_network: NeuralNetwork):
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,13 @@
from decomon.models.utils import ConvertMethod
except ImportError as e:
print(e)
from blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_decomon import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_decomon import (
BoundsComputationDecomon,
)
from blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_interface import (
BoundComputation,
)
from blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_symbolic_arithmetic import (
from airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_computation_symbolic_arithmetic import (
BoundComputationSymbolicArithmetic,
default_propagation,
)
from blocks_hub.mip_blocks_lib.commons.parameters import (
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import (
ParamsBoundComputation,
ParamsBoundComputationEnum,
)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@

import numpy as np

from blocks_hub.mip_blocks_lib.commons.layers import Layer
from blocks_hub.mip_blocks_lib.commons.linearfunctions import LinearFunctions
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds
from airobas.blocks_hub.mip_blocks_lib.commons.layers import Layer
from airobas.blocks_hub.mip_blocks_lib.commons.linearfunctions import LinearFunctions
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds


def compute_bounds(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@

import numpy as np

from blocks_hub.mip_blocks_lib.commons.layers import Layer
from blocks_hub.mip_blocks_lib.commons.linearfunctions import LinearFunctions
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds
from airobas.blocks_hub.mip_blocks_lib.commons.layers import Layer
from airobas.blocks_hub.mip_blocks_lib.commons.linearfunctions import LinearFunctions
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds


def compute_bounds(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,16 @@
import numpy as np
from numba import njit

from blocks_hub.mip_blocks_lib.commons.layers import Layer, Relu
from blocks_hub.mip_blocks_lib.commons.linearfunctions import (
from airobas.blocks_hub.mip_blocks_lib.commons.layers import Layer, Relu
from airobas.blocks_hub.mip_blocks_lib.commons.linearfunctions import (
LinearFunctions,
compute_max_values_numba,
compute_min_values_numba,
compute_upper_numba,
get_lower_relu_relax_numba,
get_upper_relu_relax_numba,
)
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds


def compute_bounds_numba(
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
import blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_function_linear as bounds_linear
import blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_function_relu as bounds_relu
from blocks_hub.mip_blocks_lib.commons.layers import InputLayer, Relu
from blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds
import airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_function_linear as bounds_linear
import airobas.blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_function_relu as bounds_relu
from airobas.blocks_hub.mip_blocks_lib.commons.layers import InputLayer, Relu
from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds


def compute_bounds_linear_propagation(
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import blocks_hub.mip_blocks_lib.commons.bounds_propagation.bounds_function_relu_numba as bounds_relu
from blocks_hub.mip_blocks_lib.commons.layers import InputLayer, Relu
from blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from blocks_hub.mip_blocks_lib.commons.parameters import Bounds
from airobas import blocks_hub as bounds_relu
from airobas.blocks_hub.mip_blocks_lib.commons.layers import InputLayer, Relu
from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import NeuralNetwork
from airobas.blocks_hub.mip_blocks_lib.commons.parameters import Bounds


def compute_bounds_linear_propagation(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@

import numpy as np

from blocks_hub.mip_blocks_lib.commons.linearfunctions import LinearFunctions
from airobas.blocks_hub.mip_blocks_lib.commons.linearfunctions import LinearFunctions


class LayerType(Enum):
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
from keras.layers import Activation, Dense
from keras.models import Sequential

from blocks_hub.mip_blocks_lib.commons.layers import (
from airobas.blocks_hub.mip_blocks_lib.commons.layers import (
InputLayer,
InputType,
Layer,
Expand Down
Empty file.
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import numpy as np

from blocks_hub.mip_blocks_lib.commons.neural_network import Linear, NeuralNetwork, Relu
from airobas.blocks_hub.mip_blocks_lib.commons.neural_network import Linear, NeuralNetwork, Relu


def random_input(neural_net: NeuralNetwork):
Expand Down
Empty file.
Empty file.
Loading

0 comments on commit 420d573

Please sign in to comment.