Traffic signs play a critical role in road safety and traffic management for
autonomous driving systems. Accurate traffic sign classification is essential
but challenging due to real-world complexities like adversarial examples and
occlusions. To address these issues, binary neural networks offer promise in
constructing classifiers suitable for resource-constrained devices.
In our previous work, we proposed high-accuracy BNN models for traffic sign
recognition, focusing on compact size for limited computation and energy
resources. To evaluate their local robustness, this paper introduces a set of
benchmark problems featuring layers that challenge state-of-the-art
verification tools. These layers include binarized convolutions, max pooling,
batch normalization, fully connected. The difficulty of the verification
problem is given by the high number of network parameters (905k - 1.7 M), of
the input dimension (2.7k-12k), and of the number of regions (43) as well by
the fact that the neural networks are not sparse.
The proposed BNN models and local robustness properties can be checked at
this https URL
The results of the 4th International Verification of Neural Networks
Competition (VNN-COMP'23) revealed the fact that 4, out of 7, solvers can
handle many of our benchmarks randomly selected (minimum is 6, maximum is 36,
out of 45). Surprisingly, tools output also wrong results or missing
counterexample (ranging from 1 to 4). Currently, our focus lies in exploring
the possibility of achieving a greater count of solved instances by extending
the allotted time (previously set at 8 minutes). Furthermore, we are intrigued
by the reasons behind the erroneous outcomes provided by the tools for certain
benchmarks.

交通标志、二进制神经网络、本地稳健性、验证工具、VNN-COMP'23

提升交通标志识别准确率的高准确性二进制神经网络的局部鲁棒性评估

Benchmarking Local Robustness of High-Accuracy Binary Neural Networks  for Enhanced Traffic Sign Recognition

Verification and safety assessment of neural network controlled systems
(NNCSs) is an emerging challenge. To provide guarantees, verification tools
must efficiently capture the interplay between the neural network and the
physical system within the control loop. In this paper, a compositional
approach focused on inclusion preserving long term symbolic dependency modeling
is proposed for the analysis of NNCSs. First of all, the matrix structure of
symbolic zonotopes is exploited to efficiently abstract the input/output
mapping of the loop elements through (inclusion preserving) affine symbolic
expressions, thus maintaining linear dependencies between interacting blocks.
Then, two further extensions are studied. Firstly, symbolic polynotopes are
used to abstract the loop elements behaviour by means of polynomial symbolic
expressions and dependencies. Secondly, an original input partitioning
algorithm takes advantage of symbol preservation to assess the sensitivity of
the computed approximation to some input directions. The approach is evaluated
via different numerical examples and benchmarks. A good trade-off between low
conservatism and computational efficiency is obtained.

本文提出了一种基于包含保持长期符号依赖性建模的组合方法，旨在分析神经网络控制系统的验证和安全评估，并通过数值实例和基准测试来评估该方法的有效性。