Training Verification-Friendly Neural Networks via Neuron Behavior Consistency

TL;DR

This work tackles the verification-time bottleneck of neural networks in safety-critical settings by introducing neuron behavior consistency (NBC) as a training regularizer. NBC encourages activation stability across inputs within a local neighborhood, reducing unstable neurons and tightening activation bounds to facilitate formal verification. Empirical results across MNIST, Fashion-MNIST, and CIFAR-10 show NBC-trained networks achieve faster verification, higher stable-neuron ratios, and greater UNSAT% while maintaining competitive robustness, and NBC can be effectively combined with existing training approaches to further boost verifiability. The method demonstrates practical impact by enabling verification-friendly networks for larger architectures without prohibitive training costs, with some trade-offs in accuracy that can be managed by tuning hyperparameters and combining with other verifiers or training schemes.

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.

Figures (3)

• Figure 1: The Branch and Bound (BaB) verification process
• Figure 2: Overview of last epoch results. For each metric at each perturbation radius, the best-performing value is defined as 100, with other values scaled proportionally. We average all the scaled values of each model at each perturbation radius in each dataset to obtain the final score. For each metric, the larger value indicates better performance.
• Figure 3: Networks trained with $\varepsilon={2}/{255}$ on CIFAR-10 dataset and evaluated on $\varepsilon={2}/{255}$. Methods unable to achieve a given accuracy range are omitted. 'Natural' means the network is trained with only cross-entropy loss.

Theorems & Definitions (1)

• Definition 1: Neural Network Verification Problem