Verification of Sigmoidal Artificial Neural Networks using iSAT

• URL: http://arxiv.org/abs/2207.06755v1
• Date: Thu, 14 Jul 2022 09:08:38 GMT
• Title: Verification of Sigmoidal Artificial Neural Networks using iSAT
• Authors: Dominik Grundt (German Aerospace Center e.V.), Sorin Liviu Jurj (German Aerospace Center e.V.), Willem Hagemann (German Aerospace Center e.V.), Paul Kr\"oger (Carl von Ossietzky University Oldenburg), Martin Fr\"anzle (Carl von Ossietzky University Oldenburg)
• Abstract summary: We implement a dedicated interval constraint propagator for the sigmoid function into the SMT solver iSAT. We compare this approach with a compositional approach encoding the sigmoid function by basic arithmetic features available in iSAT and an approximating approach.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: This paper presents an approach for verifying the behaviour of nonlinear Artificial Neural Networks (ANNs) found in cyber-physical safety-critical systems. We implement a dedicated interval constraint propagator for the sigmoid function into the SMT solver iSAT and compare this approach with a compositional approach encoding the sigmoid function by basic arithmetic features available in iSAT and an approximating approach. Our experimental results show that the dedicated and the compositional approach clearly outperform the approximating approach. Throughout all our benchmarks, the dedicated approach showed an equal or better performance compared to the compositional approach.

Related papers

• A neural network approach for solving the Monge-Ampère equation with transport boundary condition [0.0]
  This paper introduces a novel neural network-based approach to solving the Monge-Ampere equation with the transport boundary condition. We leverage multilayer perceptron networks to learn approximate solutions by minimizing a loss function that encompasses the equation's residual, boundary conditions, and convexity constraints.
  arXiv  Detail & Related papers  (2024-10-25T11:54:00Z)
• Distance Recomputator and Topology Reconstructor for Graph Neural Networks [22.210886585639063]
  We introduce Distance Recomputator and Topology Reconstructor methodologies, aimed at enhancing Graph Neural Networks (GNNs) The Distance Recomputator dynamically recalibrates node distances using a dynamic encoding scheme, thereby improving the accuracy and adaptability of node representations. The Topology Reconstructor adjusts local graph structures based on computed "similarity distances," optimizing network configurations for improved learning outcomes.
  arXiv  Detail & Related papers  (2024-06-25T05:12:51Z)
• Front-propagation Algorithm: Explainable AI Technique for Extracting Linear Function Approximations from Neural Networks [0.0]
  This paper introduces the front-propagation algorithm, a novel AI technique designed to elucidate the decision-making logic of deep neural networks. Unlike other popular explainability algorithms such as Integrated Gradients or Shapley Values, the proposed algorithm is able to extract an accurate and consistent linear function explanation of the network. We demonstrate its efficacy in providing accurate linear functions with three different neural network architectures trained on publicly available benchmark datasets.
  arXiv  Detail & Related papers  (2024-05-25T14:50:23Z)
• Optimal Inference in Contextual Stochastic Block Models [0.0]
  The contextual block model (cSBM) was proposed for unsupervised community detection on attributed graphs. The cSBM has been widely used as a synthetic dataset for evaluating the performance of graph-neural networks (GNNs) for semi-supervised node classification. We show that there can be a considerable gap between the accuracy reached by this algorithm and the performance of the GNN architectures proposed in the literature.
  arXiv  Detail & Related papers  (2023-06-06T10:02:57Z)
• On the Effective Usage of Priors in RSS-based Localization [56.68864078417909]
  We propose a Received Signal Strength (RSS) fingerprint and convolutional neural network-based algorithm, LocUNet. In this paper, we study the localization problem in dense urban settings. We first recognize LocUNet's ability to learn the underlying prior distribution of the Rx position or Rx and transmitter (Tx) association preferences from the training data, and attribute its high performance to these.
  arXiv  Detail & Related papers  (2022-11-28T00:31:02Z)
• AskewSGD : An Annealed interval-constrained Optimisation method to train Quantized Neural Networks [12.229154524476405]
  We develop a new algorithm, Annealed Skewed SGD - AskewSGD - for training deep neural networks (DNNs) with quantized weights. Unlike algorithms with active sets and feasible directions, AskewSGD avoids projections or optimization under the entire feasible set. Experimental results show that the AskewSGD algorithm performs better than or on par with state of the art methods in classical benchmarks.
  arXiv  Detail & Related papers  (2022-11-07T18:13:44Z)
• Improved Algorithms for Neural Active Learning [74.89097665112621]
  We improve the theoretical and empirical performance of neural-network(NN)-based active learning algorithms for the non-parametric streaming setting. We introduce two regret metrics by minimizing the population loss that are more suitable in active learning than the one used in state-of-the-art (SOTA) related work.
  arXiv  Detail & Related papers  (2022-10-02T05:03:38Z)
• Exploiting Temporal Structures of Cyclostationary Signals for Data-Driven Single-Channel Source Separation [98.95383921866096]
  We study the problem of single-channel source separation (SCSS) We focus on cyclostationary signals, which are particularly suitable in a variety of application domains. We propose a deep learning approach using a U-Net architecture, which is competitive with the minimum MSE estimator.
  arXiv  Detail & Related papers  (2022-08-22T14:04:56Z)
• Tree ensemble kernels for Bayesian optimization with known constraints over mixed-feature spaces [54.58348769621782]
  Tree ensembles can be well-suited for black-box optimization tasks such as algorithm tuning and neural architecture search. Two well-known challenges in using tree ensembles for black-box optimization are (i) effectively quantifying model uncertainty for exploration and (ii) optimizing over the piece-wise constant acquisition function. Our framework performs as well as state-of-the-art methods for unconstrained black-box optimization over continuous/discrete features and outperforms competing methods for problems combining mixed-variable feature spaces and known input constraints.
  arXiv  Detail & Related papers  (2022-07-02T16:59:37Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• Sinkhorn Natural Gradient for Generative Models [125.89871274202439]
  We propose a novel Sinkhorn Natural Gradient (SiNG) algorithm which acts as a steepest descent method on the probability space endowed with the Sinkhorn divergence. We show that the Sinkhorn information matrix (SIM), a key component of SiNG, has an explicit expression and can be evaluated accurately in complexity that scales logarithmically. In our experiments, we quantitatively compare SiNG with state-of-the-art SGD-type solvers on generative tasks to demonstrate its efficiency and efficacy of our method.
  arXiv  Detail & Related papers  (2020-11-09T02:51: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.