An approach to reachability analysis for feed-forward ReLU neural networks
read the original abstract
We study the reachability problem for systems implemented as feed-forward neural networks whose activation function is implemented via ReLU functions. We draw a correspondence between establishing whether some arbitrary output can ever be outputed by a neural system and linear problems characterising a neural system of interest. We present a methodology to solve cases of practical interest by means of a state-of-the-art linear programs solver. We evaluate the technique presented by discussing the experimental results obtained by analysing reachability properties for a number of benchmarks in the literature.
This paper has not been read by Pith yet.
Forward citations
Cited by 3 Pith papers
-
Relaxation-Informed Training of Neural Network Surrogate Models
Regularizers that penalize big-M constants, unstable neurons, and per-sample LP relaxation gaps during neural network training reduce MILP solve times by up to four orders of magnitude while preserving surrogate accuracy.
-
Faster Verified Explanations for Neural Networks
FaVeX accelerates verified explanations for neural networks via dynamic batch-sequential processing and query reuse while introducing verifier-optimal robust explanations that incorporate verifier incompleteness.
-
A Performance Analyzer for a Public Cloud's ML-Augmented VM Allocator
SANJESH applies bi-level optimization to production traces and reveals VM allocation scenarios that cause 4x worse performance than the operator's existing evaluator detected.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.