Geometric Path Enumeration for Equivalence Verification of Neural Networks

• URL: http://arxiv.org/abs/2112.06582v1
• Date: Mon, 13 Dec 2021 11:56:08 GMT
• Title: Geometric Path Enumeration for Equivalence Verification of Neural Networks
• Authors: Samuel Teuber, Marko Kleine B\"uning, Philipp Kern and Carsten Sinz
• Abstract summary: We focus on the formal verification problem of NN equivalence which aims to prove that two NNs show equivalent behavior. We show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use.
• Score: 2.007262412327553
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear programming and interval propagation. While the first approach lacks scalability, the latter is only suitable for structurally similar NNs with small weight changes. The contribution of our paper has four parts. First, we show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. Secondly, we extend Tran et al.'s single NN geometric path enumeration algorithm to a setting with multiple NNs. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use. Finally, we perform a comparative evaluation showing use-cases where our approach outperforms the previous state of the art, both, for equivalence verification as well as for counter-example finding.

Related papers

• A Fresh Look at Generalized Category Discovery through Non-negative Matrix Factorization [83.12938977698988]
  Generalized Category Discovery (GCD) aims to classify both base and novel images using labeled base data. Current approaches inadequately address the intrinsic optimization of the co-occurrence matrix $barA$ based on cosine similarity. We propose a Non-Negative Generalized Category Discovery (NN-GCD) framework to address these deficiencies.
  arXiv  Detail & Related papers  (2024-10-29T07:24:11Z)
• Correctness Verification of Neural Networks Approximating Differential Equations [0.0]
  Neural Networks (NNs) approximate the solution of Partial Differential Equations (PDEs) NNs can become integral parts of simulation software tools which can accelerate the simulation of complex dynamic systems more than 100 times. This work addresses the verification of these functions by defining the NN derivative as a finite difference approximation. For the first time, we tackle the problem of bounding an NN function without a priori knowledge of the output domain.
  arXiv  Detail & Related papers  (2024-02-12T12:55:35Z)
• Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
  This paper presents a theoretical analysis of linearahead as a principled method for stabilizing (large-scale) neural network training. We argue that instabilities in the optimization process are often caused by the nonmonotonicity of the loss landscape and show how linear can help by leveraging the theory of nonexpansive operators.
  arXiv  Detail & Related papers  (2023-10-20T12:45:12Z)
• Towards Better Out-of-Distribution Generalization of Neural Algorithmic Reasoning Tasks [51.8723187709964]
  We study the OOD generalization of neural algorithmic reasoning tasks. The goal is to learn an algorithm from input-output pairs using deep neural networks.
  arXiv  Detail & Related papers  (2022-11-01T18:33:20Z)
• Deep Learning meets Nonparametric Regression: Are Weight-Decayed DNNs Locally Adaptive? [16.105097124039602]
  We study the theory of neural network (NN) from the lens of classical nonparametric regression problems. Our research sheds new lights on why depth matters and how NNs are more powerful than kernel methods.
  arXiv  Detail & Related papers  (2022-04-20T17:55:16Z)
• Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
  We propose a novel machine learning framework that can be used for designing an effective branching strategy. We learn two graph neural networks (GNNs) that both directly treat the network we want to verify as a graph input. We show that our GNN models generalize well to harder properties on larger unseen networks.
  arXiv  Detail & Related papers  (2021-07-27T14:42:57Z)
• Neural Optimization Kernel: Towards Robust Deep Learning [13.147925376013129]
  Recent studies show a connection between neural networks (NN) and kernel methods. This paper proposes a novel kernel family named Kernel (NOK) We show that over parameterized deep NN (NOK) can increase the expressive power to reduce empirical risk and reduce the bound generalization at the same time.
  arXiv  Detail & Related papers  (2021-06-11T00:34:55Z)
• A Convergence Theory Towards Practical Over-parameterized Deep Neural Networks [56.084798078072396]
  We take a step towards closing the gap between theory and practice by significantly improving the known theoretical bounds on both the network width and the convergence time. We show that convergence to a global minimum is guaranteed for networks with quadratic widths in the sample size and linear in their depth at a time logarithmic in both. Our analysis and convergence bounds are derived via the construction of a surrogate network with fixed activation patterns that can be transformed at any time to an equivalent ReLU network of a reasonable size.
  arXiv  Detail & Related papers  (2021-01-12T00:40:45Z)
• Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach [1.9493449206135296]
  We consider formally verifying the complexity of ReLU Neural Networks (NNs) In this paper, we show that for two different NNs, the verification problem satisfies two different types of constraints. Both algorithms efficiently translate the NN parameters into the effect of the NN's architecture by means of hyperplanes.
  arXiv  Detail & Related papers  (2020-12-22T00:29:54Z)
• Fast Learning of Graph Neural Networks with Guaranteed Generalizability: One-hidden-layer Case [93.37576644429578]
  Graph neural networks (GNNs) have made great progress recently on learning from graph-structured data in practice. We provide a theoretically-grounded generalizability analysis of GNNs with one hidden layer for both regression and binary classification problems.
  arXiv  Detail & Related papers  (2020-06-25T00:45:52Z)
• Optimization and Generalization Analysis of Transduction through Gradient Boosting and Application to Multi-scale Graph Neural Networks [60.22494363676747]
  It is known that the current graph neural networks (GNNs) are difficult to make themselves deep due to the problem known as over-smoothing. Multi-scale GNNs are a promising approach for mitigating the over-smoothing problem. We derive the optimization and generalization guarantees of transductive learning algorithms that include multi-scale GNNs.
  arXiv  Detail & Related papers  (2020-06-15T17:06:17Z)

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.