Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks

TL;DR

This paper introduces a flexible abstraction framework for neural networks that replaces neurons with linear combinations of others, enhancing reduction and precision through syntactic and semantic methods.

Contribution

It proposes a novel linear combination abstraction approach for neural networks, improving upon previous neuron replacement methods and including a refinement technique for better balance.

Findings

Enhanced reduction of neural networks compared to previous methods

Effective semantic and syntactic abstraction implementations

Refinement method improves abstraction precision

Abstract

Abstraction is a key verification technique to improve scalability. However, its use for neural networks is so far extremely limited. Previous approaches for abstracting classification networks replace several neurons with one of them that is similar enough. We can classify the similarity as defined either syntactically (using quantities on the connections between neurons) or semantically (on the activation values of neurons for various inputs). Unfortunately, the previous approaches only achieve moderate reductions, when implemented at all. In this work, we provide a more flexible framework where a neuron can be replaced with a linear combination of other neurons, improving the reduction. We apply this approach both on syntactic and semantic abstractions, and implement and evaluate them experimentally. Further, we introduce a refinement method for our abstractions, allowing for finding a better balance between reduction and precision.