Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq

• URL: http://arxiv.org/abs/2301.12893v1
• Date: Mon, 30 Jan 2023 13:53:52 GMT
• Title: Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
• Authors: Andrei Aleksandrov and Kim V\"ollinger
• Abstract summary: We present the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks within Coq. As a proof-of-concept, we construct the popular pwa activation function ReLU. Our formalization paves the way for integrating Coq in frameworks of neural network verification as a fallback prover when automated proving fails.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verification of neural networks relies on activation functions being piecewise affine (pwa) -- enabling an encoding of the verification problem for theorem provers. In this paper, we present the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks within Coq using the library Coquelicot for real analysis. As a proof-of-concept, we construct the popular pwa activation function ReLU. We integrate our formalization into a Coq model of neural networks, and devise a verified transformation from a neural network N to a pwa function representing N by composing pwa functions that we construct for each layer. This representation enables encodings for proof automation, e.g. Coq's tactic lra -- a decision procedure for linear real arithmetic. Further, our formalization paves the way for integrating Coq in frameworks of neural network verification as a fallback prover when automated proving fails.

Related papers

• ReLUs Are Sufficient for Learning Implicit Neural Representations [17.786058035763254]
  We revisit the use of ReLU activation functions for learning implicit neural representations. Inspired by second order B-spline wavelets, we incorporate a set of simple constraints to the ReLU neurons in each layer of a deep neural network (DNN) We demonstrate that, contrary to popular belief, one can learn state-of-the-art INRs based on a DNN composed of only ReLU neurons.
  arXiv  Detail & Related papers  (2024-06-04T17:51:08Z)
• Complexity of Injectivity and Verification of ReLU Neural Networks [5.482420806459269]
  Injectivity of a function computed by a ReLU network plays a crucial role whenever invertibility of the function is required.<n>We prove coNP-completeness of the exact computational complexity of deciding injectivity.<n>We also study the network verification problem which is to verify that certain inputs only yield specific outputs.
  arXiv  Detail & Related papers  (2024-05-30T08:14:34Z)
• Permutation Equivariant Neural Functionals [92.0667671999604]
  This work studies the design of neural networks that can process the weights or gradients of other neural networks. We focus on the permutation symmetries that arise in the weights of deep feedforward networks because hidden layer neurons have no inherent order. In our experiments, we find that permutation equivariant neural functionals are effective on a diverse set of tasks.
  arXiv  Detail & Related papers  (2023-02-27T18:52:38Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• A Sparse Coding Interpretation of Neural Networks and Theoretical Implications [0.0]
  Deep convolutional neural networks have achieved unprecedented performance in various computer vision tasks. We propose a sparse coding interpretation of neural networks that have ReLU activation. We derive a complete convolutional neural network without normalization and pooling.
  arXiv  Detail & Related papers  (2021-08-14T21:54:47Z)
• Optimal Approximation with Sparse Neural Networks and Applications [0.0]
  We use deep sparsely connected neural networks to measure the complexity of a function class in $L(mathbb Rd)$. We also introduce representation system - a countable collection of functions to guide neural networks. We then analyse the complexity of a class called $beta$ cartoon-like functions using rate-distortion theory and wedgelets construction.
  arXiv  Detail & Related papers  (2021-08-14T05:14:13Z)
• On reaction network implementations of neural networks [0.0]
  This paper is concerned with the utilization of deterministically modeled chemical reaction networks for the implementation of (feed-forward) neural networks. We develop a general mathematical framework and prove that the ordinary differential equations (ODEs) associated with certain reaction network implementations of neural networks have desirable properties.
  arXiv  Detail & Related papers  (2020-10-26T02:37:26Z)
• How Neural Networks Extrapolate: From Feedforward to Graph Neural Networks [80.55378250013496]
  We study how neural networks trained by gradient descent extrapolate what they learn outside the support of the training distribution. Graph Neural Networks (GNNs) have shown some success in more complex tasks.
  arXiv  Detail & Related papers  (2020-09-24T17:48:59Z)
• UNIPoint: Universally Approximating Point Processes Intensities [125.08205865536577]
  We provide a proof that a class of learnable functions can universally approximate any valid intensity function. We implement UNIPoint, a novel neural point process model, using recurrent neural networks to parameterise sums of basis function upon each event.
  arXiv  Detail & Related papers  (2020-07-28T09:31:56Z)
• Modeling from Features: a Mean-field Framework for Over-parameterized Deep Neural Networks [54.27962244835622]
  This paper proposes a new mean-field framework for over- parameterized deep neural networks (DNNs) In this framework, a DNN is represented by probability measures and functions over its features in the continuous limit. We illustrate the framework via the standard DNN and the Residual Network (Res-Net) architectures.
  arXiv  Detail & Related papers  (2020-07-03T01:37:16Z)
• Measuring Model Complexity of Neural Networks with Curve Activation Functions [100.98319505253797]
  We propose the linear approximation neural network (LANN) to approximate a given deep model with curve activation function. We experimentally explore the training process of neural networks and detect overfitting. We find that the $L1$ and $L2$ regularizations suppress the increase of model complexity.
  arXiv  Detail & Related papers  (2020-06-16T07:38:06Z)
• Scalable Partial Explainability in Neural Networks via Flexible Activation Functions [13.71739091287644]
  High dimensional features and decisions given by deep neural networks (NN) require new algorithms and methods to expose its mechanisms. Current state-of-the-art NN interpretation methods focus more on the direct relationship between NN outputs and inputs rather than the NN structure and operations itself. In this paper, we achieve partially explainable learning model by symbolically explaining the role of activation functions (AF) under a scalable topology.
  arXiv  Detail & Related papers  (2020-06-10T20:30:15Z)

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.