Safety Verification of Deep Neural Networks View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2017-07-13

AUTHORS

Xiaowei Huang , Marta Kwiatkowska , Sen Wang , Min Wu

ABSTRACT

Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on safety of image classification decisions with respect to image manipulations, such as scratches or changes to camera angle or lighting conditions that would result in the same class being assigned by a human, and define safety for an individual decision in terms of invariance of the classification within a small neighbourhood of the original image. We enable exhaustive search of the region by employing discretisation, and propagate the analysis layer by layer. Our method works directly with the network code and, in contrast to existing methods, can guarantee that adversarial examples, if they exist, are found for the given region and family of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples and estimate network robustness. More... »

PAGES

3-29

Book

TITLE

Computer Aided Verification

ISBN

978-3-319-63386-2
978-3-319-63387-9

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-63387-9_1

DOI

http://dx.doi.org/10.1007/978-3-319-63387-9_1

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1090657161


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Huang", 
        "givenName": "Xiaowei", 
        "id": "sg:person.013276065116.65", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013276065116.65"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kwiatkowska", 
        "givenName": "Marta", 
        "id": "sg:person.011375012273.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Wang", 
        "givenName": "Sen", 
        "id": "sg:person.016010752177.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016010752177.39"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Wu", 
        "givenName": "Min", 
        "id": "sg:person.014210564476.51", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014210564476.51"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2017-07-13", 
    "datePublishedReg": "2017-07-13", 
    "description": "Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on safety of image classification decisions with respect to image manipulations, such as scratches or changes to camera angle or lighting conditions that would result in the same class being assigned by a human, and define safety for an individual decision in terms of invariance of the classification within a small neighbourhood of the original image. We enable exhaustive search of the region by employing discretisation, and propagate the analysis layer by layer. Our method works directly with the network code and, in contrast to existing methods, can guarantee that adversarial examples, if they exist, are found for the given region and family of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples and estimate network robustness.", 
    "editor": [
      {
        "familyName": "Majumdar", 
        "givenName": "Rupak", 
        "type": "Person"
      }, 
      {
        "familyName": "Kun\u010dak", 
        "givenName": "Viktor", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-63387-9_1", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-63386-2", 
        "978-3-319-63387-9"
      ], 
      "name": "Computer Aided Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "deep neural networks", 
      "Satisfiability Modulo Theories", 
      "adversarial examples", 
      "neural network", 
      "feed-forward multi-layer neural network", 
      "multi-layer neural network", 
      "self-driving cars", 
      "deep learning network", 
      "verification framework", 
      "perception module", 
      "image classification", 
      "input image", 
      "art networks", 
      "analysis layer", 
      "network codes", 
      "human testers", 
      "original image", 
      "adversarial perturbations", 
      "image manipulation", 
      "Modulo Theories", 
      "learning network", 
      "end controller", 
      "terms of invariance", 
      "safety verification", 
      "exhaustive search", 
      "camera angles", 
      "classification decisions", 
      "impressive experimental results", 
      "network robustness", 
      "network", 
      "experimental results", 
      "small neighborhood", 
      "same class", 
      "images", 
      "classification", 
      "verification", 
      "robustness", 
      "scratch", 
      "example", 
      "controller", 
      "code", 
      "module", 
      "decisions", 
      "technique", 
      "framework", 
      "search", 
      "applications", 
      "car", 
      "individual decisions", 
      "method", 
      "manipulation", 
      "Z3", 
      "neighborhood", 
      "discretisation", 
      "minimal changes", 
      "safety", 
      "class", 
      "tester", 
      "respect", 
      "potential applications", 
      "terms", 
      "invariance", 
      "layer", 
      "novel", 
      "results", 
      "end", 
      "concern", 
      "state", 
      "humans", 
      "theory", 
      "region", 
      "angle", 
      "changes", 
      "conditions", 
      "perturbations", 
      "contrast", 
      "family", 
      "image classification decisions", 
      "family of manipulations", 
      "estimate network robustness"
    ], 
    "name": "Safety Verification of Deep Neural Networks", 
    "pagination": "3-29", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1090657161"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-63387-9_1"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-63387-9_1", 
      "https://app.dimensions.ai/details/publication/pub.1090657161"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:09", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_413.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-63387-9_1"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63387-9_1'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63387-9_1'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63387-9_1'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-63387-9_1'


 

This table displays all metadata directly associated to this object as RDF triples.

166 TRIPLES      23 PREDICATES      105 URIs      98 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-63387-9_1 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N729ed899d8c3440f88d56f86116e49d9
4 schema:datePublished 2017-07-13
5 schema:datePublishedReg 2017-07-13
6 schema:description Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on safety of image classification decisions with respect to image manipulations, such as scratches or changes to camera angle or lighting conditions that would result in the same class being assigned by a human, and define safety for an individual decision in terms of invariance of the classification within a small neighbourhood of the original image. We enable exhaustive search of the region by employing discretisation, and propagate the analysis layer by layer. Our method works directly with the network code and, in contrast to existing methods, can guarantee that adversarial examples, if they exist, are found for the given region and family of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples and estimate network robustness.
7 schema:editor N2831710af14d41f69a2badea61f64d99
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N660c5c55c7c94ba7a1549e44ff2dd52f
12 schema:keywords Modulo Theories
13 Satisfiability Modulo Theories
14 Z3
15 adversarial examples
16 adversarial perturbations
17 analysis layer
18 angle
19 applications
20 art networks
21 camera angles
22 car
23 changes
24 class
25 classification
26 classification decisions
27 code
28 concern
29 conditions
30 contrast
31 controller
32 decisions
33 deep learning network
34 deep neural networks
35 discretisation
36 end
37 end controller
38 estimate network robustness
39 example
40 exhaustive search
41 experimental results
42 family
43 family of manipulations
44 feed-forward multi-layer neural network
45 framework
46 human testers
47 humans
48 image classification
49 image classification decisions
50 image manipulation
51 images
52 impressive experimental results
53 individual decisions
54 input image
55 invariance
56 layer
57 learning network
58 manipulation
59 method
60 minimal changes
61 module
62 multi-layer neural network
63 neighborhood
64 network
65 network codes
66 network robustness
67 neural network
68 novel
69 original image
70 perception module
71 perturbations
72 potential applications
73 region
74 respect
75 results
76 robustness
77 safety
78 safety verification
79 same class
80 scratch
81 search
82 self-driving cars
83 small neighborhood
84 state
85 technique
86 terms
87 terms of invariance
88 tester
89 theory
90 verification
91 verification framework
92 schema:name Safety Verification of Deep Neural Networks
93 schema:pagination 3-29
94 schema:productId N4a9f9d9c729b4c6a96aa9b42f2be65e1
95 N5f38e0b3ee8d45858138beace1ba3a36
96 schema:publisher N1c6d3847431647d99ab5fb74118f94bf
97 schema:sameAs https://app.dimensions.ai/details/publication/pub.1090657161
98 https://doi.org/10.1007/978-3-319-63387-9_1
99 schema:sdDatePublished 2021-12-01T20:09
100 schema:sdLicense https://scigraph.springernature.com/explorer/license/
101 schema:sdPublisher Nbb272ffb61b4403d96f2c83fdc6bb67a
102 schema:url https://doi.org/10.1007/978-3-319-63387-9_1
103 sgo:license sg:explorer/license/
104 sgo:sdDataset chapters
105 rdf:type schema:Chapter
106 N11d5513176154f278a90d6191a452de8 schema:familyName Majumdar
107 schema:givenName Rupak
108 rdf:type schema:Person
109 N1c6d3847431647d99ab5fb74118f94bf schema:name Springer Nature
110 rdf:type schema:Organisation
111 N2831710af14d41f69a2badea61f64d99 rdf:first N11d5513176154f278a90d6191a452de8
112 rdf:rest N3cddcae8214342bcb9b694454cbdaacd
113 N3cddcae8214342bcb9b694454cbdaacd rdf:first N55817f549fd24fbfa79588c0da38db67
114 rdf:rest rdf:nil
115 N4a9f9d9c729b4c6a96aa9b42f2be65e1 schema:name doi
116 schema:value 10.1007/978-3-319-63387-9_1
117 rdf:type schema:PropertyValue
118 N55817f549fd24fbfa79588c0da38db67 schema:familyName Kunčak
119 schema:givenName Viktor
120 rdf:type schema:Person
121 N5f38e0b3ee8d45858138beace1ba3a36 schema:name dimensions_id
122 schema:value pub.1090657161
123 rdf:type schema:PropertyValue
124 N660c5c55c7c94ba7a1549e44ff2dd52f schema:isbn 978-3-319-63386-2
125 978-3-319-63387-9
126 schema:name Computer Aided Verification
127 rdf:type schema:Book
128 N665c5b2deb514b028a0b054948035aa7 rdf:first sg:person.014210564476.51
129 rdf:rest rdf:nil
130 N729ed899d8c3440f88d56f86116e49d9 rdf:first sg:person.013276065116.65
131 rdf:rest N76e15e8f33c348a4bd719d16399cf128
132 N76e15e8f33c348a4bd719d16399cf128 rdf:first sg:person.011375012273.39
133 rdf:rest Nccabb90eeafe4414b0fbc1f1b231d147
134 Nbb272ffb61b4403d96f2c83fdc6bb67a schema:name Springer Nature - SN SciGraph project
135 rdf:type schema:Organization
136 Nccabb90eeafe4414b0fbc1f1b231d147 rdf:first sg:person.016010752177.39
137 rdf:rest N665c5b2deb514b028a0b054948035aa7
138 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
139 schema:name Information and Computing Sciences
140 rdf:type schema:DefinedTerm
141 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
142 schema:name Artificial Intelligence and Image Processing
143 rdf:type schema:DefinedTerm
144 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
145 schema:familyName Kwiatkowska
146 schema:givenName Marta
147 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
148 rdf:type schema:Person
149 sg:person.013276065116.65 schema:affiliation grid-institutes:grid.4991.5
150 schema:familyName Huang
151 schema:givenName Xiaowei
152 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013276065116.65
153 rdf:type schema:Person
154 sg:person.014210564476.51 schema:affiliation grid-institutes:grid.4991.5
155 schema:familyName Wu
156 schema:givenName Min
157 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014210564476.51
158 rdf:type schema:Person
159 sg:person.016010752177.39 schema:affiliation grid-institutes:grid.4991.5
160 schema:familyName Wang
161 schema:givenName Sen
162 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016010752177.39
163 rdf:type schema:Person
164 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
165 schema:name Department of Computer Science, University of Oxford, Oxford, UK
166 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...