Verifying Quantized Neural Networks using SMT-Based Model Checking

Understand

Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis.

• However, concerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks.
• These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus introduce additional quantization errors.
• Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs.