Need help with NeuralVerification.jl?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

174 Stars 38 Forks MIT License 911 Commits 30 Opened issues


Methods to soundly verify deep neural networks

Services available


Need anything else?

Contributors list

| 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: * Reachability methods: ExactReach, MaxSens, Ai2,

Reference: C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barrett, and M. Kochenderfer, "Algorithms for Verifying Deep Neural Networks," to appear in Foundations and Trend in Optimization. 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,

, and
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 :violated

For a full list of

and their properties, requirements, and
types, please refer to the documentation.

Example Use Cases

CARS Workshop

Head to for the material used at the NeuralVerification workshop held at the Stanford Center for Automotive research. Where NeuralVerification.jl was used to verify image classification networks and air collision avoidance systems among some other examples.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.