Verifying Neural Networks with PyRAT
summary
PyRAT is a Python verifier that uses abstract interpretation with intervals, zonotopes and constrained zonotopes, is sound for floating‑point ops, and ingests ONNX nets and a property file. It performs reachability, ReLU splitting and batch or layer splits, runs a counterexample search, and scores second place at VNN‑COMP 2024. An industrial case certifies nets vs 30 GB lookup tables, proving 80–85% match and enabling a hybrid net+table image that fits in 5 GB. Free research licenses available; core code is closed.
AI-written summary · about
chapters (13)
- 0:00PyRAT introduction
- 1:31Verified architectures
- 2:34Verification challenges
- 3:40Abstract domains in PyRAT
- 5:48Intervals and zonotopes
- 7:58Constraint domains and splitting
- 9:48Bounding and parallelization
- 11:19Counterexample search
- 12:02Testing PyRAT
- 12:43PyRAT in competitions
- 13:29Drones and lookup tables
- 14:53Future and limitations
- 15:34Q&A
related talks
17mInput-Relational Verification of Deep Neural Networks
58mBuilding Trust and Safety in Artificial Intelligence with Abstract Interpretation
31mARENA: Enhancing Abstract Refinement for Neural Network Verification
20mIncremental Verification of Neural Networks
59mVerification and Machine Learning
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
42mTowards Verification of General Neural Networks: A Dual Approach
14mAutomated Verification of Soundness of DNN Certifiers