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.

本文研究了神经网络鲁棒性的形式化验证，提出了一种新的双重逼近方法，利用激活函数的低估区间来定义紧逼近边界，并将其实现到了名为 DualApp 的工具中，在不同体系结构的深度神经网络基准测试中，DualApp 方法得到了明显的优化

两种近似算法的故事：通过欠 - 过估算收紧 DNN 的稳健性验证

A Tale of Two Approximations: Tightening Over-Approximation for DNN  Robustness Verification via Under-Approximation

Recent e-graph applications have typically considered concrete semantics of
expressions, where the notion of equivalence stems from concrete interpretation
of expressions. However, equivalences that hold over one interpretation may not
hold in an alternative interpretation. Such an observation can be exploited. We
consider the application of abstract interpretation to e-graphs, and show that
within an e-graph, the lattice meet operation associated with the abstract
domain has a natural interpretation for an e-class, leading to improved
precision in over-approximation. In this extended abstract, we use Interval
Arithmetic (IA) to illustrate this point.

本文研究在 e-graph 应用中运用抽象解释技术，在 e-graph 中对于抽象域的 meet 操作具有自然的解释。通过采用区间算术作为示例，可以提高对分析精度的控制。

E - 图上的抽象解释

Abstract Interpretation on E-Graphs

Deep neural networks are increasingly being used as controllers for
safety-critical systems. Because neural networks are opaque, certifying their
correctness is a significant challenge. To address this issue, several neural
network verification approaches have recently been proposed. However, these
approaches afford limited scalability, and applying them to large networks can
be challenging. In this paper, we propose a framework that can enhance neural
network verification techniques by using over-approximation to reduce the size
of the network - thus making it more amenable to verification. We perform the
approximation such that if the property holds for the smaller (abstract)
network, it holds for the original as well. The over-approximation may be too
coarse, in which case the underlying verification tool might return a spurious
counterexample. Under such conditions, we perform counterexample-guided
refinement to adjust the approximation, and then repeat the process. Our
approach is orthogonal to, and can be integrated with, many existing
verification techniques. For evaluation purposes, we integrate it with the
recently proposed Marabou framework, and observe a significant improvement in
Marabou's performance. Our experiments demonstrate the great potential of our
approach for verifying larger neural networks.

本研究提出了一种通过使用过度逼近来减小神经网络规模，以提高神经网络验证技术的框架，并使用反例引导调整逼近，以验证大型神经网络。实验证明，该方法对验证大型神经网络具有很大的潜力。