Verifying Low-dimensional Input Neural Networks via Input Quantization
summary
Prepending an input quantization layer maps every low‑dimensional input to the original ACAS Xu grid so pretrained networks need no retraining and run nearest‑neighbor interpolation at inference. Verification then simply enumerate all quantized inputs, bounding complexity by quantization size; experiments on φ9 show orders‑of‑magnitude speedups versus ReluVal and linear scaling with network size. Running the actual inference implementation yields exact floating‑point outputs and a complete, sound check so long as the quantization grid is small enough and accuracy is acceptable.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:15Motivating Example: ACAS Xu Benchmark
- 0:34ACAS Xu Input
- 1:11Conventional Training/Verification Procedure
- 2:09Conventional Training/Verification Problems
- 3:14Proposed Training/Verification Procedure
- 3:42Input Quantization Layer
- 5:07Experiment Results
- 6:08Problems Solved Previous Verification is slow
- 7:00Conclusion & Discussion • Input quantization enables efficient, complete, and sound verification Prerequisite
related talks
34mBeyond the Continuum: The Importance of Quantization in Deep Learning
20mIncremental Verification of Neural Networks
15mQuantization with Guaranteed Floating-Point Neural Network Classifications
25mProof transfer for fast certification of multiple approximate neural networks
40mUnlocking Local LLMs with Quantization
42mTowards Verification of General Neural Networks: A Dual Approach
17mVerification of Bit-Flip Attacks against Quantized Neural Networks
23mTowards Bit-Level Dominance Preserving Quantization of Neural Classifiers