Skip to content

Formal Specification for Deep Neural Networks

Authors: Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, Xiangyu Yue

Published: 2018 (Conference Paper)

Source: Lecture Notes in Computer Science

Algorithm: DNN formal specification

DOI: 10.1007/978-3-030-01090-4_2

Summary

Surveys what it means to specify properties of deep neural networks for verification, moving the discussion beyond solver mechanics to the quality of the property being checked. It is useful for thinking about robustness, safety envelopes, and environment assumptions in learning-enabled systems.

Abstract

The increasing use of deep neural networks in a variety of applications, including some safety-critical ones, has brought renewed interest in the topic of verification of neural networks. However, verification is most meaningful when performed with high-quality formal specifications. In this paper, we survey the landscape of formal specification for deep neural networks, and discuss the opportunities and challenges for formal methods for this domain.

Primary

Paper people.eecs.berkeley.edu

Standard

DOI 10.1007/978-3-030-01090-4_2

Tags

  • Formal methods

  • Neural network verification

  • Specifications

  • Deep learning safety

  • Autonomous systems

  • Testing