A Tale of Two Approximations: Tightening Over-Approximation for DNN
  Robustness Verification via Under-Approximation
Zhiyi Xue Si Liu Zhaodi Zhang Yiting Wu Min Zhang
The robustness of deep neural networks (DNNs) is crucial to the hosting
system's reliability and security. Formal verification has been demonstrated to
be effective in providing provable robustness guarantees. To improve its
scalability, over-approximating the non-linear activation functions in DNNs by
linear constraints has been widely adopted, which transforms the verification
problem into an efficiently solvable linear programming problem. Many efforts
have been dedicated to defining the so-called tightest approximations to reduce
overestimation imposed by over-approximation. In this paper, we study existing
approaches and identify a dominant factor in defining tight approximation,
namely the approximation domain of the activation function. We find out that
tight approximations defined on approximation domains may not be as tight as
the ones on their actual domains, yet existing approaches all rely only on
approximation domains. Based on this observation, we propose a novel
dual-approximation approach to tighten over-approximations, leveraging an
activation function's underestimated domain to define tight approximation
bounds. We implement our approach with two complementary algorithms based
respectively on Monte Carlo simulation and gradient descent into a tool called
DualApp. We assess it on a comprehensive benchmark of DNNs with different
architectures. Our experimental results show that DualApp significantly
outperforms the state-of-the-art approaches with 100% - 1000% improvement on
the verified robustness ratio and 10.64% on average (up to 66.53%) on the
certified lower bound.