Global optimization of objective functions represented by ReLU networks
From MaRDI portal
Abstract: Neural networks can learn complex, non-convex functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. Verification algorithms address this need and provide formal guarantees about a neural network by answering "yes or no" questions. For example, they can answer whether a violation exists within certain bounds. However, individual "yes or no" questions cannot answer qualitative questions such as "what is the largest error within these bounds"; the answers to these lie in the domain of optimization. Therefore, we propose strategies to extend existing verifiers to perform optimization and find: (i) the most extreme failure in a given input region and (ii) the minimum input perturbation required to cause a failure. A naive approach using a bisection search with an off-the-shelf verifier results in many expensive and overlapping calls to the verifier. Instead, we propose an approach that tightly integrates the optimization process into the verification procedure, achieving better runtime performance than the naive approach. We evaluate our approach implemented as an extension of Marabou, a state-of-the-art neural network verifier, and compare its performance with the bisection approach and MIPVerify, an optimization-based verifier. We observe complementary performance between our extension of Marabou and MIPVerify.
Recommendations
- Advances in verification of ReLU neural networks
- Improved geometric path enumeration for verifying ReLU neural networks
- Reluplex: a calculus for reasoning about deep neural networks
- Reluplex: an efficient SMT solver for verifying deep neural networks
- Branch and bound for piecewise linear neural network verification
Cites work
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Algorithm 778: L-BFGS-B
- Branch and bound for piecewise linear neural network verification
- Deep neural networks and mixed integer linear optimization
- scientific article; zbMATH DE number 1312984 (Why is no real title available?)
- scientific article; zbMATH DE number 7030501 (Why is no real title available?)
- Neural networks for control systems - a survey
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
- Reluplex: an efficient SMT solver for verifying deep neural networks
- Safety verification of deep neural networks
- Verification of deep convolutional neural networks using ImageStars
Cited in
(3)
This page was built for publication: Global optimization of objective functions represented by ReLU networks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6053800)
