Training Verification-Friendly Neural Networks via Neuron Behavior Consistency
This addresses the critical security assurance challenge in formal verification for neural networks, offering a novel training approach that enhances verifiability, though it appears incremental as it builds on existing methods.
The paper tackles the problem of long verification times for neural networks by introducing a method to train verification-friendly networks that are robust, easy to verify, and relatively accurate, achieving improved verifiability across datasets like MNIST, Fashion-MNIST, and CIFAR-10 with various architectures, where other tools fail as verification radius increases.
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.