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.
An approach to reachability analysis for feed-forward ReLU neural networks
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
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.
representative citing papers
STBP computes exact closed-form bounds for the first convolutional layer of spatio-temporal networks and propagates scalable approximations through the rest to certify robustness under subset-frame or patch perturbations.
Introduces a fidelity-based robustness lower bound for QML models, computable from measurements or via SDP, packaged in the VeriQR tool with the first 20-qubit hardware benchmark.
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.
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.
citing papers explorer
-
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.
-
Hybrid Robustness Verification for Spatio-Temporal Neural Networks
STBP computes exact closed-form bounds for the first convolutional layer of spatio-temporal networks and propagates scalable approximations through the rest to certify robustness under subset-frame or patch perturbations.
-
Verifying Adversarial Robustness in Quantum Machine Learning: from theory to physical validation via a software tool
Introduces a fidelity-based robustness lower bound for QML models, computable from measurements or via SDP, packaged in the VeriQR tool with the first 20-qubit hardware benchmark.
-
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.