{ "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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0.0\n", "\n", "\n", "0.5\n", "\n", "\n", "1.0\n", "\n", "\n", "1.5\n", "\n", "\n", "-5\n", "\n", "\n", "-4\n", "\n", "\n", "-3\n", "\n", "\n", "-2\n", "\n", "\n", "-1\n", "\n", "\n", "0\n", "\n", "\n", "\n", "\n", "\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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "0\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "5\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "-5.0\n", "\n", "\n", "-2.5\n", "\n", "\n", "0.0\n", "\n", "\n", "2.5\n", "\n", "\n", "5.0\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0.75\n", "\n", "\n", "1.00\n", "\n", "\n", "1.25\n", "\n", "\n", "1.50\n", "\n", "\n", "-1.0\n", "\n", "\n", "-0.5\n", "\n", "\n", "0.0\n", "\n", "\n", "0.5\n", "\n", "\n", "\n", "\n", "\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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0.75\n", "\n", "\n", "1.00\n", "\n", "\n", "1.25\n", "\n", "\n", "1.50\n", "\n", "\n", "0.0\n", "\n", "\n", "0.1\n", "\n", "\n", "0.2\n", "\n", "\n", "0.3\n", "\n", "\n", "0.4\n", "\n", "\n", "\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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "0\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "5\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\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", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "0\n", "\n", "\n", "1\n", "\n", "\n", "2\n", "\n", "\n", "3\n", "\n", "\n", "4\n", "\n", "\n", "5\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\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 }