{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This notebook is an experiment with the [NeuralVerification](https://github.com/sisl/NeuralVerification.jl) package (that we shorten to `NV` here) and decomposition methods available in [LazySets](https://github.com/JuliaReach/LazySets.jl/)."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"\"/Users/forets/.julia/dev/NeuralVerification/examples/networks/\""
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"using Revise, NeuralVerification, LazySets # requires schillic/1176_supportfunction\n",
"using LazySets.Approximations\n",
"\n",
"const NV = NeuralVerification\n",
"\n",
"networks_folder = \"/Users/forets/.julia/dev/NeuralVerification/examples/networks/\""
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In `NV`, [neural networks](https://en.wikipedia.org/wiki/Neural_network#/media/File:Neural_network_example.svg) are represented as a [vector of layers](https://github.com/sisl/NeuralVerification.jl/blob/master/src/utils/network.jl#L40), where a `Layer` consists of the weights matrix, the bias (an affine translation) and the [activation function](https://en.wikipedia.org/wiki/Activation_function).\n",
"\n",
"\n",
"```julia\n",
"struct Layer{F<:ActivationFunction, N<:Number}\n",
" weights::Matrix{N}\n",
" bias::Vector{N}\n",
" activation::F\n",
"end\n",
"\n",
"struct Network\n",
" layers::Vector{Layer} # layers includes output layer\n",
"end\n",
"```"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we will work with one \"small\" examples in [NeuralVerification/examples/networks/](https://github.com/sisl/NeuralVerification.jl/tree/master/examples)."
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [],
"source": [
"model = \"cartpole_nnet.nnet\" # 4 layers, first one 16x4 and the other ones 16 x 16\n",
"#model = \"ACASXU_run2a_4_5_batch_2000.nnet\" # 7 layers, 50x5 \n",
"#model = \"mnist1.nnet\" # 25 x 784 and 10 x 25\n",
"#model = \"mnist_large.nnet\" # 25 x 784 and 10 x 25\n",
"#model = \"mnist2.nnet\" # 100 x 784 and 10 x 100\n",
"\n",
"nnet = read_nnet(networks_folder * model);"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Network"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"typeof(nnet)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The number of layers in this neural network as well as the number of nodes in each layer can be obtained as follows."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L = nnet.layers\n",
"length(L)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The first two layers have two nodes each and the last layer (the output layer) has one node."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4-element Array{Int64,1}:\n",
" 16\n",
" 16\n",
" 16\n",
" 2"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"NV.n_nodes.(L)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"NeuralVerification.Layer{NeuralVerification.ReLU,Float64}\n",
" 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]\n",
" 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]\n",
" activation: NeuralVerification.ReLU NeuralVerification.ReLU()\n"
]
}
],
"source": [
"dump(L[1])"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4-element Array{Tuple{Int64,Int64},1}:\n",
" (16, 4) \n",
" (16, 16)\n",
" (16, 16)\n",
" (2, 16) "
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[size(Li.weights) for Li in L]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can directly see the weights matrix and the bias fields of the first layer:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"16×4 Array{Float64,2}:\n",
" -1.04327 -0.455724 0.192542 0.192542 \n",
" -0.0191024 -0.969242 0.154406 0.154406 \n",
" -0.418161 0.37731 -0.341209 -0.341209 \n",
" -0.576796 -0.503059 0.62542 0.62542 \n",
" 0.00491105 -0.359143 -0.177293 -0.177293 \n",
" -0.508361 -0.335279 -0.179524 -0.179524 \n",
" -0.218255 -0.288024 0.00792378 0.00792378\n",
" 0.0605804 -0.0435269 -0.305204 -0.305204 \n",
" 0.685469 2.4089 -1.51407 -1.51407 \n",
" -0.488534 -1.14581 -1.74527 -1.74527 \n",
" -2.32975 -1.76154 0.817765 0.817765 \n",
" 0.801403 -1.36655 -1.20426 -1.20426 \n",
" 0.197374 0.459956 -0.342471 -0.342471 \n",
" -0.189495 -0.277776 -0.40308 -0.40308 \n",
" -0.0467679 -0.482105 0.119671 0.119671 \n",
" 0.0445579 -0.290073 -0.389191 -0.389191 "
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L[1].weights"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"n = size(L[1].weights)[2]"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"16-element Array{Float64,1}:\n",
" -0.13889389 \n",
" 0.5759869 \n",
" -0.32110757 \n",
" 0.52708554 \n",
" 0.5855289 \n",
" 0.01758425 \n",
" -0.35979664 \n",
" 0.6125208 \n",
" 0.5478964 \n",
" -0.4406496 \n",
" 0.4447836 \n",
" -0.3337182 \n",
" 0.5095051 \n",
" 0.54117775 \n",
" 0.42754632 \n",
" -0.062375117"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L[1].bias"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Random input set for `cartpole`:"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Hyperrectangle{Float64}([-0.93869, -1.73698, 1.26868, -1.60686], [0.780393, 1.35098, 0.555982, 0.798388])"
]
},
"execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"H0 = rand(Hyperrectangle, dim=n)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"An input set for ACAS is defined in the `test/runtime3.jl` file so we use it:"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"ename": "UndefVarError",
"evalue": "UndefVarError: H not defined",
"output_type": "error",
"traceback": [
"UndefVarError: H not defined",
"",
"Stacktrace:",
" [1] top-level scope at In[14]:4"
]
}
],
"source": [
"center = [0.40143256, 0.30570418, -0.49920412, 0.52838383, 0.4]\n",
"radius = [0.0015, 0.0015, 0.0015, 0.0015, 0.0015]\n",
"H0 = Hyperrectangle(center, radius)\n",
"dim(H)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let $X_1$ be the set obtained after we apply the first layer, $X_1 = A_1 H_0 \\oplus b_1$."
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"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])"
]
},
"execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"A1 = L[1].weights\n",
"b1 = L[1].bias\n",
"X1 = A1 * H0 ⊕ b1"
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"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])"
]
},
"execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"X1_am = AffineMap(A1, H0, b1) # as an affine map"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Dimension of $X_1$:"
]
},
{
"cell_type": "code",
"execution_count": 27,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"16"
]
},
"execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"dim(X1)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's consider an element from $X_1$ and apply the rectification operation:"
]
},
{
"cell_type": "code",
"execution_count": 28,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"10-element Array{Float64,1}:\n",
" 1.5668862667477603 \n",
" 2.2252558663740523 \n",
" -0.46857571250598584\n",
" 1.7308201688049678 \n",
" 1.2646987334890278 \n",
" 1.137861079104094 \n",
" 0.3426900280822721 \n",
" 0.7344725338725435 \n",
" -3.767735876188037 \n",
" 2.5983865765364436 "
]
},
"execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"an_element(X1)[1:10]"
]
},
{
"cell_type": "code",
"execution_count": 29,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"10-element Array{Float64,1}:\n",
" 1.5668862667477603\n",
" 2.2252558663740523\n",
" 0.0 \n",
" 1.7308201688049678\n",
" 1.2646987334890278\n",
" 1.137861079104094 \n",
" 0.3426900280822721\n",
" 0.7344725338725435\n",
" 0.0 \n",
" 2.5983865765364436"
]
},
"execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"v = LazySets.rectify(an_element(X1))\n",
"v[1:10]"
]
},
{
"cell_type": "code",
"execution_count": 30,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"13"
]
},
"execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"count(!iszero, v) # number of elements which are not zero"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"rectify (generic function with 1 method)"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"function rectify(H::AbstractHyperrectangle)\n",
" Hyperrectangle(low=LazySets.rectify(low(H)), high=LazySets.rectify(high(H)))\n",
"end"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"rectify_oa (generic function with 1 method)"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"rectify_oa(X) = rectify(box_approximation(X))"
]
},
{
"cell_type": "code",
"execution_count": 33,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"2-element Array{Float64,1}:\n",
" 0.55694838727371 \n",
" 0.11141458040479368"
]
},
"execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"LazySets.rectify(rand(2))"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"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])"
]
},
"execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"X1_r = rectify_oa(X1) # concrete set"
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"16"
]
},
"execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"dim(X1_r)"
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"16×16 Array{Float64,2}:\n",
" -0.969095 -0.74201 -1.26007 … -0.112787 -0.19606 -0.19606 \n",
" 0.391285 0.104401 0.0870455 -0.107367 0.0719031 0.0719031\n",
" 0.486037 -1.20122 -0.0789432 0.105409 0.15682 0.15682 \n",
" 0.285405 0.714511 0.616202 0.281021 -0.48508 -0.48508 \n",
" 0.403812 -0.113225 0.0332528 0.284097 -0.616485 -0.616485 \n",
" -0.237504 -0.727784 -0.312868 … -2.076 0.112664 0.112664 \n",
" 0.537505 -0.954175 -0.271187 0.103498 -0.317254 -0.317254 \n",
" 1.09746 0.491936 0.648663 0.449617 -0.894633 -0.894633 \n",
" 0.680387 0.384532 0.618043 0.0395887 -0.29143 -0.29143 \n",
" 0.0707292 -1.31967 -0.540485 -0.0290527 -0.369389 -0.369389 \n",
" 0.415719 0.419337 0.110925 … 0.094451 -0.170903 -0.170903 \n",
" -0.830163 -2.33168 -2.10379 -1.38456 0.428579 0.428579 \n",
" 0.330955 0.431738 0.608234 0.232867 -0.506954 -0.506954 \n",
" 0.482378 0.207244 0.289128 0.121406 -0.295695 -0.295695 \n",
" -0.341974 -0.853769 -0.362243 -0.830389 0.101125 0.101125 \n",
" -0.961889 -1.17588 -0.598615 … -1.20583 -0.29188 -0.29188 "
]
},
"execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L[2].weights"
]
},
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"X2 (generic function with 1 method)"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# next layer\n",
"A2 = L[2].weights\n",
"b2 = L[2].bias\n",
"X2(Y) = A2 * (Y) ⊕ b2"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Running example in 2D"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"using Plots, LazySets, LazySets.Approximations\n",
"using LazySets: translate"
]
},
{
"cell_type": "code",
"execution_count": 164,
"metadata": {},
"outputs": [],
"source": [
"# generate some data\n",
"\n",
"NUMLAYERS = 5\n",
"weight_matrices = [rand(2, 2) for i in 1:NUMLAYERS]\n",
"bias_vectors = [rand(2) for i in 1:NUMLAYERS];"
]
},
{
"cell_type": "code",
"execution_count": 165,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Hyperrectangle{Float64}([0.841145, -4.49627], [0.911519, 0.962476])"
]
},
"execution_count": 165,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# initial set\n",
"H0 = Hyperrectangle{Float64}([0.841145, -4.496269], [0.911519, 0.962476])"
]
},
{
"cell_type": "code",
"execution_count": 166,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4-element Array{Array{Float64,1},1}:\n",
" [1.75266, -3.53379] \n",
" [-0.070374, -3.53379]\n",
" [1.75266, -5.45874] \n",
" [-0.070374, -5.45874]"
]
},
"execution_count": 166,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"vertices_list(H0)"
]
},
{
"cell_type": "code",
"execution_count": 167,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 167,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# showing the set after the first application of affine map\n",
"plot(H0, color=:blue)\n",
"W, b = weight_matrices[1], bias_vectors[1]\n",
"plot!(translate(linear_map(W, H0), b), color=:red)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Computation with a box overapproximation of the RELU set"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"nnet_box (generic function with 1 method)"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"function nnet_box(H0, weight_matrices, bias_vectors)\n",
" relued_subsets = Vector{Hyperrectangle{Float64}}()\n",
" result = H0\n",
" NUMLAYERS = length(bias_vectors)\n",
" \n",
" @inbounds for i in 1:NUMLAYERS\n",
" W, b = weight_matrices[i], bias_vectors[i]\n",
"\n",
" # lazy affine map\n",
" Z = AffineMap(W, result, b) \n",
"\n",
" # overapproximate with a box and rectify\n",
" result = rectify_oa(Z)\n",
" push!(relued_subsets, result)\n",
" end\n",
" return relued_subsets\n",
"end"
]
},
{
"cell_type": "code",
"execution_count": 169,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"5-element Array{Hyperrectangle{Float64},1}:\n",
" Hyperrectangle{Float64}([1.06069, 0.231937], [0.511066, 0.231937])\n",
" Hyperrectangle{Float64}([1.02693, 1.6348], [0.530903, 0.548743]) \n",
" Hyperrectangle{Float64}([1.94862, 2.68314], [0.627423, 0.655323]) \n",
" Hyperrectangle{Float64}([3.26642, 2.83915], [0.660316, 0.671064]) \n",
" Hyperrectangle{Float64}([3.27148, 4.87029], [0.647365, 0.880383]) "
]
},
"execution_count": 169,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"relued_subsets = nnet_box(H0, weight_matrices, bias_vectors)"
]
},
{
"cell_type": "code",
"execution_count": 170,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 170,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"plot(relued_subsets)\n",
"plot!(first(relued_subsets), color=:red)\n",
"plot!(last(relued_subsets), color=:grey)"
]
},
{
"cell_type": "code",
"execution_count": 171,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 171,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"plot!(translate(linear_map(first(weight_matrices), H0), first(bias_vectors)), color=:red)\n",
"plot!(H0)"
]
},
{
"cell_type": "code",
"execution_count": 172,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 172,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"u = translate(linear_map(first(weight_matrices), H0), first(bias_vectors))\n",
"ru = rectify_oa(u)\n",
"plot(u)\n",
"plot!(ru)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Computation using support functions of the lazy intersection"
]
},
{
"cell_type": "code",
"execution_count": 179,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"([0.494084 0.0630657; 0.633579 0.338275], [0.928656, 0.548816])"
]
},
"execution_count": 179,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"W, b = weight_matrices[1], bias_vectors[1]"
]
},
{
"cell_type": "code",
"execution_count": 180,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"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])"
]
},
"execution_count": 180,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"result = H0\n",
"Z = AffineMap(W, result, b) "
]
},
{
"cell_type": "code",
"execution_count": 181,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"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)))])"
]
},
"execution_count": 181,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"using LazySets: compute_union_of_projections!\n",
"\n",
"R = Rectification(Z)\n",
"res = compute_union_of_projections!(R)"
]
},
{
"cell_type": "code",
"execution_count": 182,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"2-element Array{LazySet{Float64},1}:\n",
" 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))) \n",
" 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)))"
]
},
"execution_count": 182,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"array(res)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [],
"source": [
"using Optim\n",
"\n",
"# res_ch = overapproximate(ConvexHullArray(array(res)), HPolygon, 1e-2)\n",
"# the exact support vector of an intersection is not implemented\n",
"# this doesn't work: need that iterative refinement works with support functions . . ."
]
},
{
"cell_type": "code",
"execution_count": 210,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 210,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"res_ch = overapproximate(ConvexHullArray(array(res)), PolarDirections(40))\n",
"\n",
"plot(res_ch)"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"helper_convexify (generic function with 2 methods)"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"using LazySets: compute_union_of_projections!\n",
"\n",
"function nnet_lazy(H0, weight_matrices, bias_vectors)\n",
" relued_subsets = Vector{ConvexHullArray}()\n",
" result = H0\n",
" NUMLAYERS = length(bias_vectors)\n",
" \n",
" @inbounds for i in 1:NUMLAYERS\n",
" W, b = weight_matrices[i], bias_vectors[i]\n",
"\n",
" # lazy affine map\n",
" Z = AffineMap(W, result, b)\n",
"\n",
" # overapproximate with a box and rectify\n",
" R = Rectification(Z)\n",
" result = compute_union_of_projections!(R)\n",
" result = helper_convexify(result)\n",
" \n",
" # Idea: make helper_convexify to return a concrete set, not a lazy set,\n",
" # by using template directions\n",
"\n",
" push!(relued_subsets, result)\n",
" end\n",
" return relued_subsets\n",
"end\n",
"\n",
"helper_convexify(res::UnionSetArray) = ConvexHullArray(array(res))\n",
"helper_convexify(res::LazySet) = ConvexHullArray([res]) # it is a single set => already convex"
]
},
{
"cell_type": "code",
"execution_count": 224,
"metadata": {},
"outputs": [],
"source": [
"result = nnet_lazy(H0, weight_matrices, bias_vectors);"
]
},
{
"cell_type": "code",
"execution_count": 232,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 232,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"plot(overapproximate.(result, Ref(PolarDirections(40))))\n",
"\n",
"plot!(nnet_box(H0, weight_matrices, bias_vectors))"
]
},
{
"cell_type": "code",
"execution_count": 233,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 4.556 μs (93 allocations: 6.92 KiB)\n"
]
}
],
"source": [
"@btime nnet_box($H0, $weight_matrices, $bias_vectors);"
]
},
{
"cell_type": "code",
"execution_count": 234,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 351.977 μs (4565 allocations: 402.23 KiB)\n"
]
}
],
"source": [
"@btime nnet_lazy($H0, $weight_matrices, $bias_vectors);"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Lazy with template overapproximation"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"nnet_lazy_template (generic function with 1 method)"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"using LazySets.Approximations: AbstractDirections\n",
"using LazySets: compute_union_of_projections!\n",
"using Optim\n",
"\n",
"function nnet_lazy_template(H0, weight_matrices, bias_vectors, dirs::Type{AbstractDirections})\n",
" relued_subsets = Vector{HPolytope{Float64}}()\n",
" result = H0\n",
" NUMLAYERS = length(bias_vectors)\n",
" \n",
" @inbounds for i in 1:NUMLAYERS\n",
" W, b = weight_matrices[i], bias_vectors[i]\n",
"\n",
" # lazy affine map\n",
" Z = AffineMap(W, result, b)\n",
"\n",
" # overapproximate with a box and rectify\n",
" R = Rectification(Z)\n",
" result = compute_union_of_projections!(R)\n",
" result = helper_convexify(result)\n",
" n = size(W, 2) # state-space dimension\n",
" result = overapproximate(result, dirs(n))\n",
"\n",
" push!(relued_subsets, result)\n",
" end\n",
" return relued_subsets\n",
"end"
]
},
{
"cell_type": "code",
"execution_count": 250,
"metadata": {},
"outputs": [],
"source": [
"result_lazy_template = nnet_lazy_template(H0, weight_matrices, bias_vectors, OctDirections(2));"
]
},
{
"cell_type": "code",
"execution_count": 260,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n"
]
},
"execution_count": 260,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"result_lazy = nnet_lazy(H0, weight_matrices, bias_vectors);\n",
"plot(overapproximate.(result_lazy, Ref(PolarDirections(40))))\n",
"\n",
"#plot!(nnet_box(H0, weight_matrices, bias_vectors))\n",
"\n",
"plot!(nnet_lazy_template(H0, weight_matrices, bias_vectors, OctDirections(2)))"
]
},
{
"cell_type": "code",
"execution_count": 262,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 1.863 ms (14384 allocations: 1.01 MiB)\n"
]
}
],
"source": [
"@btime nnet_lazy_template($H0, $weight_matrices, $bias_vectors, OctDirections(2));"
]
},
{
"cell_type": "code",
"execution_count": 264,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 9.366 ms (119685 allocations: 10.43 MiB)\n"
]
}
],
"source": [
"@btime begin\n",
" result_lazy = nnet_lazy(H0, weight_matrices, bias_vectors);\n",
" overapproximate.(result_lazy, Ref(PolarDirections(40)))\n",
"end;"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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."
]
},
{
"cell_type": "code",
"execution_count": 267,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 1.889 ms (14465 allocations: 1.01 MiB)\n"
]
},
{
"data": {
"text/plain": [
"2.0356334604634667"
]
},
"execution_count": 267,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"@btime ρ([1.0, 1.0], nnet_lazy_template($H0, $weight_matrices, $bias_vectors, OctDirections(2))[1])"
]
},
{
"cell_type": "code",
"execution_count": 268,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 398.471 μs (5138 allocations: 454.17 KiB)\n"
]
},
{
"data": {
"text/plain": [
"2.0356334604634667"
]
},
"execution_count": 268,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"@btime ρ([1.0, 1.0], nnet_lazy($H0, $weight_matrices, $bias_vectors)[1])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"However, if one is interested in checking the support function it is faster to use the nested lazy solution."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Computation using zonotopes"
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"nnet_zonotope (generic function with 1 method)"
]
},
"execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# (NOT TESTED YET)\n",
"using LazySets.Approximations: AbstractDirections\n",
"using LazySets: compute_union_of_projections!\n",
"\n",
"function nnet_zonotope(H0, weight_matrices, bias_vectors)\n",
" relued_subsets = [] #Vector{Zonotope{Float64}}()\n",
" result = convert(Zonotope, H0)\n",
" NUMLAYERS = length(bias_vectors)\n",
" \n",
" @inbounds for i in 1:NUMLAYERS\n",
" W, b = weight_matrices[i], bias_vectors[i]\n",
"\n",
" # lazy affine map\n",
" Z = translate(linear_map(W, result), b)\n",
"\n",
" # overapproximate with a box and rectify\n",
" R = Rectification(Z)\n",
" result = compute_union_of_projections!(R)\n",
" result = helper_convexify(result)\n",
" n = size(W, 2) # state-space dimension\n",
"\n",
" push!(relued_subsets, result)\n",
" end\n",
" return relued_subsets\n",
"end"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Example: Small MNIST Network"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [],
"source": [
"model = \"mnist_small.nnet\"\n",
"nnet = read_nnet(networks_folder * model);\n",
"\n",
"weight_matrices = [li.weights for li in nnet.layers]\n",
"bias_vectors = [li.bias for li in nnet.layers];\n",
"\n",
"# entry 23 in MNIST datset\n",
"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]\n",
"output_center = [-1311.1257826380004,4633.767704436501,-654.0718535670002,-1325.349417307,1175.2361184373997,-1897.8607293569007,-470.3405972940001,830.8337987382,-377.7467076115001,572.3674015264198]\n",
"\n",
"in_epsilon = 1 # 0-255\n",
"out_epsilon = 10 # logit domain\n",
"\n",
"input_low = input_center .- in_epsilon\n",
"input_high = input_center .+ in_epsilon\n",
"\n",
"output_low = output_center .- out_epsilon\n",
"output_high = output_center .+ out_epsilon\n",
"\n",
"inputSet = Hyperrectangle(low=input_low, high=input_high)\n",
"outputSet = Hyperrectangle(low=output_low, high=output_high);"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"784"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"dim(inputSet)"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"1-element Array{Tuple{Int64,Int64},1}:\n",
" (10, 784)"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[size(Wi) for Wi in weight_matrices]"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [],
"source": [
"sol = nnet_lazy(inputSet, weight_matrices, bias_vectors);"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"false"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"last(sol) ⊆ outputSet"
]
},
{
"cell_type": "code",
"execution_count": 319,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" 26.348 ms (12499 allocations: 24.50 MiB)\n"
]
},
{
"data": {
"text/plain": [
"false"
]
},
"execution_count": 319,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"@btime last($sol) ⊆ $outputSet"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"false"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"UnionSetArray(array(last(sol))) ⊆ outputSet"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"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])"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"lazyOutput = AffineMap(weight_matrices[1], inputSet, bias_vectors[1])"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"false"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"lazyOutput ⊆ outputSet"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"225.68222898380077\n",
"-3064.2219268452013\n",
"1355.1437532860004\n",
"1857.3691126413996\n",
"-1952.0711050577993\n",
"1190.7207700330002\n",
"-334.7990287860008\n",
"-699.7209624162\n",
"1710.9447172774028\n",
"-957.8658273950796\n",
"-124.3432243801999\n",
"3163.0175082878\n",
"-1236.9149658119995\n",
"-1744.2769431326005\n",
"2071.525731197\n",
"-1082.747737300801\n",
"448.3263940379983\n",
"824.6886955401997\n",
"-1627.2915159395993\n",
"1069.0955757377603\n"
]
}
],
"source": [
"clist_outputSet = constraints_list(outputSet)\n",
"for i in 1:20\n",
" println(ρ(clist_outputSet[i].a, lazyOutput) - clist_outputSet[i].b)\n",
"end"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Example: Deep MNIST network"
]
},
{
"cell_type": "code",
"execution_count": 337,
"metadata": {},
"outputs": [],
"source": [
"model = \"mnist_large.nnet\"\n",
"nnet = read_nnet(networks_folder * model);"
]
},
{
"cell_type": "code",
"execution_count": 338,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4"
]
},
"execution_count": 338,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"length(nnet.layers)"
]
},
{
"cell_type": "code",
"execution_count": 339,
"metadata": {},
"outputs": [],
"source": [
"weight_matrices = [li.weights for li in nnet.layers]\n",
"bias_vectors = [li.bias for li in nnet.layers];"
]
},
{
"cell_type": "code",
"execution_count": 340,
"metadata": {},
"outputs": [],
"source": [
"# See https://github.com/sisl/NeuralVerification.jl/blob/master/test/runtests2.jl#L50\n",
"# entry 23 in MNIST datset\n",
"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]\n",
"output_center = [131.8781755,134.8987015,141.6166255,158.34307,129.8803525,104.8286425,98.64196,133.6358395,131.1716215,105.10621]\n",
"\n",
"in_epsilon = 1 # 0-255\n",
"out_epsilon = 10 #logit domain\n",
"\n",
"input_low = input_center .- in_epsilon\n",
"input_high = input_center .+ in_epsilon\n",
"\n",
"output_low = output_center .- out_epsilon\n",
"output_high = output_center .+ out_epsilon\n",
"\n",
"inputSet = Hyperrectangle(low=input_low, high=input_high)\n",
"outputSet = Hyperrectangle(low=output_low, high=output_high);"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"[size(Wi) for Wi in weight_matrices]"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"dim(inputSet)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The idea is to check that the result of the network is included in the `outputSet`."
]
},
{
"cell_type": "code",
"execution_count": 341,
"metadata": {},
"outputs": [
{
"ename": "InterruptException",
"evalue": "InterruptException:",
"output_type": "error",
"traceback": [
"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"
]
}
],
"source": [
"sol = nnet_lazy(inputSet, weight_matrices, bias_vectors); # expensive"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [
{
"ename": "MethodError",
"evalue": "MethodError: no method matching nnet_lazy_template(::Hyperrectangle{Float64}, ::Array{Array{Float64,2},1}, ::Array{Array{Float64,1},1}, ::Type{BoxDirections})\nClosest candidates are:\n nnet_lazy_template(::Any, ::Any, ::Any, !Matched::Type{AbstractDirections}) at In[16]:5",
"output_type": "error",
"traceback": [
"MethodError: no method matching nnet_lazy_template(::Hyperrectangle{Float64}, ::Array{Array{Float64,2},1}, ::Array{Array{Float64,1},1}, ::Type{BoxDirections})\nClosest candidates are:\n nnet_lazy_template(::Any, ::Any, ::Any, !Matched::Type{AbstractDirections}) at In[16]:5",
"",
"Stacktrace:",
" [1] top-level scope at In[24]:1"
]
}
],
"source": [
"sol = nnet_lazy_template(inputSet, weight_matrices, bias_vectors, BoxDirections);"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"@webio": {
"lastCommId": null,
"lastKernelId": null
},
"kernelspec": {
"display_name": "Julia 1.1.0-rc2",
"language": "julia",
"name": "julia-1.1"
},
"language_info": {
"file_extension": ".jl",
"mimetype": "application/julia",
"name": "julia",
"version": "1.1.0"
}
},
"nbformat": 4,
"nbformat_minor": 2
}