Proof Minimization in Neural Network Verification
summary
Algorithms that shrink unsat proofs from DNN verifiers by removing learned lemmas and unnecessary dependencies, implemented on the Marabou verifier and tested on six benchmarks. Uses Farkas‑style certificates for leaves, backward dependency marking, and a knapsack‑style delta pruning to drop lemmas. Results show 37%-82% proof size reduction, 30%-88% faster proof checking, and only 7%-20% verification runtime overhead; some instances become verifiable only after minimization.
AI-written summary · about
chapters (10)
- 0:00Proof minimization intro
- 3:57Neural network verification background
- 8:52Proof production in CSPs
- 13:46Proof leaves structure and checking
- 14:28Why proofs can become unnecessarily large
- 16:53Backward analysis for unused lemmas
- 19:21Refining proofs by removing dependencies
- 20:46Evaluation results and impact
- 21:27Future directions and challenges
- 22:07Conclusion & Q&A
related talks
26mTowards a Certified Proof Checker for Deep Neural Network Verification
42mTowards Verification of General Neural Networks: A Dual Approach
20mIncremental Verification of Neural Networks
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
59mVerification and Machine Learning
17mInput-Relational Verification of Deep Neural Networks
55mTowards Verified Deep Learning
17mMini-Batch Robustness Verification of Deep Neural Networks