A DPLL(T) Framework for Verifying Deep Neural Networks
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.
Code (1)
Similar Papers 제목 키워드 기반
On the Tour Towards DPLL(MAPF) and Beyond
We discuss milestones on the tour towards DPLL(MAPF), a multi-agent path finding (MAPF) solver fully integrated with the Davis-Putnam-Logemann-Loveland (DPLL) propositional satisfiability testing algorithm through satisf…
Multi-Agent Path FindingNavigateSubsumption-driven clause learning with DPLL+restarts
We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approach allows the refutation of pebbling form…
Probabilistic Inference Modulo Theories
We present SGDPLL(T), an algorithm that solves (among many other problems) probabilistic inference modulo theories, that is, inference problems over probabilistic models defined via a logic theory provided as a parameter…
Forward LTLf Synthesis: DPLL At Work
This paper proposes a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (\LTLf), that overcomes some limitations of previous approaches. Within such framework, we devise a procedur…
Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
Modern SMT solvers have revolutionized the approach to constraint satisfaction problems by integrating advanced theory reasoning and encoding techniques. In this work, we evaluate the performance of modern SMT solvers in…
Benchmarking