Sparse polynomial optimisation for neural network verification
From MaRDI portal
Abstract: The prevalence of neural networks in society is expanding at an increasing rate. It is becoming clear that providing robust guarantees on systems that use neural networks is very important, especially in safety-critical applications. A trained neural network's sensitivity to adversarial attacks is one of its greatest shortcomings. To provide robust guarantees, one popular method that has seen success is to bound the activation functions using equality and inequality constraints. However, there are numerous ways to form these bounds, providing a trade-off between conservativeness and complexity. Depending on the complexity of these bounds, the computational time of the optimisation problem varies, with longer solve times often leading to tighter bounds. We approach the problem from a different perspective, using sparse polynomial optimisation theory and the Positivstellensatz, which derives from the field of real algebraic geometry. The former exploits the natural cascading structure of the neural network using ideas from chordal sparsity while the later asserts the emptiness of a semi-algebraic set with a nested family of tests of non-decreasing accuracy to provide tight bounds. We show that bounds can be tightened significantly, whilst the computational time remains reasonable. We compare the solve times of different solvers and show how the accuracy can be improved at the expense of increased computation time. We show that by using this sparse polynomial framework the solve time and accuracy can be improved over other methods for neural network verification with ReLU, sigmoid and tanh activation functions.
Recommendations
- Chordal sparsity for SDP-based neural network verification
- Advances in verification of ReLU neural networks
- Improved geometric path enumeration for verifying ReLU neural networks
- Branch and bound for piecewise linear neural network verification
- Global optimization of objective functions represented by ReLU networks
Cites work
- A direct proof for the matrix decomposition of chordal-structured positive semidefinite matrices
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- Chordal-TSSOS: a moment-SOS hierarchy that exploits term sparsity with chordal extension
- Ensemble machine learning. Methods and applications
- Formal verification of piece-wise linear feed-forward neural networks
- Positive semidefinite matrices with a given sparsity pattern
- Reinforcement learning. An introduction
- Reluplex: an efficient SMT solver for verifying deep neural networks
- Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
- Safety verification of deep neural networks
Cited in
(7)- Chordal sparsity for SDP-based neural network verification
- A Correlatively Sparse Lagrange Multiplier Expression Relaxation for Polynomial Optimization
- Efficient neural network analysis with sum-of-infeasibilities
- LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions
- A characterization for tightness of the sparse moment-SOS hierarchy
- Robust stability of neural network control systems with interval matrix uncertainties
- Sparse polynomial optimization with unbounded sets
This page was built for publication: Sparse polynomial optimisation for neural network verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6073032)
