Output Reachable Set Estimation and Verification for Multilayer Neural Networks

By Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson. 2017

306 citations recorded by the source corpus.

In this brief, the output reachable estimation and safety verification problems for multilayer perceptron (MLP) neural networks are addressed. First, a conception called maximum sensitivity is introduced, and for a class of MLPs whose activation functions are monotonic functions, the maximum sensitivity can be computed via solving convex optimization problems. Then, using a simulation-based method, the output reachable set estimation problem for neural networks is formulated into a chain of optimization problems. Finally, an automated safety verification is developed based on the output reachable set estimation result. An application to the safety verification for a robotic arm model with two joints is presented to show the effectiveness of the proposed approaches.

Subfields: Artificial Intelligence, Control and Systems Engineering

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

In Control and Systems Engineering

Citations in the corpus

Reachability Analysis of Deep Neural Networks with Provable Guarantees (2018, methodology): “Existing approaches for analysing DNNs with a guarantee work by either reducing the problem to a constraint satisfaction problem that can be solved by MILP [9, 11, 12, 13], SAT [14] or SMT [7, 12] techniques, or applying search algorithms over discretised vector spaces [6, 15].”
A Unified View of Piecewise Linear Neural Network Verification (2017, background): “Since they do not provide formal guarantees, we also don’t include approximate approaches relying on a limited set of perturbation [10] or on over-approximation methods that potentially lead to undecidable properties [16, 19].”
Algorithms for Verifying Deep Neural Networks (2019, methodology): “Representative methods are ExactReach [6], MaxSens [7], NNV [8], SymBox [9], Ai2 [10], and ERAN [11]–[14].”
A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability (2018, methodology): “We follow the naming convention from [Xiang et al., 2018,Ruan et al., 2018a,Ruan et al., 2018b].”
A Safety Framework for Critical Systems Utilising Deep Neural Networks (2020, methodology): “Formal verification [24,27,66,21,37,64,48,65,49,30] and coverage-guided testing [61,44,59,38,60,62] currently form the two major classes of V&V techniques for DL, from which a collection of evidence may be obtained that supports the partial prior knowledge.”
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019, methodology): “taken initial steps in this direction, by developing algorithms and tools for neural network verification [5,9,10,12,18,20,23,24].”
Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017, background): “Incomplete verifiers for evaluating network robustness employ a range of techniques, including duality [13, 32], layer-by-layer approximations of the adversarial polytope [41], discretizing the search space [23], abstract interpretation [16], bounding the local Lipschitz constant [40], or bounding t”
A Statistical Approach to Assessing Neural Network Robustness (2018, background): “Other work has sought approximate solutions in the same general framework but still does not scale to larger networks (Pulina & Tacchella, 2010; Xiang et al., 2018; Huang et al., 2017b).”