Incremental Verification of Fixed-Point Implementations of Neural Networks

TL;DR

This paper introduces a novel symbolic verification framework for fixed-point neural network implementations, combining incremental BMC, SMT, and invariant inference to verify safety and generate adversarial examples, especially considering finite-precision arithmetic.

Contribution

It presents the first bit-precise symbolic verification framework for CUDA-based neural networks that accounts for finite-precision effects, improving guarantees over existing methods.

Findings

Successfully verified safety properties in actual neural network implementations.

Generated adversarial examples for 85.8% of test cases.

Verified 100% of coverage-related properties.

Abstract

Implementations of artificial neural networks (ANNs) might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are barely interpretable. Here, we develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference, to obtain adversarial cases and validate coverage methods in a multi-layer perceptron (MLP). We exploit incremental BMC based on interval analysis to compute boundaries from a neuron's input. Then, the latter are propagated to effectively find a neuron's output since it is the input of the next one. This paper describes the first bit-precise symbolic verification framework to reason over actual implementations of ANNs in CUDA, based on invariant inference, therefore providing further guarantees about finite-precision arithmetic and its rounding errors, which are routinely ignored in the existing literature. We have implemented the proposed approach on top of the efficient SMT-based bounded model checker (ESBMC), and its experimental results show that it can successfully verify safety properties, in actual implementations of ANNs, and generate real adversarial cases in MLPs. Our approach was able to verify and produce adversarial examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods. Although our verification time is higher than existing approaches, our methodology can consider fixed-point implementation aspects that are disregarded by the state-of-the-art verification methodologies.