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.

翻译：抽象是提升可扩展性的关键验证技术，但其在神经网络中的应用至今极为有限。此前针对分类网络的抽象方法，通常用足够相似的神经元替换若干神经元。此类相似性可按句法（基于神经元间连接量的度量）或语义（基于不同输入下神经元的激活值）进行定义。然而，既有方法即便得以实现，也仅能取得适度的缩减效果。本研究提出更灵活的框架，允许以其他神经元的线性组合替换单个神经元，从而提升缩减效果。我们将该方法分别应用于句法与语义抽象，并通过实验实现与评估。此外，我们引入针对此类抽象的精化方法，以在缩减程度与精度之间实现更优平衡。