HullGMP

HullGMP.jl

This library contains sourse codes used in the paper "Hull is all you need", including implementations of four methods to soundly verify deep neural networks: MaxSens, HullReach, SpeGuid, and HullSearch. This library is based on https://github.com/sisl/NeuralVerification.jl.

Installation

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

(v1.5) pkg> add https://github.com/Student2Pro/HullGMP.jl

Please note that the implementations of the algorithms may not perform optimally.

Example Usage

Choose a solver

using HullGMP

solver = HullReach(0.1, true)

Set up the problem

nnet = read_nnet("nnet/dnn1.nnet")
input_set  = Hyperrectangle(fill(0.5,2), fill(0.5,2))
output_set = Hyperrectangle(fill(0.0,2), fill(0.15,2))
problem = Problem(nnet, input_set, output_set)

Solve

julia> result = solve(solver, problem)
BasicResult(:violated)

julia> result.status
:violated

The nnet directory contains the DNNs we used in the experiment. The plot_src directory contains the MatLab source files of Figure 1 and Figure 2 in the paper. The src directory contains the source files of our methods as well as the baseline methods. The test directory contains the experimental setup in the paper.