Towards a Certified Proof Checker for Deep Neural Network Verification
summary
A formally verified proof checker for deep neural network verification is implemented in Imandra and extracts to native OCaml, using Simplex proof certificates based on Farkas’ lemma and GMP arbitrary-precision reals to avoid floating‑point instability. The team specifies and mechanically proves the core correctness theorem that a negative linear combination implies unsatisfiability, with the formal development totaling 15 lemmas, 233 LOC. The prototype runs slower than the optimized C++ checker but only with a linear overhead and shows clear optimization tradeoffs (sparse vs dense vectors).
AI-written summary · about
chapters (10)
- 0:00Certified proof checkers intro
- 1:05Why verify DNNs and proof checkers
- 3:12Formally verified proof checker design
- 4:57Neural network verification and proofs
- 8:06Farkas' lemma in DNN proofs
- 11:18Imandra proof checker implementation
- 13:46Data structures and verification modes
- 15:12Correctness specification and verification
- 19:25Conclusion and future work
- 20:09Q&A
related talks
27mProof Minimization in Neural Network Verification
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
42mTowards Verification of General Neural Networks: A Dual Approach
17mInput-Relational Verification of Deep Neural Networks
14mAutomated Verification of Soundness of DNN Certifiers
55mTowards Verified Deep Learning
59mVerification and Machine Learning
11mExploiting Verified Neural Networks via Floating Point Numerical Error