Reachability Analysis for Neural Networks
Prior reading: What Are Formal Methods? | Linear Algebra Proofs of Optimality The Core Question Given a neural network $f$ and an input region $\mathcal{X}$, what is the set of all possible outputs $f(\mathcal{X})$? If we can bound this set, we can prove properties like "no input in this region produces a harmful output." Why This Is Hard Neural networks are piecewise-linear (ReLU) or worse (sigmoid, softmax). The number of linear regions grows exponentially with depth. Exact reachability is NP-hard. ...