  The robustness of neural networks is fundamental to the hosting system's
reliability and security. Formal verification has been proven to be effective
in providing provable robustness guarantees. To improve the verification
scalability, over-approximating the non-linear activation functions in neural
networks by linear constraints is widely adopted, which transforms the
verification problem into an efficiently solvable linear programming problem.
As over-approximations inevitably introduce overestimation, many efforts have
been dedicated to defining the tightest possible approximations. Recent studies
have however showed that the existing so-called tightest approximations are
superior to each other. In this paper we identify and report an crucial factor
in defining tight approximations, namely the approximation domains of
activation functions. We observe that existing approaches only rely on
overestimated domains, while the corresponding tight approximation may not
necessarily be tight on its actual domain. We propose a novel
under-approximation-guided approach, called dual-approximation, to define tight
over-approximations and two complementary under-approximation algorithms based
on sampling and gradient descent. The overestimated domain guarantees the
soundness while the underestimated one guides the tightness. We implement our
approach into a tool called DualApp and extensively evaluate it on a
comprehensive benchmark of 84 collected and trained neural networks with
different architectures. The experimental results show that DualApp outperforms
the state-of-the-art approximation-based approaches, with up to 71.22%
improvement to the verification result.
