ARENA: Enhancing Abstract Refinement for Neural Network Verification
summary
ARENA implements an abstract-refinement verifier that uses the double description method over convex polytopes to turn disjunctions into LP-friendly conjunctions, and a new activation relaxation plus iterative refinement to tighten bounds. It eliminates multiple adversarial labels at once using a batch elimination (Delta=1..5) strategy, finds concrete counterexamples for falsification, and runs as a CPU prototype that scales to ~50k neurons. Evaluation shows ~15.8% more conclusive results than DeepSRGR and ~60.6% more than PRIMA, while lagging behind alpha-beta-crown (GPU) on throughput.
AI-written summary · about
chapters (15)
- 0:00Start
- 0:27Application of Neural Networks
- 6:00Outline
- 6:19Illustrative Example
- 7:17Verify Robustness
- 9:41Disjunction Handling in LP
- 10:35An Overview of Double Description Method
- 12:14Convex Hull Computation
- 14:20Multiple Adversarial Labels Elimination
- 15:59System ARENA
- 17:00Evaluation
- 18:59Comparison with CPU-based tools
- 22:23Parameter Study of Batch Size 8
- 23:15Key Takeaways
- 29:17Tested Networks
related talks
17mInput-Relational Verification of Deep Neural Networks
20mIncremental Verification of Neural Networks
23mPRIMA: General and Precise Neural Network Certification via Scalable Convex Hull
56mAbstract Domains for Machine Learning Verification
42mTowards Verification of General Neural Networks: A Dual Approach
58mBuilding Trust and Safety in Artificial Intelligence with Abstract Interpretation
55mTowards Verified Deep Learning
20mVerifying Neural Networks with PyRAT