Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification

• URL: http://arxiv.org/abs/2603.14823v1
• Date: Mon, 16 Mar 2026 04:57:44 GMT
• Title: Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification
• Abstract summary: Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations.<n>Current dataflow approaches operate with blind refinement processes that rely on statics.<n>We propose DRG-BaB, a framework that introduces the Directional Gap to prioritize branching on neurons actively contributing to falsification.
• Score: 10.808953992870954
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations, necessitating formal verification for safety-critical deployment. To address the computational complexity of this task, researchers often employ abstraction-refinement techniques that iteratively tighten an over-approximated model. While structural methods utilize Counterexample-Guided Abstraction Refine- ment, state-of-the-art dataflow verifiers typically rely on Branch-and-Bound to refine numerical convex relaxations. However, current dataflow approaches operate with blind refinement processes that rely on static heuristics and fail to leverage specific diagnostic information from verification failures. In this work, we argue that Branch-and-Bound should be reformulated as a Dataflow CEGAR loop where the spurious counterexample serves as a precise witness to local abstraction errors. We propose DRG-BaB, a framework that introduces the Directional Relaxation Gap heuristic to prioritize branching on neurons actively contributing to falsification in the abstract domain. By deriving a closed-form spurious counterexample directly from linear bounds, our method transforms generic search into targeted refinement. Experiments on high-dimensional benchmarks demonstrate that this approach significantly reduces search tree size and verification time compared to established baselines.

Related papers

• From Open Loop to Closed Loop: A Test-Time Iterative Optimization Framework for Reference-Consistent Image Generation [108.02425846269234]
  controllable image generation has made significant strides by incorporating visual reference conditions.<n>Existing methods predominantly operate as open-loop systems.<n>We propose a novel test-time iterative optimization framework that reformulates reference-consistent generation as a closed-loop dynamic tracking problem.
  arXiv  Detail & Related papers  (2026-07-06T05:36:30Z)
• SemFlowRAG: Directed Semantic Flow from Abstraction to Evidence for Complex Reasoning [15.817479351881062]
  SemFlowRAG is a framework that reconstructs the flat retrieval space into a corpus-adaptive gradient semantic graph.<n>By quantifying the semantic abstractness of entities through the embedding variance of their associated passages, we transform static undirected edges into directed semantic constraints.<n>We show that SemFlowRAG effectively mitigates the probability black holes'' issue, outperforming existing baselines in both retrieval and downstream reasoning performance.
  arXiv  Detail & Related papers  (2026-06-26T08:40:08Z)
• Need We Teach Foundation Models What is a Generative Image? Gradient-Free Generative Artifact Detection via Analytic Spectral Adaptation [3.881211374324378]
  Adapting foundation models to detect generative artifacts via gradient-based updates compromises their intrinsic representations.<n>We propose a gradient-free methodology reframing detection from binary classification to an out-of-distribution (OOD) anomaly measurement problem.
  arXiv  Detail & Related papers  (2026-06-03T13:04:23Z)
• Efficient Discovery of Approximate Causal Abstractions via Neural Mechanism Sparsification [0.0]
  Neural networks are hypothesized to implement interpretable causal mechanisms.<n> verifying this requires finding a causal abstraction -- a simpler, high-level Structural Causal Model (SCM) faithful to the network under interventions.<n>We reframe the problem by viewing structured pruning as a search over approximate abstractions.
  arXiv  Detail & Related papers  (2026-02-27T18:35:10Z)
• Registration is a Powerful Rotation-Invariance Learner for 3D Anomaly Detection [64.0168648353038]
  3D anomaly detection in point-cloud data is critical for industrial quality control, aiming to identify structural defects with high reliability.<n>Current memory bank-based methods often suffer from inconsistent feature transformations and limited discriminative capacity.<n>We propose a registration-induced, rotation-invariant feature extraction framework that integrates the objectives of point-cloud registration and memory-based anomaly detection.
  arXiv  Detail & Related papers  (2025-10-19T14:56:38Z)
• Rethinking Contrastive Learning in Graph Anomaly Detection: A Clean-View Perspective [54.605073936695575]
  Graph anomaly detection aims to identify unusual patterns in graph-based data, with wide applications in fields such as web security and financial fraud detection.<n>Existing methods rely on contrastive learning, assuming that a lower similarity between a node and its local subgraph indicates abnormality.<n>The presence of interfering edges invalidates this assumption, since it introduces disruptive noise that compromises the contrastive learning process.<n>We propose a Clean-View Enhanced Graph Anomaly Detection framework (CVGAD), which includes a multi-scale anomaly awareness module to identify key sources of interference in the contrastive learning process.
  arXiv  Detail & Related papers  (2025-05-23T15:05:56Z)
• SINDER: Repairing the Singular Defects of DINOv2 [61.98878352956125]
  Vision Transformer models trained on large-scale datasets often exhibit artifacts in the patch token they extract. We propose a novel fine-tuning smooth regularization that rectifies structural deficiencies using only a small dataset.
  arXiv  Detail & Related papers  (2024-07-23T20:34:23Z)
• Self-Supervised Training with Autoencoders for Visual Anomaly Detection [61.62861063776813]
  We focus on a specific use case in anomaly detection where the distribution of normal samples is supported by a lower-dimensional manifold. We adapt a self-supervised learning regime that exploits discriminative information during training but focuses on the submanifold of normal examples. We achieve a new state-of-the-art result on the MVTec AD dataset -- a challenging benchmark for visual anomaly detection in the manufacturing domain.
  arXiv  Detail & Related papers  (2022-06-23T14:16:30Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  We train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations. We propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement.
  arXiv  Detail & Related papers  (2022-06-08T04:09:13Z)

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.