  The robustness of deep neural networks is crucial to modern AI-enabled
systems and should be formally verified. Sigmoid-like neural networks have been
adopted in a wide range of applications. Due to their non-linearity,
Sigmoid-like activation functions are usually over-approximated for efficient
verification, which inevitably introduces imprecision. Considerable efforts
have been devoted to finding the so-called tighter approximations to obtain
more precise verification results. However, existing tightness definitions are
heuristic and lack theoretical foundations. We conduct a thorough empirical
analysis of existing neuron-wise characterizations of tightness and reveal that
they are superior only on specific neural networks. We then introduce the
notion of network-wise tightness as a unified tightness definition and show
that computing network-wise tightness is a complex non-convex optimization
problem. We bypass the complexity from different perspectives via two
efficient, provably tightest approximations. The results demonstrate the
promising performance achievement of our approaches over state of the art: (i)
achieving up to 251.28% improvement to certified lower robustness bounds; and
(ii) exhibiting notably more precise verification results on convolutional
networks.
