Skip to content
Methods to soundly verify deep neural networks
Julia Jupyter Notebook
Branch: master
Clone or download
Latest commit 606a5d6 Nov 5, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
docs typo in docs Mar 6, 2019
examples notebook cleanup and minimal requirements Oct 28, 2019
src Merge pull request #78 from sisl/windows Nov 5, 2019
test tests Mar 11, 2019
.gitignore update ignore, docs/make, travis Jan 7, 2019
.travis.yml update for windows Nov 4, 2019
LICENSE Create LICENSE Dec 16, 2018
Manifest.toml downgrade lazysets again Nov 4, 2019
Project.toml .toml files Mar 11, 2019 Update May 6, 2019

Testing Coverage Documentation
Build Status Coverage Status


This library contains implementations of various methods to soundly verify deep neural networks. In general, we verify whether a neural network satisfies certain input-output constraints. The verification methods are divided into five categories:

Reference: C. Liu, T. Arnon, C. Lazarus, C. Barrett, and M. Kochenderfer, "Algorithms for Verifying Neural Networks," arXiv:1903.06758.


To download this library, clone it from the julia package manager like so:

(v1.0) pkg> add

Please note that the implementations of the algorithms are pedagogical in nature, and so may not perform optimally. Derivation and discussion of these algorithms is presented in the survey paper linked above.

Note: At present, Ai2, ExactReach, and Duality do not work in higher dimensions (e.g. image classification). This is being addressed in #9

The implementations run in Julia 1.0.

Example Usage

Choose a solver

using NeuralVerification

solver = BaB()

Set up the problem

nnet = read_nnet("examples/networks/small_nnet.nnet")
input_set  = Hyperrectangle(low = [-1.0], high = [1.0])
output_set = Hyperrectangle(low = [-1.0], high = [70.0])
problem = Problem(nnet, input_set, output_set)


julia> result = solve(solver, problem)
CounterExampleResult(:violated, [1.0])

julia> result.status

For a full list of Solvers and their properties, requirements, and Result types, please refer to the documentation.

You can’t perform that action at this time.