Output Range Analysis for Feed-Forward Deep Neural Networks via Linear Programming
Output Range Analysis for Feed-Forward Deep Neural Networks via Linear Programming
复制标题
DOI：
10.1109/tr.2022.3209081
复制
发表时间：
2023-09
影响因子：
5.9
通讯作者：
Zhiwu Xu;Yazheng Liu;S. Qin;Zhong Ming
中科院分区：
文献类型：
--
作者：
Zhiwu Xu;Yazheng Liu;S. Qin;Zhong Ming
The success of deep neural networks and their potential use in many safety-critical applications has motivated research on formal verification of deep neural networks. A fundamental primitive enabling the formal analysis of neural networks is the output range analysis. Existing approaches on output range analysis either focus on some simple activation functions, such as $\text{relu,}$ or compute a relaxed result for some activation functions, such as exponential linear unit $\text{({elu}}$). In this article, we propose an approach to compute the output range for feed-forward deep neural networks via linear programming. The key idea is to encode the activation functions, such as $\text{{elu}}$ and $\text{sigmoid}$, as linear constraints in term of the line between the left and right end-points of the input range and the tangent lines on some special points in the input range. A strategy to partition the network to get a tighter range is presented. The experimental results show that our approach gets a tighter result than RobustVerifier on $\text{{elu}}$ networks and $\text{sigmoid}$ networks. Moreover, our approach performs better than (the linear encodings implemented in) Crown on $\text{{elu}}$ networks with $\alpha =0.5, 1.0$ and $\text{sigmoid}$ networks, and better than CNN-Cert and DeepCert on $\text{{elu}}$ networks with $\alpha = 0.5$ or 1.0. For $\text{{elu}}$ networks with $\alpha = 2.0$, our approach can achieve results that are closed to Crown, CNN-Cert, and DeepCert. Finally, we also found that the network partition helps to achieve a tighter result as well as to improve the efficiency for $\text{{elu}}$ networks.
The success of deep neural networks and their potential use in many safety-critical applications has motivated research on formal verification of deep neural networks. A fundamental primitive enabling the formal analysis of neural networks is the output range analysis. Existing approaches on output range analysis either focus on some simple activation functions, such as $\text{relu,}$ or compute a relaxed result for some activation functions, such as exponential linear unit $\text{({elu}}$). In this article, we propose an approach to compute the output range for feed-forward deep neural networks via linear programming. The key idea is to encode the activation functions, such as $\text{{elu}}$ and $\text{sigmoid}$, as linear constraints in term of the line between the left and right end-points of the input range and the tangent lines on some special points in the input range. A strategy to partition the network to get a tighter range is presented. The experimental results show that our approach gets a tighter result than RobustVerifier on $\text{{elu}}$ networks and $\text{sigmoid}$ networks. Moreover, our approach performs better than (the linear encodings implemented in) Crown on $\text{{elu}}$ networks with $\alpha =0.5, 1.0$ and $\text{sigmoid}$ networks, and better than CNN-Cert and DeepCert on $\text{{elu}}$ networks with $\alpha = 0.5$ or 1.0. For $\text{{elu}}$ networks with $\alpha = 2.0$, our approach can achieve results that are closed to Crown, CNN-Cert, and DeepCert. Finally, we also found that the network partition helps to achieve a tighter result as well as to improve the efficiency for $\text{{elu}}$ networks.