example_notebook.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "31a8c462-1ef7-42fd-bd73-756d2e581125",
   "metadata": {},
   "source": [
    "# Example Notebook for DPNeurifyFV\n",
    "\n",
    "To make sure the notebook runs with the `DPNeurifyFV` environment, activate the directory with the corresponding `Project.toml` in Julia's package manager.\n",
    "\n",
    "**General note**: Julia precompiles a function, when it is first used. This may lead to the first execution to be rather slow. It should be much faster, for the second execution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "1f07f195-6c21-4faa-a2de-54e2eed8790b",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\u001b[32m\u001b[1m  Activating\u001b[22m\u001b[39m environment at `~/VerifyNN/DPNeurifyFV/Project.toml`\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001b[36m\u001b[1m     Project\u001b[22m\u001b[39m "
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "DPNeurifyFV v0.1.0\n",
      "\u001b[32m\u001b[1m      Status\u001b[22m\u001b[39m `~/VerifyNN/DPNeurifyFV/Project.toml`\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " \u001b[90m [864edb3b] \u001b[39mDataStructures v0.18.11\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " \u001b[90m [b4f0291d] \u001b[39mLazySets v1.56.3\n",
      " \u001b[90m [7e1232c4] \u001b[39mNeuralPriorityOptimizer v0.1.0 `https://github.com/sisl/NeuralPriorityOptimizer.jl#main`\n",
      " \u001b[90m [146f25fa] \u001b[39mNeuralVerification v0.1.0 `https://github.com/sisl/NeuralVerification.jl#0d9be34`\n",
      " \u001b[90m [d96e819e] \u001b[39mParameters v0.12.3\n",
      " \u001b[90m [37e2e46d] \u001b[39mLinearAlgebra\n"
     ]
    }
   ],
   "source": [
    "import Pkg\n",
    "Pkg.activate(\".\")\n",
    "Pkg.status()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ab903261-113b-4810-a735-154cef6619ec",
   "metadata": {},
   "source": [
    "Import the necessary packages `DPNeurifyFV`, `NeuralVerification` and `LazySets`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "id": "44c07727-a3b2-485c-ad41-54bf8878dd18",
   "metadata": {},
   "outputs": [],
   "source": [
    "using NeuralVerification, DPNeurifyFV, LazySets"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a649d8b4-441a-40e4-b372-3956e7c13071",
   "metadata": {},
   "source": [
    "We are going to demonstrate the functionality on the example of the first ACAS-Xu network operating on the input defined in property $\\phi_1$.\n",
    "\n",
    "After loading the network, we convert it into a format that stores the negative and positive weights separately to make the symbolic forward pass with `DPNeurifyFV` more efficient."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "e2de206a-37eb-4d9f-a91b-db907c3cf69b",
   "metadata": {},
   "outputs": [],
   "source": [
    "input_set, output_set = DPNeurifyFV.get_acas_sets(1)\n",
    "\n",
    "acas = read_nnet(\"./networks/ACASXU_experimental_v2a_1_1.nnet\")\n",
    "acas_npi = NetworkNegPosIdx(acas);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b524af81-678d-4cd7-8ce9-33a0760bcbb6",
   "metadata": {},
   "source": [
    "## Single Forward Pass\n",
    "\n",
    "We demonstrate the effect of introducing the maximum number of fresh variables (the original idea is given in the [NeuroDiff paper](https://arxiv.org/abs/2009.09943)) at the first possible neurons and how it can be improved by \n",
    "- introducing at fresh variables for at most a certain fraction of the neurons in a layer and\n",
    "- selecting the neurons for which to introduce fresh variables by the range between their concrete lower and upper bounds.\n",
    "\n",
    "The effect of the techniques is visible as the computed lower and upper bounds of the $5$ output neurons of the network get progressively tighter.\n",
    "\n",
    "Bounds computed by zonotope propagation are also shown for comparison."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "id": "087442c1-1c24-4721-90a3-cb4783a01dab",
   "metadata": {},
   "outputs": [],
   "source": [
    "max_vars = 0\n",
    "s = init_symbolic_interval_fvheur(acas_npi, input_set, max_vars=max_vars)\n",
    "ŝ₀ = forward_network(DPNFV(method=:DeepPolyRelax), acas_npi, s);"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "id": "1ee50458-668b-420a-95d5-5a81abb189c0",
   "metadata": {},
   "outputs": [],
   "source": [
    "max_vars = 20  # best possible value found with linear search\n",
    "s = init_symbolic_interval_fvheur(acas_npi, input_set, max_vars=max_vars)\n",
    "ŝ₁ = forward_network(DPNFV(method=:DeepPolyRelax), acas_npi, s);"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "id": "cc21f0b8-ff36-4780-812d-16eafa3bc8b5",
   "metadata": {},
   "outputs": [],
   "source": [
    "max_vars = 43  # best possible value found with linear search\n",
    "s = init_symbolic_interval_fvheur(acas_npi, input_set, max_vars=max_vars)\n",
    "ŝ = forward_network(DPNFV(method=:DeepPolyRelax, get_fresh_var_idxs=DPNeurifyFV.fresh_var_range_non_zero, var_frac=0.2), acas_npi, s);"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "id": "d397d96c-7533-4c1c-8285-dc60432f6dc7",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Zonotope propagation\n",
    "ẑ = forward_network(Ai2z(), acas, input_set);"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "id": "7021cffa-1aa4-4d5f-81cf-653628ae96bf",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "---- lower bounds ----\n",
      "no fresh vars: [-945.7437378443676, -1593.1292720792367, -1107.327504883211, -2657.431833411753, -1721.522667184016]\n",
      "earliest vars: [-713.5475439388757, -1206.8144662819318, -836.4005121250489, -2011.2980832629394, -1298.6134640550054]\n",
      "DPNeurifyFV:   [-545.8439243441478, -849.9244688863708, -620.4441380554525, -1369.794720592327, -968.0683908576995]\n",
      "Zonotopes:     [-3284.187439643944, -3858.877872030732, -3974.832966356989, -4135.3674257450475, -3829.9250811223164]\n",
      "---- upper bounds ----\n",
      "no fresh vars: [2627.2788360915074, 3430.996100304105, 3485.8259676663447, 3830.7907683913627, 3815.8806839777662]\n",
      "earliest vars: [1986.046102724299, 2595.4574974837446, 2635.617754849305, 2896.4768664566177, 2885.8584796706364]\n",
      "DPNeurifyFV:   [1327.6136788440915, 1711.7279892887761, 1682.6841791238921, 1985.863498730014, 1921.661177949215]\n",
      "Zonotopes:     [5023.28774060603, 5701.11965091425, 6211.210325766039, 5365.67801572021, 5514.254478245289]\n"
     ]
    }
   ],
   "source": [
    "println(\"---- lower bounds ----\")\n",
    "println(\"no fresh vars: \", ŝ₀.lbs[end])\n",
    "println(\"earliest vars: \", ŝ₁.lbs[end])\n",
    "println(\"DPNeurifyFV:   \", ŝ.lbs[end])\n",
    "println(\"Zonotopes:     \", low(ẑ))\n",
    "\n",
    "println(\"---- upper bounds ----\")\n",
    "println(\"no fresh vars: \", ŝ₀.ubs[end])\n",
    "println(\"earliest vars: \", ŝ₁.ubs[end])\n",
    "println(\"DPNeurifyFV:   \", ŝ.ubs[end])\n",
    "println(\"Zonotopes:     \", high(ẑ))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7eb35c94-9704-430a-8cc1-b1dbd775aa7b",
   "metadata": {},
   "source": [
    "# Branch and Bound with Input Splitting\n",
    "\n",
    "We are now going to maximize the first output of the network over the input space given by property $\\phi_1$. (We terminate as soon as an optimality gap of $10^{-4}$ is reached)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "id": "6203201b-26d1-4373-a2c2-7831e159aa77",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "i: 100 - [-0.017807535560300215, 0.28346228356969677], 0.1857128143310547 sec\n",
      "i: 200 - [-0.017807535560300215, -0.0005626577176235797], 0.3333280086517334 sec\n",
      "i: 300 - [-0.017807535560300215, -0.014229881669890589], 0.47218894958496094 sec\n",
      "i: 400 - [-0.017807535560300215, -0.01616575874515486], 0.6078557968139648 sec\n",
      "i: 500 - [-0.017768583207969105, -0.01700112607245889], 0.7410039901733398 sec\n",
      "i: 600 - [-0.01771721730558143, -0.017293899238105828], 0.8720948696136475 sec\n",
      "i: 700 - [-0.01768762570130527, -0.017444203723618303], 0.998323917388916 sec\n",
      "i: 800 - [-0.01768762570130527, -0.017532476976106312], 1.119107961654663 sec\n",
      "i: 900 - [-0.01768762570130527, -0.01757186146113745], 1.237293004989624 sec\n",
      "i: 1000 - [-0.01768762570130527, -0.017591160922579428], 1.3489699363708496 sec\n",
      "i: 1059 - [-0.01768762570130527, -0.017602731762479756], 1.42289400100708 sec\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "([0.5999999999999999, 0.0009765625, 0.34375, 0.5, -0.45], -0.01768762570130527, -0.017602731762479756, 1059)"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "params = DPNeurifyFV.PriorityOptimizerParameters(max_steps=5000, print_frequency=100, stop_frequency=1, verbosity=2)\n",
    "optimize_linear_deep_poly(acas, input_set, [1.,0,0,0,0], params, solver=DPNFV(method=:DeepPolyRelax, max_vars=15), concrete_sample=:BoundsMaximizer, split=DPNeurifyFV.split_important_interval)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f8088907-4673-4ab9-b229-833594163528",
   "metadata": {},
   "source": [
    "To verify, if the output of a neural network is contained within a certain polytope, we maximize the maximum violation of its constraints over the input region of interest.\n",
    "\n",
    "For property $\\phi_1$, we want to prove that the first output $o_1$ of the network is at most $b = 3.9911...$. The violation of this constraint is then $o_1 - b$. If we find an upper bound on this violation that is always below zero, then the property is satisfied."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "id": "00fedd71-d197-47b4-9282-bf3a349f22f9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "i: 10 - [-4.010900538960003, 161.65152125857605], 0.01834392547607422 sec\n",
      "i: 20 - [-4.009413609141843, 35.005185303363035], 0.05038785934448242 sec\n",
      "i: 30 - [-4.00917068264572, 12.449902203700105], 0.06676292419433594 sec\n",
      "i: 40 - [-4.00917068264572, 4.5827470329762505], 0.08274698257446289 sec\n",
      "Returning early because of upper bound threshold\n",
      "lower_bound = -4.00917068264572\n",
      "upper_bound = -0.15106125856841235\n",
      "steps = 44\n"
     ]
    }
   ],
   "source": [
    "input_set, output_set = DPNeurifyFV.get_acas_sets(1)\n",
    "\n",
    "params = DPNeurifyFV.PriorityOptimizerParameters(max_steps=5000, print_frequency=10, stop_frequency=1, verbosity=2)\n",
    "x_star, lower_bound, upper_bound, steps = contained_within_polytope_deep_poly(acas, input_set, output_set, params, solver=DPNFV(method=:DeepPolyRelax, max_vars=20), \n",
    "                                                                              split=DPNeurifyFV.split_important_interval, concrete_sample=:BoundsMaximizer)\n",
    "\n",
    "@show lower_bound\n",
    "@show upper_bound\n",
    "@show steps;"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7947d5cc-5325-4896-95e4-2940160db056",
   "metadata": {},
   "source": [
    "To verify, that the output of a neural network never reaches a certain polytope, we minimize the minimum violation of its constraints over the input region of interest.\n",
    "\n",
    "For property $\\phi_2$, we want to prove that the first output $o_1$ is never larger than the other outputs of the network.\n",
    "This can be captured by the linear constraints $o_1 \\leq o_i$ for $i = 2,...,5$ with their respective violation $o_1 - o_2$.\n",
    "\n",
    "If we find a lower bound that is larger than zero on the minimum of the constraint violations, we can guarantee that the polytope is never reached."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "id": "3c3e1dc4-216e-4765-82b3-449491a2acc1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "i: 50 - [-0.002872276893186433, 1.211565045737391], 0.10503101348876953 sec\n",
      "i: 100 - [-0.0025448432264916516, 0.1619738574082134], 0.19298195838928223 sec\n",
      "i: 150 - [-0.0025448432264916516, 0.0366643163048731], 0.26526808738708496 sec\n",
      "i: 200 - [-0.0025448432264916516, 0.008490718747280575], 0.3477649688720703 sec\n",
      "i: 250 - [-0.0025448432264916516, 0.0012385253647943031], 0.4178740978240967 sec\n",
      "i: 300 - [-0.0025448432264916516, 9.35084304466878e-6], 0.4970970153808594 sec\n",
      "Returning early because of upper bound threshold\n",
      "lower_bound = 2.7476926375185132e-5\n",
      "upper_bound = 0.0025448432264916516\n",
      "steps = 301\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "301"
      ]
     },
     "execution_count": 75,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "input_set, output_set = DPNeurifyFV.get_acas_sets(2)\n",
    "\n",
    "params = DPNeurifyFV.PriorityOptimizerParameters(max_steps=5000, print_frequency=50, stop_frequency=1, verbosity=2)\n",
    "x_star, lower_bound, upper_bound, steps = reaches_polytope_deep_poly(acas, input_set, output_set.X, params, solver=DPNFV(method=:DeepPolyRelax, max_vars=20), \n",
    "                                                                      split=DPNeurifyFV.split_important_interval, concrete_sample=:BoundsMaximizer)\n",
    "\n",
    "@show lower_bound\n",
    "@show upper_bound\n",
    "@show steps"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "7fafdd3f-e0d9-4973-9c3e-9d1908bf481b",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Julia 1.6.3",
   "language": "julia",
   "name": "julia-1.6"
  },
  "language_info": {
   "file_extension": ".jl",
   "mimetype": "application/julia",
   "name": "julia",
   "version": "1.6.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}