Whats and Whys of Neural Network Verification (A Declarative Programming Perspec...
summary
Vehicle is a domain-specific language that specifies neural‑network properties in engineering terms and compiles them down to existing tools; it generates VNN‑Lib queries for Marabou SMT backend, emits differentiable loss functions for property‑driven retraining, and can produce proofs for Agda backend while the host is Haskell. The tool finds normalization and spec bugs, reports fragment/quantifier errors, and glues verification, training and theorem proving workflows — it works on collision‑avoidance/controller examples and is used for teaching.
AI-written summary · about
chapters (10)
- 0:00Neural network verification intro
- 3:36Why networks need verification
- 8:10Properties to verify
- 14:57Verification tools and VNN-LIB
- 18:28Challenges in verification
- 23:45Verifying complex systems
- 30:36Vehicle language intro
- 37:06Vehicle safety example
- 45:12Declarative languages role
- 47:40Q&A
related talks
26mTowards a Certified Proof Checker for Deep Neural Network Verification
55mTowards Verified Deep Learning
42mTowards Verification of General Neural Networks: A Dual Approach
27mProof Minimization in Neural Network Verification
17mInput-Relational Verification of Deep Neural Networks
37mNeural Networks are Programs, Too
59mVerification and Machine Learning
59mDifferential Verification of Deep Neural Networks