Neural Network Verification using Partial Multi-Neuron Relaxation

• URL: http://arxiv.org/abs/2605.30155v3
• Date: Tue, 02 Jun 2026 17:20:50 GMT
• Title: Neural Network Verification using Partial Multi-Neuron Relaxation
• Abstract summary: We present a middle-ground approach featuring partial multi-neuron relaxation.<n>We build upon existing branchings for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds.<n>Our experiments showcase the potential of our technique for neural network verification.
• Score: 2.2058293096044586
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.

Related papers

• NeuronSeek: On Stability and Expressivity of Task-driven Neurons [19.773883759021764]
  Prototyping task-driven neurons (referred to as NeuronSeek) employs symbolic regression (SR) to discover the optimal neuron formulation.<n>This work replaces symbolic regression with tensor decomposition (TD) to discover optimal neuronal formulations.<n>We establish theoretical guarantees that modifying the aggregation functions with common activation functions can empower a network with a fixed number of parameters to approximate any continuous function with an arbitrarily small error.
  arXiv  Detail & Related papers  (2025-06-01T01:36:27Z)
• Expressiveness of Multi-Neuron Convex Relaxations in Neural Network Certification [5.05356759900008]
  We present the first rigorous analysis of the expressiveness of multi-neuron relaxations.<n>We show that they are inherently incomplete, even when allocated sufficient resources to capture finitely many neurons and optimally layers.<n>Our findings establish a foundation for multi-neuron relaxations and point to new directions for certified robustness.
  arXiv  Detail & Related papers  (2024-10-09T12:14:24Z)
• A More Accurate Approximation of Activation Function with Few Spikes Neurons [6.306126887439676]
  spiking neural networks (SNNs) have attracted lots of attention as energy-efficient neural networks. conventional spiking neurons, such as leaky integrate-and-fire neurons, cannot accurately represent complex non-linear activation functions.
  arXiv  Detail & Related papers  (2024-08-19T02:08:56Z)
• The Expressive Leaky Memory Neuron: an Efficient and Expressive Phenomenological Neuron Model Can Solve Long-Horizon Tasks [64.08042492426992]
  We introduce the Expressive Memory (ELM) neuron model, a biologically inspired model of a cortical neuron. Our ELM neuron can accurately match the aforementioned input-output relationship with under ten thousand trainable parameters. We evaluate it on various tasks with demanding temporal structures, including the Long Range Arena (LRA) datasets.
  arXiv  Detail & Related papers  (2023-06-14T13:34:13Z)
• Zonotope Domains for Lagrangian Neural Network Verification [102.13346781220383]
  We decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. Our technique yields bounds that improve upon both linear programming and Lagrangian-based verification techniques.
  arXiv  Detail & Related papers  (2022-10-14T19:31:39Z)
• Understanding Neural Coding on Latent Manifolds by Sharing Features and Dividing Ensembles [3.625425081454343]
  Systems neuroscience relies on two complementary views of neural data, characterized by single neuron tuning curves and analysis of population activity. These two perspectives combine elegantly in neural latent variable models that constrain the relationship between latent variables and neural activity. We propose feature sharing across neural tuning curves, which significantly improves performance and leads to better-behaved optimization.
  arXiv  Detail & Related papers  (2022-10-06T18:37:49Z)
• Spiking neural network for nonlinear regression [68.8204255655161]
  Spiking neural networks carry the potential for a massive reduction in memory and energy consumption. They introduce temporal and neuronal sparsity, which can be exploited by next-generation neuromorphic hardware. A framework for regression using spiking neural networks is proposed.
  arXiv  Detail & Related papers  (2022-10-06T13:04:45Z)
• And/or trade-off in artificial neurons: impact on adversarial robustness [91.3755431537592]
  Presence of sufficient number of OR-like neurons in a network can lead to classification brittleness and increased vulnerability to adversarial attacks. We define AND-like neurons and propose measures to increase their proportion in the network. Experimental results on the MNIST dataset suggest that our approach holds promise as a direction for further exploration.
  arXiv  Detail & Related papers  (2021-02-15T08:19:05Z)
• The distribution of inhibitory neurons in the C. elegans connectome facilitates self-optimization of coordinated neural activity [78.15296214629433]
  The nervous system of the nematode Caenorhabditis elegans exhibits remarkable complexity despite the worm's small size. A general challenge is to better understand the relationship between neural organization and neural activity at the system level. We implemented an abstract simulation model of the C. elegans connectome that approximates the neurotransmitter identity of each neuron.
  arXiv  Detail & Related papers  (2020-10-28T23:11:37Z)
• Online neural connectivity estimation with ensemble stimulation [5.156484100374058]
  We propose a method based on noisy group testing that drastically increases the efficiency of this process in sparse networks. We show that it is possible to recover binarized network connectivity with a number of tests that grows only logarithmically with population size. We also demonstrate the feasibility of inferring connectivity for networks of up to tens of thousands of neurons online.
  arXiv  Detail & Related papers  (2020-07-27T23:47:03Z)
• Non-linear Neurons with Human-like Apical Dendrite Activations [81.18416067005538]
  We show that a standard neuron followed by our novel apical dendrite activation (ADA) can learn the XOR logical function with 100% accuracy. We conduct experiments on six benchmark data sets from computer vision, signal processing and natural language processing.
  arXiv  Detail & Related papers  (2020-02-02T21:09:39Z)

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.