REVIEW 4 cited by
A DPLL(T) Framework for Verifying Deep Neural Networks
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original 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.
Forward citations
Cited by 4 Pith papers
-
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.
-
IoUCert: Robustness Verification for Anchor-based Object Detectors
IoUCert derives exact IoU bounds over anchor-offset boxes via a coordinate transformation and uses them to formally verify single-object SSD, YOLOv2, and YOLOv3 models under brightness, contrast, and motion-blur pertu...
-
Influence-Guided Concolic Testing of Transformer Robustness
SHAP-based branch prioritization lets a concolic tester find subtle one-pixel attacks on small Transformer classifiers, but the reported evidence is mixed and the abstract overstates results.
Discussion (0). Sign in to comment.