1_30_2020_ReluplexBaselineIssue.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "using NeuralVerification\n",
    "using Plots"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Network(NeuralVerification.Layer[NeuralVerification.Layer{NeuralVerification.ReLU,Float64}([4.085846895799728; 4.1588173348358115], [0.8817063994604648, 0.2796385232288592], NeuralVerification.ReLU()), NeuralVerification.Layer{NeuralVerification.ReLU,Float64}([-4.334249191310455 -1.8483717148645762], [0.06296092967586442], NeuralVerification.ReLU())])"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Create your network and visualize its output\n",
    "l1 = NeuralVerification.Layer(reshape([4.085846895799728; 4.1588173348358115], (2, 1)), [0.8817063994604648, 0.2796385232288592], NeuralVerification.ReLU())\n",
    "l2 = NeuralVerification.Layer([-4.334249191310455 -1.8483717148645762], [0.06296092967586442], NeuralVerification.ReLU())\n",
    "nnet = NeuralVerification.Network([l1, l2])\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n",
       "<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" width=\"600\" height=\"400\" viewBox=\"0 0 2400 1600\">\n",
       "<defs>\n",
       "  <clipPath id=\"clip4100\">\n",
       "    <rect x=\"0\" y=\"0\" width=\"2400\" height=\"1600\"/>\n",
       "  </clipPath>\n",
       "</defs>\n",
       "<path clip-path=\"url(#clip4100)\" d=\"\n",
       "M0 1600 L2400 1600 L2400 0 L0 0  Z\n",
       "  \" fill=\"#ffffff\" fill-rule=\"evenodd\" fill-opacity=\"1\"/>\n",
       "<defs>\n",
       "  <clipPath id=\"clip4101\">\n",
       "    <rect x=\"480\" y=\"0\" width=\"1681\" height=\"1600\"/>\n",
       "  </clipPath>\n",
       "</defs>\n",
       "<path clip-path=\"url(#clip4100)\" d=\"\n",
       "M180.66 1487.47 L2352.76 1487.47 L2352.76 47.2441 L180.66 47.2441  Z\n",
       "  \" fill=\"#ffffff\" fill-rule=\"evenodd\" fill-opacity=\"1\"/>\n",
       "<defs>\n",
       "  <clipPath id=\"clip4102\">\n",
       "    <rect x=\"180\" y=\"47\" width=\"2173\" height=\"1441\"/>\n",
       "  </clipPath>\n",
       "</defs>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  242.135,1487.47 242.135,47.2441 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  754.421,1487.47 754.421,47.2441 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  1266.71,1487.47 1266.71,47.2441 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  1778.99,1487.47 1778.99,47.2441 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  2291.28,1487.47 2291.28,47.2441 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,1446.71 2352.76,1446.71 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,1230.91 2352.76,1230.91 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,1015.11 2352.76,1015.11 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,799.308 2352.76,799.308 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,583.506 2352.76,583.506 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,367.705 2352.76,367.705 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#000000; stroke-width:1.6; stroke-opacity:0.1; fill:none\" points=\"\n",
       "  180.66,151.903 2352.76,151.903 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,1487.47 2352.76,1487.47 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,1487.47 180.66,47.2441 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  242.135,1487.47 242.135,1465.87 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  754.421,1487.47 754.421,1465.87 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  1266.71,1487.47 1266.71,1465.87 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  1778.99,1487.47 1778.99,1465.87 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  2291.28,1487.47 2291.28,1465.87 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,1446.71 213.242,1446.71 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,1230.91 213.242,1230.91 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,1015.11 213.242,1015.11 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,799.308 213.242,799.308 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,583.506 213.242,583.506 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,367.705 213.242,367.705 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  180.66,151.903 213.242,151.903 \n",
       "  \"/>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:middle;\" transform=\"rotate(0, 242.135, 1541.47)\" x=\"242.135\" y=\"1541.47\">-1.0</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:middle;\" transform=\"rotate(0, 754.421, 1541.47)\" x=\"754.421\" y=\"1541.47\">-0.5</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:middle;\" transform=\"rotate(0, 1266.71, 1541.47)\" x=\"1266.71\" y=\"1541.47\">0.0</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:middle;\" transform=\"rotate(0, 1778.99, 1541.47)\" x=\"1778.99\" y=\"1541.47\">0.5</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:middle;\" transform=\"rotate(0, 2291.28, 1541.47)\" x=\"2291.28\" y=\"1541.47\">1.0</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 1464.21)\" x=\"156.66\" y=\"1464.21\">0.00</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 1248.41)\" x=\"156.66\" y=\"1248.41\">0.01</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 1032.61)\" x=\"156.66\" y=\"1032.61\">0.02</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 816.808)\" x=\"156.66\" y=\"816.808\">0.03</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 601.006)\" x=\"156.66\" y=\"601.006\">0.04</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 385.205)\" x=\"156.66\" y=\"385.205\">0.05</text>\n",
       "</g>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:end;\" transform=\"rotate(0, 156.66, 169.403)\" x=\"156.66\" y=\"169.403\">0.06</text>\n",
       "</g>\n",
       "<polyline clip-path=\"url(#clip4102)\" style=\"stroke:#009af9; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  242.135,88.0053 252.38,88.0053 262.626,88.0053 272.872,88.0053 283.118,88.0053 293.363,88.0053 303.609,88.0053 313.855,88.0053 324.101,88.0053 334.346,88.0053 \n",
       "  344.592,88.0053 354.838,88.0053 365.084,88.0053 375.329,88.0053 385.575,88.0053 395.821,88.0053 406.066,88.0053 416.312,88.0053 426.558,88.0053 436.804,88.0053 \n",
       "  447.049,88.0053 457.295,88.0053 467.541,88.0053 477.787,88.0053 488.032,88.0053 498.278,88.0053 508.524,88.0053 518.77,88.0053 529.015,88.0053 539.261,88.0053 \n",
       "  549.507,88.0053 559.752,88.0053 569.998,88.0053 580.244,88.0053 590.49,88.0053 600.735,88.0053 610.981,88.0053 621.227,88.0053 631.473,88.0053 641.718,88.0053 \n",
       "  651.964,88.0053 662.21,88.0053 672.456,88.0053 682.701,88.0053 692.947,88.0053 703.193,88.0053 713.438,88.0053 723.684,88.0053 733.93,88.0053 744.176,88.0053 \n",
       "  754.421,88.0053 764.667,88.0053 774.913,88.0053 785.159,88.0053 795.404,88.0053 805.65,88.0053 815.896,88.0053 826.142,88.0053 836.387,88.0053 846.633,88.0053 \n",
       "  856.879,88.0053 867.124,88.0053 877.37,88.0053 887.616,88.0053 897.862,88.0053 908.107,88.0053 918.353,88.0053 928.599,88.0053 938.845,88.0053 949.09,88.0053 \n",
       "  959.336,88.0053 969.582,88.0053 979.828,88.0053 990.073,88.0053 1000.32,88.0053 1010.56,88.0053 1020.81,88.0053 1031.06,88.0053 1041.3,88.0053 1051.55,1446.71 \n",
       "  1061.79,1446.71 1072.04,1446.71 1082.28,1446.71 1092.53,1446.71 1102.78,1446.71 1113.02,1446.71 1123.27,1446.71 1133.51,1446.71 1143.76,1446.71 1154.01,1446.71 \n",
       "  1164.25,1446.71 1174.5,1446.71 1184.74,1446.71 1194.99,1446.71 1205.23,1446.71 1215.48,1446.71 1225.73,1446.71 1235.97,1446.71 1246.22,1446.71 1256.46,1446.71 \n",
       "  1266.71,1446.71 1276.95,1446.71 1287.2,1446.71 1297.45,1446.71 1307.69,1446.71 1317.94,1446.71 1328.18,1446.71 1338.43,1446.71 1348.67,1446.71 1358.92,1446.71 \n",
       "  1369.17,1446.71 1379.41,1446.71 1389.66,1446.71 1399.9,1446.71 1410.15,1446.71 1420.39,1446.71 1430.64,1446.71 1440.89,1446.71 1451.13,1446.71 1461.38,1446.71 \n",
       "  1471.62,1446.71 1481.87,1446.71 1492.11,1446.71 1502.36,1446.71 1512.61,1446.71 1522.85,1446.71 1533.1,1446.71 1543.34,1446.71 1553.59,1446.71 1563.83,1446.71 \n",
       "  1574.08,1446.71 1584.33,1446.71 1594.57,1446.71 1604.82,1446.71 1615.06,1446.71 1625.31,1446.71 1635.55,1446.71 1645.8,1446.71 1656.05,1446.71 1666.29,1446.71 \n",
       "  1676.54,1446.71 1686.78,1446.71 1697.03,1446.71 1707.27,1446.71 1717.52,1446.71 1727.77,1446.71 1738.01,1446.71 1748.26,1446.71 1758.5,1446.71 1768.75,1446.71 \n",
       "  1778.99,1446.71 1789.24,1446.71 1799.49,1446.71 1809.73,1446.71 1819.98,1446.71 1830.22,1446.71 1840.47,1446.71 1850.71,1446.71 1860.96,1446.71 1871.21,1446.71 \n",
       "  1881.45,1446.71 1891.7,1446.71 1901.94,1446.71 1912.19,1446.71 1922.44,1446.71 1932.68,1446.71 1942.93,1446.71 1953.17,1446.71 1963.42,1446.71 1973.66,1446.71 \n",
       "  1983.91,1446.71 1994.16,1446.71 2004.4,1446.71 2014.65,1446.71 2024.89,1446.71 2035.14,1446.71 2045.38,1446.71 2055.63,1446.71 2065.88,1446.71 2076.12,1446.71 \n",
       "  2086.37,1446.71 2096.61,1446.71 2106.86,1446.71 2117.1,1446.71 2127.35,1446.71 2137.6,1446.71 2147.84,1446.71 2158.09,1446.71 2168.33,1446.71 2178.58,1446.71 \n",
       "  2188.82,1446.71 2199.07,1446.71 2209.32,1446.71 2219.56,1446.71 2229.81,1446.71 2240.05,1446.71 2250.3,1446.71 2260.54,1446.71 2270.79,1446.71 2281.04,1446.71 \n",
       "  2291.28,1446.71 \n",
       "  \"/>\n",
       "<path clip-path=\"url(#clip4100)\" d=\"\n",
       "M1989.93 251.724 L2280.76 251.724 L2280.76 130.764 L1989.93 130.764  Z\n",
       "  \" fill=\"#ffffff\" fill-rule=\"evenodd\" fill-opacity=\"1\"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#000000; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  1989.93,251.724 2280.76,251.724 2280.76,130.764 1989.93,130.764 1989.93,251.724 \n",
       "  \"/>\n",
       "<polyline clip-path=\"url(#clip4100)\" style=\"stroke:#009af9; stroke-width:3.2; stroke-opacity:1; fill:none\" points=\"\n",
       "  2013.93,191.244 2157.93,191.244 \n",
       "  \"/>\n",
       "<g clip-path=\"url(#clip4100)\">\n",
       "<text style=\"fill:#000000; fill-opacity:1; font-family:Arial,Helvetica Neue,Helvetica,sans-serif; font-size:48px; text-anchor:start;\" transform=\"rotate(0, 2181.93, 208.744)\" x=\"2181.93\" y=\"208.744\">y1</text>\n",
       "</g>\n",
       "</svg>\n"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Simple plot of outputs between x=-1 and x=1\n",
    "outputs =[NeuralVerification.compute_output(nnet, [x])[1] for x=-1:0.01:1] \n",
    "plot(collect(-1:0.01:1), outputs)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1-element Array{Float64,1}:\n",
       " 0.0"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Example output above 0.05: -0.5 --> 0.063\n",
    "NeuralVerification.compute_output(nnet, [-0.06723991479176115])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CounterExampleResult(:holds, Float64[])"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Try using Reluplex to check if the output is constrained to the set below 0.05 when x is between -1 and 1\n",
    "solver = Reluplex()\n",
    "\n",
    "input_set = NeuralVerification.Hyperrectangle(low = [-1.0], high = [1.0])\n",
    "output_set = NeuralVerification.LinearConstraint([1.0], 0.05)\n",
    "problem = Problem(nnet, input_set, output_set)\n",
    "\n",
    "NeuralVerification.solve(solver, problem)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "CounterExampleResult(:violated, [-0.06723991479176115])"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# However, it still will find counterexamples that reach an output of 0 - say if I test if the output is always less than -0.1\n",
    "output_set = NeuralVerification.LinearConstraint([1.0], -0.1)\n",
    "problem = Problem(nnet, input_set, output_set)\n",
    "\n",
    "NeuralVerification.solve(solver, problem)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Julia 1.2.0",
   "language": "julia",
   "name": "julia-1.2"
  },
  "language_info": {
   "file_extension": ".jl",
   "mimetype": "application/julia",
   "name": "julia",
   "version": "1.2.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}