dnnv - deep neural network verification
Deep Neural Network Verification Toolbox
Tools for verification and analysis of deep neural networks. Watch our demo video for a quick description!
For more detailed instructions, see our documentation.
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
$ ./manage.sh install reluplex planet mipverify neurify eran
Make sure that the project environment is activated when installing verifiers with the
manage.sh script. Otherwise some tools may not install correctly.
Additionally, several verifiers make use of the Gurobi solver. This should be installed automatically, but requires a license to be manually activated and available on the host machine. Academic licenses can be obtained for free from the Gurobi website.
Finally, planet has several additional requirements that currently must be installed separately before installation with
./manage.sh: libglpk-dev, qt5-qmake, valgrind, libltdl-dev, protobuf-compiler.
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
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
A set of example networks and properties that can be run with DNNV are available here.
This material is based in part upon work supported by the National Science Foundation under grant number 1900676.
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
|Filename, size||File type||Python version||Upload date||Hashes|
|Filename, size dnnv-0.3.0-py3-none-any.whl (75.4 kB)||File type Wheel||Python version py3||Upload date||Hashes View|
|Filename, size dnnv-0.3.0.tar.gz (9.1 MB)||File type Source||Python version None||Upload date||Hashes View|