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 https://github.com/ChristopherBrix/vnncomp2023_benchmarks/tree/main/benchmarks/traffic_signs_recognition. 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.

翻译：交通标志在自动驾驶系统的道路安全和交通管理中发挥着关键作用。准确的交通标志分类至关重要，但由于对抗样本和遮挡等现实世界的复杂性而具有挑战性。为解决这些问题，二值神经网络有望构建适用于资源受限设备的分类器。在我们先前的工作中，我们针对交通标志识别提出了高精度二值神经网络模型，重点关注适用于有限计算和能源资源的紧凑尺寸。为评估其局部鲁棒性，本文引入了一组基准问题，其网络层对最先进的验证工具构成挑战。这些层包括二值化卷积、最大池化、批归一化和全连接层。验证问题的难度源于大量网络参数（90.5万至170万）、输入维度（2700至1.2万）以及区域数量（43），同时网络并非稀疏。所提出的二值神经网络模型和局部鲁棒性属性可在https://github.com/ChristopherBrix/vnncomp2023_benchmarks/tree/main/benchmarks/traffic_signs_recognition 查看。第四届国际神经网络验证竞赛（VNN-COMP'23）的结果显示，7个求解器中有4个能够处理我们随机选取的多个基准测试（在45个中，最小值为6个，最大值为36个）。令人惊讶的是，部分工具还输出了错误结果或缺失反例（范围从1到4个）。目前，我们的重点在于通过延长分配时间（此前为8分钟）来探索实现更多求解实例的可能性。此外，我们对某些基准测试中工具产生错误结果的原因颇感兴趣。