dnnv 0.0.1

dnnv - deep neural network verification

Deep Neural Network Verification Toolbox

Tools for verification and analysis of deep neural networks.

Getting Started

Installation

Clone this network:

$ git clone https://github.com/dlshriver/DNNV.git

Create a python virtual environment for this project:

$ ./manage.sh init

To activate the virtual environment and set environment variables correctly for tools installed using the provided manage.sh script, run:

$ . .env.d/openenv.sh

Install any of the supported verifiers (Reluplex, planet, MIPVerify.jl, Neurify, ERAN):

$ ./manage.sh install reluplex planet mipverify neurify eran

Usage

Properties are specified in our property DSL, extended from Python. A property specification can import python modules, and define variables. The only required component is the property expression, which must appear at the end of the file. An example of a local robustness property is shown below.

from dnnv.properties import *

N = Network("N")
x = Image("path/to/image")
epsilon = Parameter("epsilon", float, default=1.0)

Forall(
    x_,
    Implies(
        ((x - epsilon) < x_ < (x + epsilon)),
        argmax(N(x_)) == argmax(N(x))),
    ),
)

To check whether property holds for some network using the ERAN verifier, run:

$ python -m dnnv network.onnx property.prop --eran

Additionally, if the property defines parameters, using the Parameter keyword, they can be specified on the command line using the option --prop.PARAMETER_NAME, where PARAMETER_NAME is the name of the parameter. For the property defined above, a value for epsilon can be provided with a command line option as follows:

$ python -m dnnv network.onnx property.prop --eran --prop.epsilon=2.0

Contributing