DLS
Sun 15 - Fri 20 November 2020 Online Conference
co-located with SPLASH 2020
Thu 19 Nov 2020 05:40 - 06:00 at SPLASH-III - 5 Chair(s): Xavier Rival, Sukyoung Ryu
Wed 18 Nov 2020 17:40 - 18:00 at SPLASH-III - 5 Chair(s): Patrick Cousot, Sukyoung Ryu

We are interested in algorithmically proving the robustness of neural networks. Notions of robustness have been discussed in the literature; we are interested in probabilistic notions of robustness that assume it feasible to construct a statistical model of the process generating the inputs of a neural network. We find this a reasonable assumption given the rapid advances in algorithms for learning generative models of data. A neural network f is then defined to be probabilistically robust if, for a randomly generated pair of inputs, f is likely to demonstrate k-Lipschitzness, i.e., the distance between the outputs computed by $f$ is upper-bounded by the k-th multiple of the distance between the pair of inputs. We name this property, probabilistic Lipschitzness.

We model generative models and neural networks, together, as programs in a simple, first-order, imperative, probabilistic programming language, pcat. Inspired by a large body of existing literature, we define a denotational semantics for this language. Then we develop a sound local Lipschitzness analysis for cat, a non-probabilistic sublanguage of pcat. This analysis can compute an upper bound of the ``Lipschitzness'' of a neural network in a bounded region of the input set. We next present a provably correct algorithm, PROLIP, that analyzes the behavior of a neural network in a user-specified box-shaped input region and computes - (i) lower bounds on the probabilistic mass of such a region with respect to the generative model, (ii) upper bounds on the Lipschitz constant of the neural network in this region, with the help of the local Lipschitzness analysis. Finally, we present a sketch of a proof-search algorithm that uses PROLIP as a primitive for finding proofs of probabilistic Lipschitzness. We implement the PROLIP algorithm and empirically evaluate the computational complexity of PROLIP.

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

17:00 - 18:20: 5SAS / DLS 2020 at SPLASH-III +12h
Chair(s): Patrick CousotNew York University, Sukyoung Ryu
17:00 - 17:20
Research paper
SAS
Matthew SotoudehUniversity of California, Davis, Aditya V. ThakurUniversity of California, Davis
Pre-print Media Attached
17:20 - 17:40
Talk
DLS 2020
Yusuke IzawaTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology
Link to publication DOI Pre-print Media Attached
17:40 - 18:00
Research paper
SAS
Ravi MangalGeorgia Institute of Technology, Kartik SarangmathGeorgia Institute of Technology, Aditya Nori, Alessandro OrsoGeorgia Tech
Pre-print Media Attached
18:00 - 18:20
Talk
DLS 2020
Dejice JacobUniversity of Glasgow, UK, Phil TrinderUniversity of Glasgow, Jeremy SingerGlasgow University
Link to publication DOI Pre-print Media Attached

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

05:00 - 06:20: 5SAS / DLS 2020 at SPLASH-III
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris, Sukyoung Ryu
05:00 - 05:20
Research paper
SAS
Matthew SotoudehUniversity of California, Davis, Aditya V. ThakurUniversity of California, Davis
Pre-print Media Attached
05:20 - 05:40
Talk
DLS 2020
Yusuke IzawaTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology
Link to publication DOI Pre-print Media Attached
05:40 - 06:00
Research paper
SAS
Ravi MangalGeorgia Institute of Technology, Kartik SarangmathGeorgia Institute of Technology, Aditya Nori, Alessandro OrsoGeorgia Tech
Pre-print Media Attached
06:00 - 06:20
Talk
DLS 2020
Dejice JacobUniversity of Glasgow, UK, Phil TrinderUniversity of Glasgow, Jeremy SingerGlasgow University
Link to publication DOI Pre-print Media Attached