updates

ibook/notebooks/logic.ipynb → ibook/notebooks/vnn.ipynb

@@ -1,13 +1,67 @@
 {
  "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Background\n",
+    "\n",
+    "## Deep Neural Networks\n",
+    "\n",
+    "\n",
+    "## An Example\n",
+    "\n",
+    "<img src=\"files/dnn1.png\" alt=\"drawing\" width=\"800\"/>\n",
+    "Fig. 1: A simple DNN with 2 inputs, 2 hidden layers, and 2 outputs.\n",
+    "\n",
+    "<!-- ![DNN example with 2 inputs, 2 hidden layers, and 2 outputs.](files/dnn1.png) -->\n",
+    "\n",
+    "Fig. 1 shows a simple DNN that we will use to demonstrate various techniques throughout this paper.\n",
+    "This DNN is composed of an input layer with two inputs $i_0, i_1$, an output layer with two outputs $o_0, o_1$, and two hidden layers with two nodes for each layer. The weights are shown for each edge and in this example we do not use bias (i.e., they are set to 0). This DNN model is fully connected (no weights having value 0) and uses the ReLU activation function. \n",
+    "\n",
+    "For this DNN, the outputs of the neurons in the hidden layers (prefixed\n",
+    "with `n`) are applied with the `relu` activation function, but the\n",
+    "outputs of the DNN (prefixed with `o`) are not. These settings are\n",
+    "controlled by the `True`, `False` parameters as shown in the code below. Also, this\n",
+    "example does not use `bias`, i.e., bias values are all 0.0's as shown below.\n",
+    "Note that all of these settings are parameterized and I deliberately use\n",
+    "this example to show these how these parameters are used (e.g., `relu`\n",
+    "only applies to hidden neurons, but not outputs).\n",
+    "\n",
+    "It can be seen that this DNN has the follow properties:\n",
+    "- $P_2 = (i0 - i1 > 0 \\land i0 + i1 \\le 0) \\Rightarrow o0 > o1$\n",
+    "- $P_1 = (n0_0 > 0.0 \\land n0_1 \\le 0.0) \\Rightarrow  o0 > o1$\n",
+    "\n",
+    "but /does not/ have the following properties:\n",
+    "- $P_3 = i0 - i1 >0 \\Rightarrow o0 > o1$ because on input $i0=4; i_1=\\frac{7}{2}$, the DNN evaluates to $o0=\\frac{-1}{2}; o1 = \\frac{1}{2}$ (i.e., a counterexample invalidating the property).\n",
+    "\n",
+    "## DNN Verification Problem\n",
+    "Let $N$ be a DNN with ReLU's and let $\\alpha$ be a property on the inputs $x$'s and $\\beta$ a property on the outputs $y$'s of $N$. \n",
+    "The DNN verification problem asks if $\\alpha(x) \\implies \\beta(y)$ is a property of $N$. That is, every assignment $\\sigma$ for $x$ that satisfies $\\alpha$, the result of propagating $\\sigma$ through $N$ is an output that satisfies $\\beta$.  In other words, every input satisfying the precondition $\\alpha$ produces in an input satisfying the postcondition $\\beta$.\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Complexity of DNN Verification"
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "08548c5c-2a03-4bb2-b58c-70f6b139583b",
    "metadata": {},
    "source": [
     "# Propositional Logic\n",
     "\n",
-    "Gengle introduction to terminologies in *Propositional Logic*.  Code is demonstrated using the *Z3* SMT solver."
+    "Gentle introduction to terminologies in *Propositional Logic*.  Code is demonstrated using the *Z3* SMT solver."
    ]
   },
   {
@@ -27,7 +81,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 8,
    "id": "5c8069b1-daa3-433b-b4ff-12cc79a11172",
    "metadata": {},
    "outputs": [
@@ -40,7 +94,7 @@
        "Or(And(A, Not(B), Not(C)), And(C, Not(A)))"
       ]
      },
-     "execution_count": 1,
+     "execution_count": 8,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -95,7 +149,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 9,
    "id": "b65537df-ac8b-4735-b986-f631e6913a19",
    "metadata": {},
    "outputs": [],
@@ -143,7 +197,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 10,
    "id": "1e9576d0-65d6-42e1-ba7c-57181ca4de9e",
    "metadata": {},
    "outputs": [],
@@ -236,7 +290,7 @@
     }
    ],
    "source": [
-    "from z3 import Ints\n",
+    "from z3 import Ints, And, Implies\n",
     "import z3\n",
     "x, y = Ints(\"x y\")\n",
     "\n",
@@ -260,7 +314,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 12,
    "id": "dd65d96b-0e21-45b3-a61a-273718d68655",
    "metadata": {},
    "outputs": [],
@@ -327,7 +381,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.9.13"
+   "version": "3.9.18"
   },
   "name": "logic.ipynb",
   "vscode": {

index.html

@@ -210,6 +210,7 @@ <h3 id="press">Press Release</h3>
         <li><a href="https://www.gmu.edu/news/2023-02/boom-crash-mason-researcher-receives-half-million-nsf-grant-could-steer-ai-safely">Boom crash: Mason researcher receives half million NSF grant that could steer AI safely</a>: GMU press release on CAREER award</li>
         <li><a href="https://thanhnien.vn/tien-si-goc-viet-duoc-tai-tro-nghien-cuu-ai-185230304234603638.htm">Tiến sĩ gốc Việt được tài trợ nghiên cứu AI</a>: from Thanh Nien, a Vietnamese news outlet</li>
         <li><a href="https://computing.unl.edu/nguyen-earns-nsf-crii-award/">CRII Award</a>: UNL press release on NSF CRII award</li>
+        <li><a href="https://newsroom.unl.edu/announce/cse/9518/56343">UNL press release</a> on ACM SIGSOFT 10-year Most Influential Paper Award at ICSE</li>
       </ol>      
     </div>