1. escritoire
  2. reachability

This notebook is an experiment with the NeuralVerification package (that we shorten to NV here) and decomposition methods available in LazySets.

In [2]:
using Revise, NeuralVerification, LazySets # requires schillic/1176_supportfunction
using LazySets.Approximations

const NV = NeuralVerification

networks_folder = "/Users/forets/.julia/dev/NeuralVerification/examples/networks/"
Out[2]:
"/Users/forets/.julia/dev/NeuralVerification/examples/networks/"

In NV, neural networks are represented as a vector of layers, where a Layer consists of the weights matrix, the bias (an affine translation) and the activation function.

struct Layer{F<:ActivationFunction, N<:Number}
    weights::Matrix{N}
    bias::Vector{N}
    activation::F
end

struct Network
    layers::Vector{Layer} # layers includes output layer
end

Now we will work with one "small" examples in NeuralVerification/examples/networks/.

In [13]:
model = "cartpole_nnet.nnet" # 4 layers, first one 16x4 and the other ones 16 x 16
#model = "ACASXU_run2a_4_5_batch_2000.nnet" # 7 layers, 50x5 
#model = "mnist1.nnet" # 25 x 784 and 10 x 25
#model = "mnist_large.nnet" # 25 x 784 and 10 x 25
#model = "mnist2.nnet" # 100 x 784 and 10 x 100

nnet = read_nnet(networks_folder * model);
In [3]:
typeof(nnet)
Out[3]:
Network

The number of layers in this neural network as well as the number of nodes in each layer can be obtained as follows.

In [4]:
L = nnet.layers
length(L)
Out[4]:
4

The first two layers have two nodes each and the last layer (the output layer) has one node.

In [5]:
NV.n_nodes.(L)
Out[5]:
4-element Array{Int64,1}:
 16
 16
 16
  2
In [6]:
dump(L[1])

NeuralVerification.Layer{NeuralVerification.ReLU,Float64}
  weights: Array{Float64}((16, 4)) [-1.04327 -0.455724 0.192542 0.192542; -0.0191024 -0.969242 0.154406 0.154406; … ; -0.0467679 -0.482105 0.119671 0.119671; 0.0445579 -0.290073 -0.389191 -0.389191]
  bias: Array{Float64}((16,)) [-0.138894, 0.575987, -0.321108, 0.527086, 0.585529, 0.0175842, -0.359797, 0.612521, 0.547896, -0.44065, 0.444784, -0.333718, 0.509505, 0.541178, 0.427546, -0.0623751]
  activation: NeuralVerification.ReLU NeuralVerification.ReLU()
In [7]:
[size(Li.weights) for Li in L]
Out[7]:
4-element Array{Tuple{Int64,Int64},1}:
 (16, 4) 
 (16, 16)
 (16, 16)
 (2, 16)

We can directly see the weights matrix and the bias fields of the first layer:

In [8]:
L[1].weights
Out[8]:
16×4 Array{Float64,2}:
 -1.04327     -0.455724    0.192542     0.192542  
 -0.0191024   -0.969242    0.154406     0.154406  
 -0.418161     0.37731    -0.341209    -0.341209  
 -0.576796    -0.503059    0.62542      0.62542   
  0.00491105  -0.359143   -0.177293    -0.177293  
 -0.508361    -0.335279   -0.179524    -0.179524  
 -0.218255    -0.288024    0.00792378   0.00792378
  0.0605804   -0.0435269  -0.305204    -0.305204  
  0.685469     2.4089     -1.51407     -1.51407   
 -0.488534    -1.14581    -1.74527     -1.74527   
 -2.32975     -1.76154     0.817765     0.817765  
  0.801403    -1.36655    -1.20426     -1.20426   
  0.197374     0.459956   -0.342471    -0.342471  
 -0.189495    -0.277776   -0.40308     -0.40308   
 -0.0467679   -0.482105    0.119671     0.119671  
  0.0445579   -0.290073   -0.389191    -0.389191
In [9]:
n = size(L[1].weights)[2]
Out[9]:
4
In [10]:
L[1].bias
Out[10]:
16-element Array{Float64,1}:
 -0.13889389 
  0.5759869  
 -0.32110757 
  0.52708554 
  0.5855289  
  0.01758425 
 -0.35979664 
  0.6125208  
  0.5478964  
 -0.4406496  
  0.4447836  
 -0.3337182  
  0.5095051  
  0.54117775 
  0.42754632 
 -0.062375117

Random input set for cartpole:

In [24]:
H0 = rand(Hyperrectangle, dim=n)
Out[24]:
Hyperrectangle{Float64}([-0.93869, -1.73698, 1.26868, -1.60686], [0.780393, 1.35098, 0.555982, 0.798388])

An input set for ACAS is defined in the test/runtime3.jl file so we use it:

In [14]:
center = [0.40143256,  0.30570418, -0.49920412,  0.52838383,  0.4]
radius = [0.0015, 0.0015, 0.0015, 0.0015, 0.0015]
H0 = Hyperrectangle(center, radius)
dim(H)

UndefVarError: H not defined

Stacktrace:
 [1] top-level scope at In[14]:4

Let $X_1$ be the set obtained after we apply the first layer, $X_1 = A_1 H_0 \oplus b_1$.

In [25]:
A1 = L[1].weights
b1 = L[1].bias
X1 = A1 * H0 ⊕ b1
Out[25]:
Translation{Float64,Array{Float64,1},LinearMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2}}}(LinearMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2}}([-1.04327 -0.455724 0.192542 0.192542; -0.0191024 -0.969242 0.154406 0.154406; … ; -0.0467679 -0.482105 0.119671 0.119671; 0.0445579 -0.290073 -0.389191 -0.389191], Hyperrectangle{Float64}([-0.93869, -1.73698, 1.26868, -1.60686], [0.780393, 1.35098, 0.555982, 0.798388])), [-0.138894, 0.575987, -0.321108, 0.527086, 0.585529, 0.0175842, -0.359797, 0.612521, 0.547896, -0.44065, 0.444784, -0.333718, 0.509505, 0.541178, 0.427546, -0.0623751])
In [26]:
X1_am = AffineMap(A1, H0, b1) # as an affine map
Out[26]:
AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([-1.04327 -0.455724 0.192542 0.192542; -0.0191024 -0.969242 0.154406 0.154406; … ; -0.0467679 -0.482105 0.119671 0.119671; 0.0445579 -0.290073 -0.389191 -0.389191], Hyperrectangle{Float64}([-0.93869, -1.73698, 1.26868, -1.60686], [0.780393, 1.35098, 0.555982, 0.798388]), [-0.138894, 0.575987, -0.321108, 0.527086, 0.585529, 0.0175842, -0.359797, 0.612521, 0.547896, -0.44065, 0.444784, -0.333718, 0.509505, 0.541178, 0.427546, -0.0623751])

Dimension of $X_1$:

In [27]:
dim(X1)
Out[27]:
16

Let's consider an element from $X_1$ and apply the rectification operation:

In [28]:
an_element(X1)[1:10]
Out[28]:
10-element Array{Float64,1}:
  1.5668862667477603 
  2.2252558663740523 
 -0.46857571250598584
  1.7308201688049678 
  1.2646987334890278 
  1.137861079104094  
  0.3426900280822721 
  0.7344725338725435 
 -3.767735876188037  
  2.5983865765364436
In [29]:
v = LazySets.rectify(an_element(X1))
v[1:10]
Out[29]:
10-element Array{Float64,1}:
 1.5668862667477603
 2.2252558663740523
 0.0               
 1.7308201688049678
 1.2646987334890278
 1.137861079104094 
 0.3426900280822721
 0.7344725338725435
 0.0               
 2.5983865765364436
In [30]:
count(!iszero, v) # number of elements which are not zero
Out[30]:
13

We can apply a box approximation to the set and then apply the rectification, since it is easy to apply the rectification to a hyperrectangular set.

In [2]:
function rectify(H::AbstractHyperrectangle)
    Hyperrectangle(low=LazySets.rectify(low(H)), high=LazySets.rectify(high(H)))
end
Out[2]:
rectify (generic function with 1 method)
In [3]:
rectify_oa(X) = rectify(box_approximation(X))
Out[3]:
rectify_oa (generic function with 1 method)
In [33]:
LazySets.rectify(rand(2))
Out[33]:
2-element Array{Float64,1}:
 0.55694838727371   
 0.11141458040479368
In [34]:
X1_r = rectify_oa(X1) # concrete set
Out[34]:
Hyperrectangle{Float64}([1.62875, 2.22526, 0.414807, 1.85381, 1.2647, 1.13786, 0.45643, 0.734473, 1.03609, 3.44567, 5.41491, 2.89876, 0.440183, 1.33786, 1.26838, 0.742515], [1.62875, 1.53345, 0.414807, 1.85381, 0.729146, 1.09282, 0.45643, 0.519439, 1.03609, 3.44567, 5.30548, 2.89876, 0.440183, 1.06907, 0.849889, 0.742515])
In [35]:
dim(X1_r)
Out[35]:
16
In [36]:
L[2].weights
Out[36]:
16×16 Array{Float64,2}:
 -0.969095   -0.74201   -1.26007    …  -0.112787   -0.19606    -0.19606  
  0.391285    0.104401   0.0870455     -0.107367    0.0719031   0.0719031
  0.486037   -1.20122   -0.0789432      0.105409    0.15682     0.15682  
  0.285405    0.714511   0.616202       0.281021   -0.48508    -0.48508  
  0.403812   -0.113225   0.0332528      0.284097   -0.616485   -0.616485 
 -0.237504   -0.727784  -0.312868   …  -2.076       0.112664    0.112664 
  0.537505   -0.954175  -0.271187       0.103498   -0.317254   -0.317254 
  1.09746     0.491936   0.648663       0.449617   -0.894633   -0.894633 
  0.680387    0.384532   0.618043       0.0395887  -0.29143    -0.29143  
  0.0707292  -1.31967   -0.540485      -0.0290527  -0.369389   -0.369389 
  0.415719    0.419337   0.110925   …   0.094451   -0.170903   -0.170903 
 -0.830163   -2.33168   -2.10379       -1.38456     0.428579    0.428579 
  0.330955    0.431738   0.608234       0.232867   -0.506954   -0.506954 
  0.482378    0.207244   0.289128       0.121406   -0.295695   -0.295695 
 -0.341974   -0.853769  -0.362243      -0.830389    0.101125    0.101125 
 -0.961889   -1.17588   -0.598615   …  -1.20583    -0.29188    -0.29188
In [37]:
# next layer
A2 = L[2].weights
b2 = L[2].bias
X2(Y) = A2 * (Y) ⊕ b2
Out[37]:
X2 (generic function with 1 method)

Running example in 2D

In [4]:
using Plots, LazySets, LazySets.Approximations
using LazySets: translate
In [164]:
# generate some data

NUMLAYERS = 5
weight_matrices = [rand(2, 2) for i in 1:NUMLAYERS]
bias_vectors = [rand(2) for i in 1:NUMLAYERS];
In [165]:
# initial set
H0 = Hyperrectangle{Float64}([0.841145, -4.496269], [0.911519, 0.962476])
Out[165]:
Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476])
In [166]:
vertices_list(H0)
Out[166]:
4-element Array{Array{Float64,1},1}:
 [1.75266, -3.53379]  
 [-0.070374, -3.53379]
 [1.75266, -5.45874]  
 [-0.070374, -5.45874]
In [167]:
# showing the set after the first application of affine map
plot(H0, color=:blue)
W, b = weight_matrices[1], bias_vectors[1]
plot!(translate(linear_map(W, H0), b), color=:red)
Out[167]:
0.0 0.5 1.0 1.5 -5 -4 -3 -2 -1 0

Computation with a box overapproximation of the RELU set

In [3]:
function nnet_box(H0, weight_matrices, bias_vectors)
    relued_subsets = Vector{Hyperrectangle{Float64}}()
    result = H0
    NUMLAYERS = length(bias_vectors)
    
    @inbounds for i in 1:NUMLAYERS
        W, b = weight_matrices[i], bias_vectors[i]

        # lazy affine map
        Z = AffineMap(W, result, b)  

        # overapproximate with a box and rectify
        result = rectify_oa(Z)
        push!(relued_subsets, result)
    end
    return relued_subsets
end
Out[3]:
nnet_box (generic function with 1 method)
In [169]:
relued_subsets = nnet_box(H0, weight_matrices, bias_vectors)
Out[169]:
5-element Array{Hyperrectangle{Float64},1}:
 Hyperrectangle{Float64}([1.06069, 0.231937], [0.511066, 0.231937])
 Hyperrectangle{Float64}([1.02693, 1.6348], [0.530903, 0.548743])  
 Hyperrectangle{Float64}([1.94862, 2.68314], [0.627423, 0.655323]) 
 Hyperrectangle{Float64}([3.26642, 2.83915], [0.660316, 0.671064]) 
 Hyperrectangle{Float64}([3.27148, 4.87029], [0.647365, 0.880383])
In [170]:
plot(relued_subsets)
plot!(first(relued_subsets), color=:red)
plot!(last(relued_subsets), color=:grey)
Out[170]:
1 2 3 4 0 1 2 3 4 5
In [171]:
plot!(translate(linear_map(first(weight_matrices), H0), first(bias_vectors)), color=:red)
plot!(H0)
Out[171]:
0 1 2 3 4 -5.0 -2.5 0.0 2.5 5.0
In [172]:
u = translate(linear_map(first(weight_matrices), H0), first(bias_vectors))
ru = rectify_oa(u)
plot(u)
plot!(ru)
Out[172]:
0.75 1.00 1.25 1.50 -1.0 -0.5 0.0 0.5

Computation using support functions of the lazy intersection

In [179]:
W, b = weight_matrices[1], bias_vectors[1]
Out[179]:
([0.494084 0.0630657; 0.633579 0.338275], [0.928656, 0.548816])
In [180]:
result = H0
Z = AffineMap(W, result, b)
Out[180]:
AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([0.494084 0.0630657; 0.633579 0.338275], Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476]), [0.928656, 0.548816])
In [181]:
using LazySets: compute_union_of_projections!

R = Rectification(Z)
res = compute_union_of_projections!(R)
Out[181]:
UnionSetArray{Float64,LazySet{Float64}}(LazySet{Float64}[LinearMap{Float64,Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}},Float64,Diagonal{Float64,Array{Float64,1}}}([1.0 0.0; 0.0 0.0], Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}(AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([0.494084 0.0630657; 0.633579 0.338275], Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476]), [0.928656, 0.548816]), HPolyhedron{Float64}(HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1}[HalfSpace{Float64,SingleEntryVector{Float64}}([0.0, 1.0], 0.0)]), IntersectionCache(-1))), LinearMap{Float64,Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}},Float64,Diagonal{Float64,Array{Float64,1}}}([1.0 0.0; 0.0 1.0], Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}(AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([0.494084 0.0630657; 0.633579 0.338275], Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476]), [0.928656, 0.548816]), HPolyhedron{Float64}(HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1}[HalfSpace{Float64,SingleEntryVector{Float64}}([0.0, -1.0], 0.0)]), IntersectionCache(-1)))])
In [182]:
array(res)
Out[182]:
2-element Array{LazySet{Float64},1}:
 LinearMap{Float64,Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}},Float64,Diagonal{Float64,Array{Float64,1}}}([1.0 0.0; 0.0 0.0], Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}(AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([0.494084 0.0630657; 0.633579 0.338275], Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476]), [0.928656, 0.548816]), HPolyhedron{Float64}(HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1}[HalfSpace{Float64,SingleEntryVector{Float64}}([0.0, 1.0], 0.0)]), LazySets.IntersectionCache(-1))) 
 LinearMap{Float64,Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}},Float64,Diagonal{Float64,Array{Float64,1}}}([1.0 0.0; 0.0 1.0], Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}(AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([0.494084 0.0630657; 0.633579 0.338275], Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476]), [0.928656, 0.548816]), HPolyhedron{Float64}(HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1}[HalfSpace{Float64,SingleEntryVector{Float64}}([0.0, -1.0], 0.0)]), LazySets.IntersectionCache(-1)))
In [6]:
using Optim

# res_ch = overapproximate(ConvexHullArray(array(res)), HPolygon, 1e-2)
# the exact support vector of an intersection is not implemented
# this doesn't work: need that iterative refinement works with support functions . . .
In [210]:
res_ch = overapproximate(ConvexHullArray(array(res)), PolarDirections(40))

plot(res_ch)
Out[210]:
0.75 1.00 1.25 1.50 0.0 0.1 0.2 0.3 0.4
In [4]:
using LazySets: compute_union_of_projections!

function nnet_lazy(H0, weight_matrices, bias_vectors)
    relued_subsets = Vector{ConvexHullArray}()
    result = H0
    NUMLAYERS = length(bias_vectors)
    
    @inbounds for i in 1:NUMLAYERS
        W, b = weight_matrices[i], bias_vectors[i]

        # lazy affine map
        Z = AffineMap(W, result, b)

        # overapproximate with a box and rectify
        R = Rectification(Z)
        result = compute_union_of_projections!(R)
        result = helper_convexify(result)
        
        # Idea: make helper_convexify to return a concrete set, not a lazy set,
        # by using template directions

        push!(relued_subsets, result)
    end
    return relued_subsets
end

helper_convexify(res::UnionSetArray) = ConvexHullArray(array(res))
helper_convexify(res::LazySet) = ConvexHullArray([res]) # it is a single set => already convex
Out[4]:
helper_convexify (generic function with 2 methods)
In [224]:
result = nnet_lazy(H0, weight_matrices, bias_vectors);
In [232]:
plot(overapproximate.(result, Ref(PolarDirections(40))))

plot!(nnet_box(H0, weight_matrices, bias_vectors))
Out[232]:
1 2 3 4 0 1 2 3 4 5
In [233]:
@btime nnet_box($H0, $weight_matrices, $bias_vectors);

  4.556 μs (93 allocations: 6.92 KiB)
In [234]:
@btime nnet_lazy($H0, $weight_matrices, $bias_vectors);

  351.977 μs (4565 allocations: 402.23 KiB)

Lazy with template overapproximation

In [12]:
using LazySets.Approximations: AbstractDirections
using LazySets: compute_union_of_projections!
using Optim

function nnet_lazy_template(H0, weight_matrices, bias_vectors, dirs::Type{AbstractDirections})
    relued_subsets = Vector{HPolytope{Float64}}()
    result = H0
    NUMLAYERS = length(bias_vectors)
    
    @inbounds for i in 1:NUMLAYERS
        W, b = weight_matrices[i], bias_vectors[i]

        # lazy affine map
        Z = AffineMap(W, result, b)

        # overapproximate with a box and rectify
        R = Rectification(Z)
        result = compute_union_of_projections!(R)
        result = helper_convexify(result)
        n = size(W, 2) # state-space dimension
        result = overapproximate(result, dirs(n))

        push!(relued_subsets, result)
    end
    return relued_subsets
end
Out[12]:
nnet_lazy_template (generic function with 1 method)
In [250]:
result_lazy_template = nnet_lazy_template(H0, weight_matrices, bias_vectors, OctDirections(2));
In [260]:
result_lazy = nnet_lazy(H0, weight_matrices, bias_vectors);
plot(overapproximate.(result_lazy, Ref(PolarDirections(40))))

#plot!(nnet_box(H0, weight_matrices, bias_vectors))

plot!(nnet_lazy_template(H0, weight_matrices, bias_vectors, OctDirections(2)))
Out[260]:
1 2 3 4 0 1 2 3 4 5
In [262]:
@btime nnet_lazy_template($H0, $weight_matrices, $bias_vectors, OctDirections(2));

  1.863 ms (14384 allocations: 1.01 MiB)
In [264]:
@btime begin
    result_lazy = nnet_lazy(H0, weight_matrices, bias_vectors);
    overapproximate.(result_lazy, Ref(PolarDirections(40)))
end;

  9.366 ms (119685 allocations: 10.43 MiB)

So overapproximating at each layer is actually faster than overapproximated the nested lazy set (as expected), but it is less precise as the plot above shows.

In [267]:
@btime ρ([1.0, 1.0], nnet_lazy_template($H0, $weight_matrices, $bias_vectors, OctDirections(2))[1])

  1.889 ms (14465 allocations: 1.01 MiB)
Out[267]:
2.0356334604634667
In [268]:
@btime ρ([1.0, 1.0], nnet_lazy($H0, $weight_matrices, $bias_vectors)[1])

  398.471 μs (5138 allocations: 454.17 KiB)
Out[268]:
2.0356334604634667

However, if one is interested in checking the support function it is faster to use the nested lazy solution.

Computation using zonotopes

In [25]:
# (NOT TESTED YET)
using LazySets.Approximations: AbstractDirections
using LazySets: compute_union_of_projections!

function nnet_zonotope(H0, weight_matrices, bias_vectors)
    relued_subsets = [] #Vector{Zonotope{Float64}}()
    result = convert(Zonotope, H0)
    NUMLAYERS = length(bias_vectors)
    
    @inbounds for i in 1:NUMLAYERS
        W, b = weight_matrices[i], bias_vectors[i]

        # lazy affine map
        Z = translate(linear_map(W, result), b)

        # overapproximate with a box and rectify
        R = Rectification(Z)
        result = compute_union_of_projections!(R)
        result = helper_convexify(result)
        n = size(W, 2) # state-space dimension

        push!(relued_subsets, result)
    end
    return relued_subsets
end
Out[25]:
nnet_zonotope (generic function with 1 method)

Example: Small MNIST Network

In [6]:
model = "mnist_small.nnet"
nnet = read_nnet(networks_folder * model);

weight_matrices = [li.weights for li in nnet.layers]
bias_vectors = [li.bias for li in nnet.layers];

# entry 23 in MNIST datset
input_center = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,121,254,136,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,13,230,253,248,99,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,118,253,253,225,42,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,61,253,253,253,74,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,206,253,253,186,9,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,211,253,253,239,69,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,254,253,253,133,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,142,255,253,186,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,149,229,254,207,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,54,229,253,254,105,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,152,254,254,213,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,112,251,253,253,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,29,212,253,250,149,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,36,214,253,253,137,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,75,253,253,253,59,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,93,253,253,189,17,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,224,253,253,84,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,43,235,253,126,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,99,248,253,119,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,225,235,49,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
output_center = [-1311.1257826380004,4633.767704436501,-654.0718535670002,-1325.349417307,1175.2361184373997,-1897.8607293569007,-470.3405972940001,830.8337987382,-377.7467076115001,572.3674015264198]

in_epsilon = 1 # 0-255
out_epsilon = 10 # logit domain

input_low = input_center .- in_epsilon
input_high = input_center .+ in_epsilon

output_low = output_center .- out_epsilon
output_high = output_center .+ out_epsilon

inputSet = Hyperrectangle(low=input_low, high=input_high)
outputSet = Hyperrectangle(low=output_low, high=output_high);
In [7]:
dim(inputSet)
Out[7]:
784
In [8]:
[size(Wi) for Wi in weight_matrices]
Out[8]:
1-element Array{Tuple{Int64,Int64},1}:
 (10, 784)
In [10]:
sol = nnet_lazy(inputSet, weight_matrices, bias_vectors);
In [13]:
last(sol) ⊆ outputSet
Out[13]:
false
In [319]:
@btime last($sol) ⊆ $outputSet

  26.348 ms (12499 allocations: 24.50 MiB)
Out[319]:
false
In [14]:
UnionSetArray(array(last(sol))) ⊆ outputSet
Out[14]:
false
In [15]:
lazyOutput = AffineMap(weight_matrices[1], inputSet, bias_vectors[1])
Out[15]:
AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}([0.00967898 0.0158844 … 0.00187861 0.00280567; -0.00881655 0.00386361 … -0.00767655 -0.00259271; … ; 0.0112104 0.00166185 … 0.00131557 -0.00481982; 0.0125582 -0.00665823 … -0.00723359 0.0167881], Hyperrectangle{Float64}([0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0  …  0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0  …  1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]), [-0.400092, 0.375775, 0.136846, -0.239122, -0.00442209, 1.41899, -0.130078, 0.650365, -1.54558, -0.262676])
In [16]:
lazyOutput ⊆ outputSet
Out[16]:
false
In [34]:
clist_outputSet = constraints_list(outputSet)
for i in 1:20
    println(ρ(clist_outputSet[i].a, lazyOutput) - clist_outputSet[i].b)
end

225.68222898380077
-3064.2219268452013
1355.1437532860004
1857.3691126413996
-1952.0711050577993
1190.7207700330002
-334.7990287860008
-699.7209624162
1710.9447172774028
-957.8658273950796
-124.3432243801999
3163.0175082878
-1236.9149658119995
-1744.2769431326005
2071.525731197
-1082.747737300801
448.3263940379983
824.6886955401997
-1627.2915159395993
1069.0955757377603
In [ ]:

Example: Deep MNIST network

In [337]:
model = "mnist_large.nnet"
nnet = read_nnet(networks_folder * model);
In [338]:
length(nnet.layers)
Out[338]:
4
In [339]:
weight_matrices = [li.weights for li in nnet.layers]
bias_vectors = [li.bias for li in nnet.layers];
In [340]:
# See https://github.com/sisl/NeuralVerification.jl/blob/master/test/runtests2.jl#L50
# entry 23 in MNIST datset
input_center = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,121,254,136,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,13,230,253,248,99,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,118,253,253,225,42,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,61,253,253,253,74,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,206,253,253,186,9,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,211,253,253,239,69,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,254,253,253,133,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,142,255,253,186,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,149,229,254,207,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,54,229,253,254,105,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,152,254,254,213,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,112,251,253,253,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,29,212,253,250,149,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,36,214,253,253,137,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,75,253,253,253,59,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,93,253,253,189,17,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,224,253,253,84,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,43,235,253,126,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,99,248,253,119,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,225,235,49,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
output_center = [131.8781755,134.8987015,141.6166255,158.34307,129.8803525,104.8286425,98.64196,133.6358395,131.1716215,105.10621]

in_epsilon = 1 # 0-255
out_epsilon = 10 #logit domain

input_low = input_center .- in_epsilon
input_high = input_center .+ in_epsilon

output_low = output_center .- out_epsilon
output_high = output_center .+ out_epsilon

inputSet = Hyperrectangle(low=input_low, high=input_high)
outputSet = Hyperrectangle(low=output_low, high=output_high);
In [ ]:
[size(Wi) for Wi in weight_matrices]
In [ ]:
dim(inputSet)

The idea is to check that the result of the network is included in the outputSet.

In [341]:
sol = nnet_lazy(inputSet, weight_matrices, bias_vectors); # expensive

InterruptException:

Stacktrace:
 [1] materialize at ./boot.jl:402 [inlined]
 [2] broadcast(::typeof(*), ::Float64, ::LazySets.Arrays.SingleEntryVector{Float64}) at ./broadcast.jl:707
 [3] * at ./arraymath.jl:52 [inlined]
 [4] (::getfield(LazySets, Symbol("#f#285")){Array{Float64,1},AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},LazySets.Arrays.SingleEntryVector{Float64},Float64})(::Float64) at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:897
 [5] #optimize#77(::Float64, ::Float64, ::Int64, ::Bool, ::Bool, ::Nothing, ::Int64, ::Bool, ::typeof(optimize), ::getfield(LazySets, Symbol("#f#285")){Array{Float64,1},AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},LazySets.Arrays.SingleEntryVector{Float64},Float64}, ::Float64, ::Float64, ::Brent) at /Users/forets/.julia/packages/Optim/nEBWi/src/univariate/solvers/brent.jl:143
 [6] #optimize at ./none:0 [inlined]
 [7] #optimize#84 at /Users/forets/.julia/packages/Optim/nEBWi/src/univariate/optimize/interface.jl:21 [inlined]
 [8] (::getfield(Optim, Symbol("#kw##optimize")))(::NamedTuple{(:method,),Tuple{Brent}}, ::typeof(optimize), ::getfield(LazySets, Symbol("#f#285")){Array{Float64,1},AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},LazySets.Arrays.SingleEntryVector{Float64},Float64}, ::Float64, ::Float64) at ./none:0
 [9] #_line_search#284 at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:922 [inlined]
 [10] _line_search(::Array{Float64,1}, ::AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}}, ::HalfSpace{Float64,LazySets.Arrays.SingleEntryVector{Float64}}) at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:893
 [11] #ρ_helper#169(::Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}}, ::Function, ::Array{Float64,1}, ::Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HalfSpace{Float64,LazySets.Arrays.SingleEntryVector{Float64}}}, ::String) at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:271
 [12] ρ_helper at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:255 [inlined]
 [13] #ρ#170 at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:376 [inlined]
 [14] ρ at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:376 [inlined]
 [15] (::getfield(LazySets, Symbol("##173#174")){Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}},Array{Float64,1},Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}})(::HalfSpace{Float64,LazySets.Arrays.SingleEntryVector{Float64}}) at ./none:0
 [16] iterate at ./generator.jl:47 [inlined]
 [17] collect_to!(::Array{Float64,1}, ::Base.Generator{Array{HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1},1},getfield(LazySets, Symbol("##173#174")){Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}},Array{Float64,1},Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}}}, ::Int64, ::Int64) at ./array.jl:651
 [18] collect_to_with_first!(::Array{Float64,1}, ::Float64, ::Base.Generator{Array{HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1},1},getfield(LazySets, Symbol("##173#174")){Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}},Array{Float64,1},Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}}}, ::Int64) at ./array.jl:630
 [19] collect(::Base.Generator{Array{HalfSpace{Float64,VN} where VN<:AbstractArray{Float64,1},1},getfield(LazySets, Symbol("##173#174")){Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}},Array{Float64,1},Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}}}) at ./array.jl:611
 [20] #ρ#172(::Base.Iterators.Pairs{Union{},Union{},Tuple{},NamedTuple{(),Tuple{}}}, ::Function, ::Array{Float64,1}, ::Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}}) at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:424
 [21] ρ at /Users/forets/.julia/dev/LazySets/src/Intersection.jl:423 [inlined]
 [22] #ρ#184 at /Users/forets/.julia/dev/LazySets/src/LinearMap.jl:191 [inlined]
 [23] ρ at /Users/forets/.julia/dev/LazySets/src/LinearMap.jl:191 [inlined]
 [24] (::getfield(LazySets, Symbol("##161#162")){Array{Float64,1}})(::LinearMap{Float64,Intersection{Float64,AffineMap{Float64,Hyperrectangle{Float64},Float64,Array{Float64,2},Array{Float64,1}},HPolyhedron{Float64}},Float64,Diagonal{Float64,Array{Float64,1}}}) at ./none:0
 [25] iterate at ./generator.jl:47 [inlined]
 [26] collect_to!(::Array{Float64,1}, ::Base.Generator{Array{LazySet{Float64},1},getfield(LazySets, Symbol("##161#162")){Array{Float64,1}}}, ::Int64, ::Int64) at ./array.jl:651
 [27] collect_to_with_first!(::Array{Float64,1}, ::Float64, ::Base.Generator{Array{LazySet{Float64},1},getfield(LazySets, Symbol("##161#162")){Array{Float64,1}}}, ::Int64) at ./array.jl:630
 [28] collect(::Base.Generator{Array{LazySet{Float64},1},getfield(LazySets, Symbol("##161#162")){Array{Float64,1}}}) at ./array.jl:611
 [29] ρ(::Array{Float64,1}, ::ConvexHullArray{Float64,LazySet{Float64}}) at /Users/forets/.julia/dev/LazySets/src/ConvexHull.jl:318
 [30] ρ(::LazySets.Arrays.SingleEntryVector{Float64}, ::AffineMap{Float64,ConvexHullArray{Float64,LazySet{Float64}},Float64,Array{Float64,2},Array{Float64,1}}) at /Users/forets/.julia/dev/LazySets/src/AffineMap.jl:159
 [31] compute_union_of_projections!(::Rectification{Float64,AffineMap{Float64,ConvexHullArray{Float64,LazySet{Float64}},Float64,Array{Float64,2},Array{Float64,1}}}) at /Users/forets/.julia/dev/LazySets/src/Rectification.jl:491
 [32] nnet_lazy(::Hyperrectangle{Float64}, ::Array{Array{Float64,2},1}, ::Array{Array{Float64,1},1}) at ./In[220]:14
 [33] top-level scope at In[341]:1
In [24]:
sol = nnet_lazy_template(inputSet, weight_matrices, bias_vectors, BoxDirections);

MethodError: no method matching nnet_lazy_template(::Hyperrectangle{Float64}, ::Array{Array{Float64,2},1}, ::Array{Array{Float64,1},1}, ::Type{BoxDirections})
Closest candidates are:
  nnet_lazy_template(::Any, ::Any, ::Any, !Matched::Type{AbstractDirections}) at In[16]:5

Stacktrace:
 [1] top-level scope at In[24]:1
In [ ]: