Reluplex

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.


References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Gambella, Claudio; Ghaddar, Bissan; Naoum-Sawaya, Joe: Optimization problems for machine learning: a survey (2021)
  2. Kopetzki, Anna-Kathrin; Günnemann, Stephan: Reachable sets of classifiers and regression models: (non-)robustness analysis and robust training (2021)
  3. Rössig, Ansgar; Petkovic, Milena: Advances in verification of ReLU neural networks (2021)
  4. Sotoudeh, Matthew; Thakur, Aditya V.: SyReNN: a tool for analyzing deep neural networks (2021)
  5. Tran, Hoang-Dung; Pal, Neelanjana; Manzanas Lopez, Diego; Musau, Patrick; Yang, Xiaodong; Nguyen, Luan Viet; Xiang, Weiming; Bak, Stanley; Johnson, Taylor T.: Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  6. Wu, Huihui; Lv, Deyun; Cui, Tengxiang; Hou, Gang; Watanabe, Masahiko; Kong, Weiqiang: SDLV: verification of steering angle safety for self-driving cars (2021)
  7. Yang, Pengfei; Li, Jianlin; Liu, Jiangchao; Huang, Cheng-Chao; Li, Renjue; Chen, Liqian; Huang, Xiaowei; Zhang, Lijun: Enhancing robustness verification for deep neural networks via symbolic propagation (2021)
  8. Zhao, Hengjun; Zeng, Xia; Chen, Taolue; Liu, Zhiming; Woodcock, Jim: Learning safe neural network controllers with barrier certificates (2021)
  9. Anderson, Ross; Huchette, Joey; Ma, Will; Tjandraatmadja, Christian; Vielma, Juan Pablo: Strong mixed-integer programming formulations for trained neural networks (2020)
  10. Bunel, Rudy; Turkaslan, Ilker; Torr, Philip H. S.; Kumar, M. Pawan; Lu, Jingyue; Kohli, Pushmeet: Branch and bound for piecewise linear neural network verification (2020)
  11. Edward Ayers, Francisco Eiras, Majd Hawasly, Iain Whiteside: PaRoT: A Practical Framework for Robust Deep NeuralNetwork Training (2020) arXiv
  12. Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson: NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems (2020) arXiv
  13. Kuwajima, Hiroshi; Yasuoka, Hirotoshi; Nakae, Toshihiro: Engineering problems in machine learning systems (2020)
  14. Wang, Lu; Zhang, Huan; Yi, Jinfeng; Hsieh, Cho-Jui; Jiang, Yuan: Spanning attack: reinforce black-box attacks with unlabeled data (2020)
  15. Wu, Min; Wicker, Matthew; Ruan, Wenjie; Huang, Xiaowei; Kwiatkowska, Marta: A game-based approximate verification of deep neural networks with provable guarantees (2020)