Output Range Analysis for Deep Feedforward Neural Networks

By Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari. 2018

298 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Safety, Robustness & Interpretability

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Alexey Ignatiev
2. Huan Zhang
3. Cho-Jui Hsieh
4. Suman Sekhar Jana
5. Joao Marques-Silva
6. Nina Narodytska
7. Shiqi Wang
8. Hadi Salman

In Computational Theory and Mathematics

1. Nina Narodytska
2. Joao Marques-Silva
3. Alexey Ignatiev
4. Zico Kolter
5. George Pappas
6. Christian Tjandraatmadja
7. Manfred Morari
8. Craig Boutilier

In Safety, Robustness & Interpretability

1. Huan Zhang
2. Suman Sekhar Jana
3. Cho-Jui Hsieh
4. Shiqi Wang
5. A. Dimakis
6. Matt Jordan
7. Alexey Ignatiev
8. Kexin Pei

Citations in the corpus

• Formal Security Analysis of Neural Networks using Symbolic Intervals (2018, background): “Recently, Mixed Integer Linear programming (MILP) solvers combined with gradient descent have also been proposed for verification of DNNs [9, 10].”
• Strong mixed-integer programming formulations for trained neural networks (2018, unknown): “In recent years a number of authors have used MIP formulations to model trained neural networks [19,22,24,29,40,47,54,64,66,67,70,80,81], mostly applying big-M formulation techniques to ReLU-based networks.”
• Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes (2019, methodology): “Binary networks were trained to distinguish a subset of 1’s and 7’s from the full MNIST dataset.”
• Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017, methodology): “We used two procedures (in increasing order of speed) to determine bounds: LINEAR PROGRAMMING (LP), and INTERVAL ARITHMETIC (IA), also used in [10, 12, 28].”
• Abduction-Based Explanations for Machine Learning Models (2018, background): “More-over and as the experimental results suggest, the approach still applies (with no conceptual modification) if one opts to use oracles other than an ILP solver (Katz et al. 2017; Ruan, Huang, and Kwiatkowska 2018; Gehr et al. 2018; Dutta et al. 2018).”
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, methodology): “…exact verifiers solve the robustness verification problem (1) by typically employing MILP solvers (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2018; Fischetti & Jo, 2017; Tjeng et al., 2019; Xiao et al., 2019) or Satisfiability Modulo Theories (SMT) solvers (Scheibler et al.,…”
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification (2021, background): “Related Work Early complete verifiers relied on existing solvers (Katz et al., 2017; Ehlers, 2017; Huang et al., 2017; Dutta et al., 2018; Tjeng et al., 2019) and were limited to very small problem instances.”
• CAQL: Continuous Action Q-Learning (2019, methodology): “Versions of this MIP model have been used in neural network verification (Cheng et al., 2017; Lomuscio & Maganti, 2017; Bunel et al., 2018; Dutta et al., 2018; Fischetti & Jo, 2018; Anderson et al., 2019; Tjeng et al., 2019) and analysis (Serra et al.”
• MixTrain: Scalable Training of Formally Robust Neural Networks (2018, background): “MILP solver achieves better performance [60], [61], [62], but they still suffer from high nonlinearity of resulting formulas.”
• Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks (2019, background): “This can be done either locally around a specific input [7, 35, 15, 33, 12, 29, 30, 13, 40, 21, 41, 42], or globally by bounding the sensitivity of the function to input perturbations, i.”