Verification and Machine Learning
summary
An MILP encoding for quantized DNNs is implemented in Python with a commercial MILP backend and beats SMT baselines on standard benchmarks (315 instances across four nets), claiming up to order-of-magnitude speedup and consistent mean/median improvements while encoding fixed‑point rounding with novel linear constraints. A layerwise splitting verifier integrates symbolic bounds, targeted splitting and LP refinement to be complete and shows modest speedups over competitors. Tardis is a Rust coverage‑guided fuzzer for embedded OSes that boots instrumented images in QEMU, finds 17 previously unknown bugs, and reports ~15% coverage uplift, 27% memory and 13% execution overhead. A deductive verification framework analyzes RTEMS protocol code, uncovers mismatches in ICP and MrsP, proposes fixes/assumptions and re-verifies the implementations.
AI-written summary · about
chapters (16)
- 0:00Start
- 1:01Introduction
- 1:19Adversarial Attacks
- 4:39Sound Encoding of Rounding - Examp
- 7:50Experimental Setup
- 9:56Conclusion
- 13:37Verification of Neural Networks
- 14:42Complete Verification
- 15:13Main Framework
- 15:42Single-Pass abstract analysis (SPAA)
- 17:34Splitting by FUL Strategy
- 20:01An example
- 20:31Overview
- 41:26Resource Sharing on Real-Time Systems
- 47:08Verification of ICPP in RTEMS
- 53:47Verification Framework
related talks
20mIncremental Verification of Neural Networks
15mSMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
11mExploiting Verified Neural Networks via Floating Point Numerical Error
11mQiMeng-Xpiler: Transcompiling Tensor Programs for Deep Learning Systems with a...
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
27mProof Minimization in Neural Network Verification
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
17mVerification of Bit-Flip Attacks against Quantized Neural Networks