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

• URL: http://arxiv.org/abs/2305.16998v1
• Date: Fri, 26 May 2023 14:58:30 GMT
• Title: A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation
• Authors: Zhiyi Xue, Si Liu, Zhaodi Zhang, Yiting Wu, Min Zhang
• Abstract summary: We propose a novel dual-approximation approach to tighten over-approximations, leveraging an activation function's underestimated domain to define tight approximation bounds. Our 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.
• Score: 17.924507519230424
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: 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.

Related papers

• Statistical Inference for Temporal Difference Learning with Linear Function Approximation [62.69448336714418]
  Temporal Difference (TD) learning, arguably the most widely used for policy evaluation, serves as a natural framework for this purpose. In this paper, we study the consistency properties of TD learning with Polyak-Ruppert averaging and linear function approximation, and obtain three significant improvements over existing results.
  arXiv  Detail & Related papers  (2024-10-21T15:34:44Z)
• Bridging the Gap Between End-to-End and Two-Step Text Spotting [88.14552991115207]
  Bridging Text Spotting is a novel approach that resolves the error accumulation and suboptimal performance issues in two-step methods. We demonstrate the effectiveness of the proposed method through extensive experiments.
  arXiv  Detail & Related papers  (2024-04-06T13:14:04Z)
• Enabling Uncertainty Estimation in Iterative Neural Networks [49.56171792062104]
  We develop an approach to uncertainty estimation that provides state-of-the-art estimates at a much lower computational cost than techniques like Ensembles. We demonstrate its practical value by embedding it in two application domains: road detection in aerial images and the estimation of aerodynamic properties of 2D and 3D shapes.
  arXiv  Detail & Related papers  (2024-03-25T13:06:31Z)
• Distributionally Robust Off-Dynamics Reinforcement Learning: Provable Efficiency with Linear Function Approximation [8.234072589087095]
  We study off-dynamics Reinforcement Learning (RL), where the policy is trained on a source domain and deployed to a distinct target domain. We provide the first study on online DRMDPs with function approximation for off-dynamics RL. We introduce DR-LSVI-UCB, the first provably efficient online DRMDP algorithm for off-dynamics with function approximation.
  arXiv  Detail & Related papers  (2024-02-23T16:01:44Z)
• Identity Curvature Laplace Approximation for Improved Out-of-Distribution Detection [4.779196219827508]
  Uncertainty estimation is crucial in safety-critical applications, where robust out-of-distribution detection is essential. Traditional Bayesian methods, though effective, are often hindered by high computational demands. We introduce the Identity Curvature Laplace Approximation (ICLA), a novel method that challenges the conventional posterior coimation formulation.
  arXiv  Detail & Related papers  (2023-12-16T14:46:24Z)
• DualApp: Tight Over-Approximation for Neural Network Robustness Verification via Under-Approximation [17.924507519230424]
  We propose a novel under-approximation-guided approach to define tight over-approximations and two complementary under-approximation algorithms. 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 benchmark of 84 collected and trained neural networks.
  arXiv  Detail & Related papers  (2022-11-21T05:09:34Z)
• Stabilizing Q-learning with Linear Architectures for Provably Efficient Learning [53.17258888552998]
  This work proposes an exploration variant of the basic $Q$-learning protocol with linear function approximation. We show that the performance of the algorithm degrades very gracefully under a novel and more permissive notion of approximation error.
  arXiv  Detail & Related papers  (2022-06-01T23:26:51Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• Fast Objective & Duality Gap Convergence for Non-Convex Strongly-Concave Min-Max Problems with PL Condition [52.08417569774822]
  This paper focuses on methods for solving smooth non-concave min-max problems, which have received increasing attention due to deep learning (e.g., deep AUC)
  arXiv  Detail & Related papers  (2020-06-12T00:32:21Z)
• Distributional Robustness and Regularization in Reinforcement Learning [62.23012916708608]
  We introduce a new regularizer for empirical value functions and show that it lower bounds the Wasserstein distributionally robust value function. It suggests using regularization as a practical tool for dealing with $textitexternal uncertainty$ in reinforcement learning.
  arXiv  Detail & Related papers  (2020-03-05T19:56:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.