  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.
