SecureCROWN enables privacy-preserving neural network robustness verification via secure two-party computation, eliminating data-dependent branching using ReLU arithmetic and Newton-Raphson refinement.
A dpll(t) framework for verifying deep neural networks
2 Pith papers cite this work. Polarity classification is still indexing.
abstract
Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs can have bugs and can be attacked. To address this, research has explored a wide-range of algorithmic approaches to verify DNN behavior. In this work, we introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers. A key feature of SMT solvers is the use of conflict clause learning and search restart to scale verification. Unlike prior DNN verification approaches, NeuralSAT combines an abstraction-based deductive theory solver with clause learning and an evaluation clearly demonstrates the benefits of the approach on a set of challenging verification benchmarks.
years
2026 2verdicts
CONDITIONAL 2representative citing papers
A reusable framework generates verification instances with provably known robustness labels, revealing numeric tolerance issues and bugs in five verifiers while introducing difficulty profiles to diagnose failure modes.
citing papers explorer
-
Privacy-Preserving Robustness Verification for Neural Networks
SecureCROWN enables privacy-preserving neural network robustness verification via secure two-party computation, eliminating data-dependent branching using ReLU arithmetic and Newton-Raphson refinement.
-
Stress-Testing Neural Network Verifiers with Provably Robust Instances
A reusable framework generates verification instances with provably known robustness labels, revealing numeric tolerance issues and bugs in five verifiers while introducing difficulty profiles to diagnose failure modes.