PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull
summary
PRIMA presents a verifier that computes scalable convex-hull abstractions for groups of neurons using a novel dual-space partial double description method and approximate convex-hull intersection. It handles any activation (ReLU, Sigmoid, Tanh), yields only ~5% extra volume versus exact hulls, produces up to 200x speedup, and verifies 20–34% more images than prior work on different activations. It certifies a realistic autonomous‑driving CNN with 27 million connections in minutes and reduces per-example analysis to ~50 seconds on smaller problems.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:31Neural Networks Lack Trustworthiness
- 1:41Problem Statement Neural Network Verification
- 2:07Neural Network Verification via Abstract Interpretation
- 2:34Example Specification
- 3:52Main Challenge
- 4:23The Neural Network Verification Race
- 5:03Abstracting Non-Linear Activations
- 10:07Duals of Polyhedra
- 10:52Polyhedra Representation
- 11:37Batch Intersection
- 13:52Boosting Precision
- 17:29Verification Performance
- 18:40Application Verification for Autonomous Driving
- 20:11Summary
related talks
14mConvex Hull Approximation for Activation Functions
30mBoosting Multi-Neuron Convex Relaxation for Neural Network Verification
31mARENA: Enhancing Abstract Refinement for Neural Network Verification
25mProof transfer for fast certification of multiple approximate neural networks
20mIncremental Verification of Neural Networks
18mReLU Hull Approximation
42mTowards Verification of General Neural Networks: A Dual Approach
20mSupport Triangle Machine