Abstrakt. Djupa neurala nätverk har uppnått imponerande experimentella resultat i bildklassificering, men kan överraskande vara instabil med avseende på motstående perturbationer, det vill säga minimala förändringar i indatabilden som orsakar nätverket att felklassificera det. Med potentiella tillämpningar, inklusive perception moduler och end-to-end styrenheter för självkörande bilar, väcker detta farhågor om deras säkerhet. Vi utvecklar en ny automatiserad verifieringsram för feed-forward flerlagers neurala nätverk baserade på tillfredsställande Modulo Theory (SMT). Vi fokuserar på säkerhet i bildklassificeringsbeslut med avseende på bildmanipulationer, såsom repor eller förändringar i kameravinkel eller ljusförhållanden som skulle resultera i att samma klass tilldelas av en människa, och definierar säkerhet för ett enskilt beslut när det gäller variation av klassifikationen inom ett litet område av den ursprungliga bilden. Vi möjliggör en omfattande sökning i regionen genom att använda diskretisering och sprida analysskiktet efter lager. Vår metod fungerar direkt med nätverkskoden och kan, i motsats till befintliga metoder, garantera att kontradiktoriska exempel, om de finns, hittas för den givna regionen och familjen av manipulationer. Om det finns kontradiktoriska exempel kan de visas för testare och/eller användas för att finjustera nätverket. Vi implementerar teknikerna med hjälp av Z3 och utvärderar dem på toppmoderna nätverk, inklusive legaliserade och djupt lärande nätverk. Vi jämför också med befintliga tekniker för att söka efter kontradiktoriska exempel och uppskatta nätverkets robusthet.
När det t.ex. gäller testning och verifiering för NN utvecklas i REF en ram för verifiering baserad på tillfredsställande Modulo Theory (SMT) för flerskiktsbaserade NN:er (feed-forward multi-layer).
Safety Verification of Deep Neural Networks
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science', 'Mathematics']}