Training Verification-Friendly Neural Networks via Neuron Behavior Consistency

TL;DR

This paper presents a training method for neural networks that enhances their verifiability by ensuring neuron behavior consistency, leading to more robust and easily verifiable models across various datasets and architectures.

Contribution

The work introduces a novel training approach that incorporates neuron behavior consistency, improving neural network verifiability without sacrificing accuracy.

Findings

Networks trained with our method are verification-friendly across different radii and architectures.

Our approach reduces unstable neurons and tightens neuron bounds, facilitating formal verification.

Combining our method with existing techniques further enhances network verifiability.

Abstract

Formal verification provides critical security assurances for neural networks, yet its practical application suffers from the long verification time. This work introduces a novel method for training verification-friendly neural networks, which are robust, easy to verify, and relatively accurate. Our method integrates neuron behavior consistency into the training process, making neuron activation states remain consistent across different inputs within a local neighborhood. This reduces the number of unstable neurons and tightens the bounds of neurons thereby enhancing the network's verifiability. We evaluated our method using the MNIST, Fashion-MNIST, and CIFAR-10 datasets with various network architectures. The experimental results demonstrate that networks trained using our method are verification-friendly across different radii and architectures, whereas other tools fail to maintain verifiability as the radius increases. Additionally, we show that our method can be combined with existing approaches to further improve the verifiability of networks.