To use neural networks in safety-critical settings it is paramount to provide
assurances on their runtime operation. Recent work on ReLU networks has sought
to verify whether inputs belonging to a bounded box can ever yield some
undesirable output. Input-splitting procedures, a particular type of
verification mechanism, do so by recursively partitioning the input set into
smaller sets. The efficiency of these methods is largely determined by the
number of splits the box must undergo before the property can be verified. In
this work, we propose a new technique based on shadow prices that fully
exploits the information of the problem yielding a more efficient generation of
splits than the state-of-the-art. Results on the Airborne Collision Avoidance
System (ACAS) benchmark verification tasks show a considerable reduction in the
partitions generated which substantially reduces computation times. These
results open the door to improved verification methods for a wide variety of
machine learning applications including vision and control.

本研究介绍了一种基于影子价格的新技术，可以更高效地对神经网络进行验证，降低了计算时间，同时也为视觉和控制等各种机器学习应用提供了改进的验证方法。