00:00 uh both yal andan will be presenting the
00:04 session hey my name is yal shapira and
00:08 together with me is aranov ner and today
00:10 we will present our paper de playing
00:11 robustness verification for few pixel
00:14 talks done under the supervision of dler
00:16 coin at the techon we start with an
00:19 example of a few pixel attack consider
00:22 this image it was clearly four but by
00:24 changing only three pixels we F the
00:26 neural network to classify it as nine in
00:29 contrast consider this image of the
00:31 digit two in this talk we will show you
00:33 how we formally proved that by changing
00:36 at most three pixels it is impossible to
00:38 fool the same newal network from before
00:40 to change classification from
00:43 two okay as most of you probably know
00:46 deploying has become a very useful tool
00:49 specifically in image classification
00:51 tasks unfortunately previous Studies
00:53 have shown it is vulnerable to aders
00:55 example attacks an aders example is a
00:58 slight perturbation of an image that
01:00 causes a network to
01:01 misclassify for example consider the
01:04 panda image on the left which is
01:06 correctly classified by some neural
01:07 network adding to it this little noise
01:10 which is undetectable by the human eye
01:12 makes the same network classified as a
01:15 confidence this weakness raises a great
01:18 concern regarding regarding safety and
01:20 reliability of deep learning renewal
01:24 networks to address these concerns
01:27 various Studies have shown methods to
01:28 formally prove robustness of ual
01:30 networks focusing on a property called
01:32 local robustness this property means
01:35 that no adval example could be found in
01:37 a given neighborhood of an image they
01:39 typically work with box neighborhoods
01:42 therefore we call them box robustness
01:44 verifiers their input is a newal network
01:47 an image and a box neighborhood contains
01:49 it expressed by a sequence of intervals
01:52 one for each pixels and the output is
01:54 whether the network is robust Lo Vel
01:56 example in this neighborhood or not and
02:00 we know that these kind of verifiers are
02:02 suitable for uh for proving robustness
02:04 against H attack models the change is
02:11 independently in our walk we focus on
02:13 different kind of attacks L zero attacks
02:16 given a positive integer T an adversary
02:20 goal is to find an adversarial example
02:22 by changing at most T pixels of the
02:24 image for example on the left there is a
02:27 pole and by changing a few dozens of
02:29 pixels is misclassified as traffic light
02:31 in the right there is a backpack which
02:33 is also misclassified by changes a few
02:38 pixels an important property of the L
02:40 zero neighborhoods is that they can be
02:42 represented as sequences of intervals
02:45 for example if T equals 1 the
02:48 corresponding l0 neighborhood of an
02:50 image with v pixels is all different
02:52 perturbations that change only one pixel
02:56 so for each such perturbation the
02:58 corresponding a sequence there is a
03:01 corresponding sequence of V intervals
03:04 each bounding the respective pixel value
03:07 if we change just one pixel then all
03:09 pixel values should be fixed but one and
03:11 we should let this pixel value range
03:13 over all possible values say between
03:16 zero and one since each sequence is
03:19 uniquely determined by the pixels we can
03:21 change we can think of each sequence as
03:24 the set of these pixels as you can see
03:26 in the slide this representation and
03:29 naturally extends to all values of T not
03:31 just T equals 1 and we will use it from
03:34 now on we can also learn from this
03:37 representation that in order to verify L
03:39 Zer robustness of an image with v pixels
03:42 we have to verify robustness of all of
03:47 subsets this representation as sequences
03:50 of intervals is important because we
03:52 because we can use it in existing box
03:54 robustness verifiers that you all talked
03:56 about earlier we can use this box
03:58 robustness verifier in order to suggest
04:00 a naive approach for solving the l0
04:03 robustness verification problem we can
04:05 simply iterate over all subsets of size
04:08 T in the image for each such subset we
04:11 can use an existing box robustness
04:13 verifier and on the respective interval
04:16 neighborhood as we explained in the
04:17 previous slide if all subsets are robust
04:20 then the image is robust for LZ Tech
04:22 with parameter T for example if I have
04:25 an image with five pixels 1 2 3 4 5 and
04:28 I want to verify l0 and its robustness
04:32 with respect to l0 attack with parameter
04:34 tals 3 so I will have to iterate over
04:37 all of its three sized subsets and
04:39 submit the corresponding neighborhood to
04:42 the existing box robust verifier as you
04:45 can see in the example in the
04:48 slide however this approach fails to
04:50 scale even for tals 3 H the reason for
04:53 that is that the number of iterations of
04:55 our native approach is V chose T when
04:58 can which can be exponential large in
05:00 the general case for example if you
05:02 consider an Mist image of 784 pixels and
05:05 the Box robust verifier that always
05:07 completes in 1 millisecond then for t
05:09 equal 3 our nav approach will terminate
05:11 after 22 hours for tals 4 180 days for
05:15 tal 5 77 years so clearly we must find a
05:20 solution our main Insight is that if a
05:24 subset sized K which is a number larger
05:26 than T is robust then all of its subsets
05:29 are robust specifically all of its
05:31 subsets of size T so with a single query
05:34 of an existing box robust verifier we
05:36 can verify multiple t uh t- sized
05:39 subsets for example if we verify that
05:42 the subset 1 2 3 4 is robust then all of
05:45 its subsets are robust specifically all
05:48 of its subsets size three so we we
05:51 proved robustness of four subsets using
05:54 using just one query to the existing box
05:56 robustness verifier so that means means
05:59 that we can significantly reduce the
06:01 number of queries to the existing box
06:03 robot verifier by submitting to it to a
06:09 neighborhood however this approach faces
06:11 many challenges and questions that arise
06:15 for example we must understand how we
06:17 choose the value of K how do we do that
06:19 and how to choose the sets and if we
06:22 verify sets of size K how do we know
06:23 we've covered all sets of Si since this
06:25 is our purpose and what happens if a set
06:28 is not robust now youal will answer
06:34 questions okay to overcome these
06:36 challenges we will use a combinatorial
06:38 object called covering designs given
06:41 three parameters m v which is greater
06:43 than equal to K which is greater than
06:45 equal to T covering covering designs
06:48 deals with finding a group of subsets of
06:50 size K of our universe which is the
06:53 numbers one to V minimal as possible
06:56 such that every subset of size T of our
06:58 universe is contain at least one of
07:00 these subset of size k for example if V
07:03 is equal to 5 our universe is the
07:05 numbers 1 2 3 4 5 and here we have
07:08 subset of size k equals 4 three of them
07:13 such that every subset of size two is
07:15 contain at least one of the subset of
07:17 size four therefore these three subset
07:19 of size fours forms a 5 42 covering
07:23 design finding minimal covering designs
07:26 for arbitrary parameters is a out
07:28 combinatorial problem
07:30 but luckily this subject has been well
07:33 studied okay now we'll see how C design
07:35 can help us assume that we have an image
07:38 with v equal 5 pixels and we want to
07:40 prove it is l0s for tal 2 also assume
07:44 that we decided to use covering with
07:46 size K1 equals 4 we will explain later
07:50 how the this decision is made so here we
07:53 have three subset of size four four in
07:57 the slide if all of these subset of size
07:59 four were robust we could conclude that
08:02 all of the subset of size T equals 2 is
08:04 also robust because these three subsets
08:06 covered them all so we run the Box
08:09 verifier on them first one is
08:12 robust the second one is not but it does
08:15 not mean it as a subset of size two
08:17 which is not robust so we make a
08:19 refinement step and cover it subset of
08:21 size two using subset of size K two
08:24 Which is less than can one let's say
08:26 three and now we run the Box very
08:29 robustness verifier on them the first
08:32 one is robust and again the second one
08:34 is not robust so we make another
08:36 refinement step and coverage subset of
08:38 size two using in this case subset of
08:41 two now run the Box verify on them the
08:45 first one is robust the second one is
08:47 robust and the third one is also robust
08:50 we go back up this subset is robust and
08:53 the last one is also
08:55 robust in this procedure we managed to
08:57 find a group of subsets robust subsets
09:00 such that every subset of size two is
09:02 contained in at least one of them
09:04 therefore we proved that the image is l
09:06 z robust for T equals
09:10 2 let's go back to our challenges and
09:13 the procedure from the previous slide
09:14 solves the Second Challenge we choose
09:17 the sets using covering designs and by
09:19 the way we choose them we know that we
09:21 cover all of the subset of size to what
09:23 happen if a set is not robust in this
09:26 case we make a refinement step if
09:28 possible if if its size is greater than
09:30 T and if it size is T we found a a
09:34 subset of T which is not robust and we
09:37 can terminate because we know that the
09:38 image is not LZ robust for
09:42 this regarding the first challenge which
09:45 case should we choose now we can
09:47 rephrase it more accurately at which
09:49 refinement strategy to choose meaning
09:52 which sizes K1 K2 and so on to choose in
09:57 strategy so we want to choose the
09:59 finding strategy efficient as possible
10:02 for that we use programming dynamic
10:04 programming and sampling and the
10:06 technical datas are are in our perer for
10:07 those of you are interested this method
10:10 basically considered the tradeoff uh
10:14 the consider the tradeoff when K is
10:18 small it is more likely that subset of
10:19 size K is robust but when K is large it
10:22 has more subset of size T that it covers
10:25 and we can prove them all at
10:31 the the two main parts that youve all
10:34 just described the cover and Designs
10:36 procedure and the method of sampling and
10:39 dynamic programming are the two
10:41 components of our contribution in the
10:43 paper and algorithm called kzone a
10:46 certification analyzer for L zero
10:48 neighborhoods we implemented kzone and
10:50 evaluated it for T from 1 to 5 on
10:53 several known image data sets such as
10:55 mnist and C4 10 and on several neural
10:57 networks convolutional and fully
10:59 connected and now we discuss these
11:01 results so in the table you can see the
11:04 our results for the mless data sets on
11:06 few selected networks H first we
11:08 consider the different values of T and
11:11 the number of subsets of size T that had
11:13 to be verified we can see here the
11:15 exponential growth of this number H for
11:18 tal 1 784 subsets had to be verified for
11:21 tal 3 it already becomes 80 million
11:24 subsets for tal 5 2.4 trillion subsets
11:28 so we see again the importance of
11:30 iterating through them all let's take a
11:32 look in on an experiment we did with a
11:34 convolution network and tals 3 here
11:37 again we had to verify 80 million
11:39 subsets we gave Kone kzone a timeout for
11:43 HMS we set a timeout of 30 minutes per
11:45 image and we gave it 100 images to go
11:48 through out of them 98 images were
11:51 correctly classified by the network and
11:53 out of them kzone determined that 87
11:56 were robust for a Tex with LZ Tex with
11:59 parameter t equal 3 11 images were non
12:02 robust and none of the images timed out
12:05 and in the last two columns you can see
12:07 the average execution time for robust
12:10 images and the average execution time
12:11 for non-rust images as you can see on
12:14 average it took alone to determine in
12:17 either case less less than a minute and
12:20 as we saw in our results no more than
12:23 few minutes generally you can also see
12:25 that it terminates faster in non-rust IM
12:29 than it is for robust images and it was
12:31 and it is something that was repeatedly
12:33 true mostly throughout our experiments
12:36 and now let's take a look on another
12:38 experiment which is more challenging the
12:40 case where T equals 5 in another
12:42 convolutional Network and here again we
12:44 had to verify 2.4 trillion subsets we
12:47 set there for a higher value of Time Out
12:50 300 minutes and gave kzone 10 images to
12:53 go through nine of them were correctly
12:55 classified by the network kzone
12:58 determined that five were robust three
13:00 were not robust and one did time out as
13:03 for as for the average execution time
13:06 you can see that for robust images it
13:08 took a Zone much longer than the
13:09 previous case where tal 3 over an hour
13:12 on average and few hours generally per
13:15 image and for the non robust images it
13:18 is slower than before the case where tal
13:21 3 but much faster than for the robust
13:23 images only few minutes on
13:26 average to conclude we present here
13:29 kzone the first sound and complete L
13:31 zero robustness analyzer for neural
13:33 networks as far as we know typically as
13:36 we saw in the previous slide kzone
13:37 completes within few minutes on our most
13:40 challenging instances tals 5 as we saw
13:43 kzone completes within few hours H we
13:46 put here a link to GitHub and we will
13:48 upload our code there soon so stay
13:57 you uh so we're just at time so I think
14:00 this uh time for one or two quick
14:02 questions uh uh please just introduce
14:04 yourself hi thank you for the talk I'm
14:06 theora I'm from n us so I was wondering
14:09 um for l0 you have this few pixels
14:13 attacks do you have any idea of what
14:15 that means for an image like for example
14:17 how many pixels do does it does this
14:20 make sense in the sense of like visually
14:22 imperceptible changes and if you and
14:25 this is the first question the second
14:26 question have you considered other types
14:30 distances do do you mean for the first
14:32 questions like how much is how much like
14:35 what happens in reality like how how how
14:38 many pixels you have to to change to to
14:41 really full a network yeah so for
14:43 example for L Infinity there are some uh
14:46 studies that tell you that like 0.3 for
14:48 mest is close to what would be
14:50 considered human imperceptible right
14:53 visually imperceptible so I'm just
14:55 wondering for this case for l0 do you
14:58 have such a metric that says hey five
15:00 pixels for amnest is enough for a human
15:03 to also distinguish that this is a four
15:07 nine we don't really like have this
15:10 number like how how many do you need but
15:19 and in our first example you can see the
15:22 the three uh pixels with changed and
15:25 they cause the network to change it to
15:27 nine so it's really you can see that it
15:29 really closes the the upper bridge
15:31 between this we can see why it it would
15:34 become a nine but we don't have like a
15:36 bench mark that says I need six pixels
15:39 and then I I guess it depends on the
15:40 image as well okay and for the second
15:43 question have you considered other
15:45 distances and how would that would this
15:47 approach work for other types of uh
15:50 distances I think like for the the the
15:55 the the existing box Rob bance verifier
15:57 usually work for like L INF inity
15:59 distances and uh this approach is is is
16:03 really used it's the combinatoric
16:05 structure of the L zero H distance then
16:09 you have number of pixels that change
16:11 other distances usually say well you can
16:14 the distance is not something that has
16:17 this combinatorial structure so I don't
16:20 think it will apply to other kind of
16:22 distance thank you right uh one last
16:24 question from here hi I'm sorry again
16:29 look I mean the question is interesting
16:30 you're phrasing it as a combinatorial
16:32 question right have you looked at the
16:35 geometry of this question which is if I
16:38 remove one pixel from the set how much
16:42 is the distance going to change how much
16:43 is the distance going to change right if
16:46 you ask geometric questions as to the
16:47 size of changes you might make this
16:50 procedure a lot more efficient right
16:51 because you're not doing it
16:52 combinatorially searching for the option
16:54 like the number of combinations you're
16:56 searching geometrically so have you
16:58 thought about this this approach uh at
17:03 approach um this is interesting I agree
17:06 um we basically uh don't treat all the
17:10 pixels the same we don't care which
17:11 pixel we change which is not the best we
17:14 can improve that um and I guess we can
17:18 choose a covering in a way that pixel
17:22 which are important in the image not in
17:24 the background or something will appear
17:26 less and and I guess it can improve the
17:29 results got it thanks wonderful all
17:32 right thank you so idea for another
17:34 paper all right um thank you everyone
17:36 for coming um and I think there's a a
17:38 coffee break at this point
