Name
Abstract | ||
|---|---|---|
Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network's properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks. We describe the system architecture and main components, evaluate the technique and discuss ongoing work. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1007/978-3-030-25540-4_26 | COMPUTER AIDED VERIFICATION, CAV 2019, PT I |
Field | DocType | Volume |
Complex system,Computer science,Constraint satisfaction problem,Theoretical computer science,Network topology,Systems architecture,Network analysis,Artificial neural network,Certification,Scalability,Distributed computing | Conference | 11561 |
ISSN | Citations | PageRank |
0302-9743 | 13 | 0.58 |
References | Authors | |
0 | 13 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Guy Katz | 1 | 261 | 17.17 |
| Derek A. Huang | 2 | 13 | 0.58 |
| Duligur Ibeling | 3 | 13 | 2.27 |
| Kyle Julian | 4 | 176 | 6.00 |
| Christopher Lazarus | 5 | 13 | 0.58 |
| Rachel Lim | 6 | 13 | 0.58 |
| Parth Shah | 7 | 13 | 0.58 |
| Shantanu Thakoor | 8 | 13 | 0.92 |
| Haoze Wu | 9 | 13 | 1.93 |
| Aleksandar Zeljic | 10 | 13 | 0.58 |
| David L. Dill | 11 | 12629 | 1293.07 |
| Mykel J. Kochenderfer | 12 | 423 | 68.51 |
| Clark Barrett | 13 | 1268 | 108.65 |