Proof-Driven Clause Learning in Neural Network Verification

• URL: http://arxiv.org/abs/2503.12083v1
• Date: Sat, 15 Mar 2025 11:05:15 GMT
• Title: Proof-Driven Clause Learning in Neural Network Verification
• Authors: Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz,
• Abstract summary: We propose an approach for improving the scalability of DNN verifiers using Conflict-Driven Clause Learning (CDCL)<n>We present a novel algorithm for deriving conflict clauses using UNSAT proofs, and propose several optimizations for expediting it.<n>The evaluation of our implementation over several benchmarks suggests a 2X--3X improvement over a similar approach, with specific cases outperforming the state of the art.
• Score: 1.6036524120600033
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The widespread adoption of deep neural networks (DNNs) requires efficient techniques for safety verification. Existing methods struggle to scale to real-world DNNs, and tremendous efforts are being put into improving their scalability. In this work, we propose an approach for improving the scalability of DNN verifiers using Conflict-Driven Clause Learning (CDCL) -- an approach that has proven highly successful in SAT and SMT solving. We present a novel algorithm for deriving conflict clauses using UNSAT proofs, and propose several optimizations for expediting it. Our approach allows a modular integration of SAT solvers and DNN verifiers, and we implement it on top of an interface designed for this purpose. The evaluation of our implementation over several benchmarks suggests a 2X--3X improvement over a similar approach, with specific cases outperforming the state of the art.

Related papers

• Adversarially Robust Spiking Neural Networks Through Conversion [16.2319630026996]
  Spiking neural networks (SNNs) provide an energy-efficient alternative to a variety of artificial neural network (ANN) based AI applications. As the progress in neuromorphic computing with SNNs expands their use in applications, the problem of adversarial robustness of SNNs becomes more pronounced.
  arXiv  Detail & Related papers  (2023-11-15T08:33:46Z)
• A DPLL(T) Framework for Verifying Deep Neural Networks [9.422860826278788]
  Like human-written software, Deep Neural Networks (DNNs) can have bugs and can be attacked. We introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers.
  arXiv  Detail & Related papers  (2023-07-17T18:49:46Z)
• Incremental Verification of Neural Networks [3.9661031279983896]
  We propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines.
  arXiv  Detail & Related papers  (2023-04-04T15:28:22Z)
• Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks [22.015676101940077]
  We present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. We implement our algorithm as an incremental solver called DeepInc, and exerimental results show that DeepInc is more efficient in most cases.
  arXiv  Detail & Related papers  (2023-02-10T04:31:28Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• 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)
• 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)
• Automatic Mapping of the Best-Suited DNN Pruning Schemes for Real-Time Mobile Acceleration [71.80326738527734]
  We propose a general, fine-grained structured pruning scheme and corresponding compiler optimizations. We show that our pruning scheme mapping methods, together with the general fine-grained structured pruning scheme, outperform the state-of-the-art DNN optimization framework.
  arXiv  Detail & Related papers  (2021-11-22T23:53:14Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Designing Interpretable Approximations to Deep Reinforcement Learning [14.007731268271902]
  Deep neural networks (DNNs) set the bar for algorithm performance. It may not be feasible to actually use such high-performing DNNs in practice. This work seeks to identify reduced models that not only preserve a desired performance level, but also, for example, succinctly explain the latent knowledge represented by a DNN.
  arXiv  Detail & Related papers  (2020-10-28T06:33:09Z)
• Deep Multi-Task Learning for Cooperative NOMA: System Design and Principles [52.79089414630366]
  We develop a novel deep cooperative NOMA scheme, drawing upon the recent advances in deep learning (DL) We develop a novel hybrid-cascaded deep neural network (DNN) architecture such that the entire system can be optimized in a holistic manner.
  arXiv  Detail & Related papers  (2020-07-27T12:38:37Z)

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.