Formal Security Analysis of Neural Networks using Symbolic Intervals
summary
ReluVal uses interval arithmetic and symbolic intervals to compute rigorous output bounds for ReLU networks, then applies iterated interval refinement (bisecting inputs) to eliminate overestimation; the system is highly parallelizable and keeps linear bounds until ReLU concretization. Claims: 200x faster than Reluplex on average and on an 8-core machine verifies a property in 4 hours that Reluplex times out after 5+ days. It finds 35% more counterexamples than gradient attacks but suffers more false positives and occasional timeouts as perturbation ranges grow.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:40Background of Machine Learning Systems
- 3:47Why Provide the Formal Analysis on the Output of the Neural Network Is Very Difficult
- 8:14Dependency Error
- 10:38Iterated Interval Refinement
related talks
28mReduced Products of Abstract Domains for Fairness Certification of Neural Networks
15mReduced Products of Abstract Domains for Fairness Certification of Neural Networks
28mStatic analysis of ReLU neural networks with tropical polyhedra
15mPerfectly Parallel Fairness Certification of Neural Networks
14mStatic analysis of ReLU neural networks with tropical polyhedra
01h 03mUnderstanding ReLU Networks Through Graph Problems and Polyhedra
19mInterval Universal Approximation for Neural Networks
42mReLUs: An Alternative to the ReLU Activation Function