A DPLL(T) Framework for Verifying Deep Neural Networks
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911761468227584 |
|---|---|
| author | Duong, Hai Nguyen, ThanhVu Dwyer, Matthew |
| author_facet | Duong, Hai Nguyen, ThanhVu Dwyer, Matthew |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_10266 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | A DPLL(T) Framework for Verifying Deep Neural Networks Duong, Hai Nguyen, ThanhVu Dwyer, Matthew Machine Learning Logic in Computer Science Software Engineering 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. |
| title | A DPLL(T) Framework for Verifying Deep Neural Networks |
| topic | Machine Learning Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2307.10266 |