Formal verification of deep neural networks

This paper introduces a method for the formal verification of neural networks using a Satisfiability Modulo Theories (SMT) solver. This approach enables the mathematical validation of specific neural network properties, enhancing their predictability. We propose a method for simplifying a neural net...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2024
1. Verfasser:	Panchuk, B.O.
Format:	Artikel
Sprache:	Ukrainian
Veröffentlicht:	PROBLEMS IN PROGRAMMING 2024
Schlagworte:	neural networks formal verification satisfiability modulo theories constraints satisfaction intrusion detection systems network traffic analysis UDC 004.415.52 004.89 004.492
Online Zugang:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/644
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Problems in programming
Завантажити файл:

Institution

Problems in programming

id	pp_isofts_kiev_ua-article-644
record_format	ojs
resource_txt_mv	ppisoftskievua/ef/4f80b65e03274e441fb63b48348f13ef.pdf
spelling	pp_isofts_kiev_ua-article-6442025-02-15T13:39:41Z Formal verification of deep neural networks Формальна верифікація нейронних мереж глибокого навчання Panchuk, B.O. neural networks; formal verification; satisfiability modulo theories; constraints satisfaction; intrusion detection systems; network traffic analysis UDC 004.415.52, 004.89, 004.492 нейронні мережі; формальна верифікація; satisfiability modulo theories; задача виконуваності обмежень; системи виявлення вторгнень; аналіз мережевих даних УДК 004.415.52, 004.89, 004.492 This paper introduces a method for the formal verification of neural networks using a Satisfiability Modulo Theories (SMT) solver. This approach enables the mathematical validation of specific neural network properties, enhancing their predictability. We propose a method for simplifying a neural network’s computational graph within certain input space regions. This is achieved by replacing neurons’ piecewise-linear activation functions with a subset of their linear segments. This optimization hypothesizes a simpler interpretation of a neural network over limited input data ranges. The simplified interpretation is derived from the incremental simplification of the neural network graph, achieved by solving local SMT tasks on a neuron-by-neuron basis. This optimization significantly speeds up the verification algorithm compared to solving a single SMT task over the entire unoptimized network graph. The method is applicable to any deep neural networks with piecewise-linear activation functions. The approach’s effectiveness was demonstrated by automatically verifying a network traffic classifier specializing in botnet activity detection. The classification model was tested for robustness against adversarial attacks, where attackers attempt to evade detection by introducing specially crafted disturbances into the network data. The verification procedure was conducted over regions in the feature-space near the classifier’s decision boundary. The results contribute to the prospects for more active application of artificial intelligence models in cybersecurity, where result predictability and interpretability are crucial. Additionally, the neuron - wise simplification technique proposed is a promising direction for further development in neural network verification.Prombles in programming 2024; 2-3: 253-262 У цій роботі представлено спосіб формальної верифікації властивостей нейронних мереж за допомогою "Satisfiability Modulo Theories" (SMT) розв’язувача. Цей підхід дозволяє математично доводити специфічні властивості нейромереж, що робить їх більш передбачуваними. У процесі дослідження було розроблено новий метод спрощення обчислювального графа нейромережі над певними регіонами вхідного простору, шляхом заміни кусково-лінійних функцій активації нейронів на підмножину їхніх лінійних сегментів. Запропонований спосіб оптимізації ґрунтується на гіпотезі існування значно простішої інтерпретації нейромережі на обмежених діапазонах вхідних даних. У роботі пропонується спосіб отримання такої спрощеної інтерпретації через понейронне розв’язування локальних SMT-задач з інкрементальним спрощенням графу нейромережі. Ця оптимізація дозволила значно прискорити алгоритм верифікації порівняно з розв’язанням єдиної SMT-задачі над суцільним неоптимізованим графом мережі. Описаний метод можна застосовувати для верифікації довільних повнозв’язних нейромереж глибокого навчання з кусково-лінійними функціями активації. Для практичної демонстрації результатів створений метод верифікації було застосовано для перевірки роботи нейромережі-аналізатора мережевого трафіку, метою якого є виявлення активності ботнетів. Модель класифікації перевірялась на стійкість до «змагальних атак» – спроб зловмисника уникнути виявлення, вносячи спеціальні збурення в дані, що класифікуються. В роботі було проведено автоматизовану перевірку коректності роботи класифікатора над сумнівними регіонами даних, які розміщені біля межі ухвалення рішень. Отримані результати роблять важливий внесок у розвиток застосування штучного інтелекту в царині кібербезпеки, де інтерпретація та передбачуваність є критично необхідними. Крім того, запропонований метод понейронного спрощення є перспективним напрямком для подальшого розвитку верифікації нейронних мереж.Prombles in programming 2024; 2-3: 253-262 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2024-12-17 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/644 10.15407/pp2024.02-03.253 PROBLEMS IN PROGRAMMING; No 2-3 (2024); 253-262 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2024); 253-262 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2024); 253-262 1727-4907 10.15407/pp2024.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/644/696 Copyright (c) 2024 PROBLEMS IN PROGRAMMING
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2025-02-15T13:39:41Z
collection	OJS
language	Ukrainian
topic	neural networks formal verification satisfiability modulo theories constraints satisfaction intrusion detection systems network traffic analysis UDC 004.415.52 004.89 004.492
spellingShingle	neural networks formal verification satisfiability modulo theories constraints satisfaction intrusion detection systems network traffic analysis UDC 004.415.52 004.89 004.492 Panchuk, B.O. Formal verification of deep neural networks
topic_facet	neural networks formal verification satisfiability modulo theories constraints satisfaction intrusion detection systems network traffic analysis UDC 004.415.52 004.89 004.492 нейронні мережі формальна верифікація satisfiability modulo theories задача виконуваності обмежень системи виявлення вторгнень аналіз мережевих даних УДК 004.415.52 004.89 004.492
format	Article
author	Panchuk, B.O.
author_facet	Panchuk, B.O.
author_sort	Panchuk, B.O.
title	Formal verification of deep neural networks
title_short	Formal verification of deep neural networks
title_full	Formal verification of deep neural networks
title_fullStr	Formal verification of deep neural networks
title_full_unstemmed	Formal verification of deep neural networks
title_sort	formal verification of deep neural networks
title_alt	Формальна верифікація нейронних мереж глибокого навчання
description	This paper introduces a method for the formal verification of neural networks using a Satisfiability Modulo Theories (SMT) solver. This approach enables the mathematical validation of specific neural network properties, enhancing their predictability. We propose a method for simplifying a neural network’s computational graph within certain input space regions. This is achieved by replacing neurons’ piecewise-linear activation functions with a subset of their linear segments. This optimization hypothesizes a simpler interpretation of a neural network over limited input data ranges. The simplified interpretation is derived from the incremental simplification of the neural network graph, achieved by solving local SMT tasks on a neuron-by-neuron basis. This optimization significantly speeds up the verification algorithm compared to solving a single SMT task over the entire unoptimized network graph. The method is applicable to any deep neural networks with piecewise-linear activation functions. The approach’s effectiveness was demonstrated by automatically verifying a network traffic classifier specializing in botnet activity detection. The classification model was tested for robustness against adversarial attacks, where attackers attempt to evade detection by introducing specially crafted disturbances into the network data. The verification procedure was conducted over regions in the feature-space near the classifier’s decision boundary. The results contribute to the prospects for more active application of artificial intelligence models in cybersecurity, where result predictability and interpretability are crucial. Additionally, the neuron - wise simplification technique proposed is a promising direction for further development in neural network verification.Prombles in programming 2024; 2-3: 253-262
publisher	PROBLEMS IN PROGRAMMING
publishDate	2024
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/644
work_keys_str_mv	AT panchukbo formalverificationofdeepneuralnetworks AT panchukbo formalʹnaverifíkacíânejronnihmerežglibokogonavčannâ
first_indexed	2025-07-17T09:52:41Z
last_indexed	2025-07-17T09:52:41Z
_version_	1850410100190085120
fulltext	253 Машинне навчання та нейронні мережі УДК 004.415.52, 004.89, 004.492 http://doi.org/10.15407/pp2024.02-03.253 Б.О. Панчук ФОРМАЛЬНА ВЕРИФІКАЦІЯ НЕЙРОННИХ МЕРЕЖ ГЛИБОКОГО НАВЧАННЯ У цій роботі представлено спосіб формальної верифікації властивостей нейронних мереж за допомо- гою “Satisfiability Modulo Theories” (SMT) розв’язувача. Цей підхід дозволяє математично доводити специфічні властивості нейромереж, що робить їх більш передбачуваними. У процесі дослідження було розроблено новий метод спрощення обчислювального графа нейромережі над певними регіонами вхідного простору, шляхом заміни кусково-лінійних функцій активації нейронів на підмножину їхніх лінійних сегментів. Запропонований спосіб оптимізації ґрунтується на гіпотезі існування значно про- стішої інтерпретації нейромережі на обмежених діапазонах вхідних даних. У роботі пропонується спо- сіб отримання такої спрощеної інтерпретації через понейронне розв’язування локальних SMT-задач з інкрементальним спрощенням графу нейромережі. Ця оптимізація дозволила значно прискорити алго- ритм верифікації порівняно з розв’язанням єдиної SMT-задачі над суцільним неоптимізованим графом мережі. Описаний метод можна застосовувати для верифікації довільних повнозв’язних нейромереж глибокого навчання з кусково-лінійними функціями активації. Для практичної демонстрації результатів створений метод верифікації було застосовано для перевірки роботи нейромережі-аналізатора мережевого трафіку, метою якого є виявлення активності ботнетів. Модель класифікації перевірялась на стійкість до «змагальних атак» – спроб зловмисника уникнути виявлення, вносячи спеціальні збурення в дані, що класифікуються. В роботі було проведено автома- тизовану перевірку коректності роботи класифікатора над сумнівними регіонами даних, які розміщені біля межі ухвалення рішень. Отримані результати роблять важливий внесок у розвиток застосування штучного інтелекту в царині кібербезпеки, де інтерпретація та передбачуваність є критично необхід- ними. Крім того, запропонований метод понейронного спрощення є перспективним напрямком для подальшого розвитку верифікації нейронних мереж. Ключові слова: нейронні мережі, формальна верифікація, satisfiability modulo theories, задача викону- ваності обмежень, системи виявлення вторгнень, аналіз мережевих даних. B.O. Panchuk FORMAL VERIFICATION OF DEEP NEURAL NETWORKS This paper introduces a method for the formal verification of neural networks using a Satisfiability Modulo Theories (SMT) solver. This approach enables the mathematical validation of specific neural network prop- erties, enhancing their predictability. We propose a method for simplifying a neural network’s computational graph within certain input space regions. This is achieved by replacing neurons’ piecewise -linear activation functions with a subset of their linear segments. This optimization hypothesizes a simpler interpretation of a neural network over limited input data ranges. The simplified interpretation is derived from the incremental simplification of the neural network graph, achieved by solving local SMT tasks on a neuron-by-neuron basis. This optimization significantly speeds up the verification algorithm compared to solving a single SMT task over the entire unoptimized network graph. The method is applicable to any deep neural networks with piece- wise-linear activation functions. The approach’s effectiveness was demonstrated by automatically verifying a network traffic classifier spe- cializing in botnet activity detection. The classification model was tested for robustness against adversarial attacks, where attackers attempt to evade detection by introducing specially crafted disturbances into the net- work data. The verification procedure was conducted over regions in the feature-space near the classifier’s decision boundary. The results contribute to the prospects for more active application of artificial intelligence models in cybersecurity, where result predictability and interpretability are crucial. Additionally, the neuron - wise simplification technique proposed is a promising direction for further development in neural network verification. Key words: neural networks, formal verification, satisfiability modulo theories, constraints satisfaction, in- trusion detection systems, network traffic analysis. © Б.О. Панчук, 2024 ISSN 1727-4907. Проблеми програмування. 2024. №2-3 254 Машинне навчання та нейронні мережі Вступ На сьогодні написано чимало робіт із застосування ШІ у сфері кібербезпеки. Зокрема, моделі ШІ неодноразово викорис- товувалися для аналізу інтернет трафіку з метою виявлення мережевих атак (IDS, intrusion detection system). Значно менше уваги приділено стійкості таких моделей до так званих «змагальних атак». Такі атаки передбачають спробу ухилення від вияв- лення шляхом збурення вхідних даних з ме- тою спричинення помилкової класифікації, водночас залишаючи дані правдоподіб- ними. В роботах, де зазвичай ця проблема розглядається, використовуються класичні емпіричні методи статистичної оцінки стій- кості моделей на штучно згенерованих да- них. Недоліком такого підходу, є те, що в результаті не надається жодних абсолют- них гарантій. Відповідно поведінка IDS за- лишається непередбачуваною на даних, які не присутні в тестовій вибірці, що є ваго- мим контраргументом до використання ШІ в цій сфері. Нещодавно почав набувати розви- тку підхід «формальної верифікації» ней- ронних мереж, за якого вимоги задаються формально у формі обмежень, що наклада- ються на входи та виходи моделі. Після цього відбувається автоматична математи- чна перевірка виконання обмежень мо- деллю на всіх можливих вхідних даних. Та- кий підхід принципово відрізняється від пе- ревірки результатів для окремих штучно- згенерованих прикладів, адже отримані ре- зультати надійності розповсюджуються на цілий спектр наборів вхідних даних. Мета статті Першочерговою метою цієї роботи було створення методу для отримання ма- тематичних гарантій cтійкості глибоких нейронних мереж-класифікаторів. Отрима- ний метод верифікації, може бути застосо- ваний для довільних нейромереж прямого розповсюдження з більше, ніж одним при- хованим шаром та кусково-лінійною функ- цією активації прихованих нейронів. Метою експериментальної частини роботи була демонстрація застосування да- ного методу для верифікації попередньо на- вченої нейромережі, що спеціалізується на класифікації мережевих даних з метою ви- явлення шкідливих дій. Сам алгоритм має бути оптимізовано з метою уникнення ком- бінаторного вибуху слкладності при аналізі розв’язувачем графу нейромережі. Методи верифікації властивостей моделей Найбільш поширеним методом є ем- піричні оцінки характеристик моделі. Пере- вірка даних властивостей здійснюється шляхом отримання результатів роботи мо- делі над фіксованою множиною точок з вхі- дного простору. Після чого порівнюють отримані результати із заздалегідь відо- мими та підраховуються статистичні оці- нки їх схожості. Класичними показниками при такій оцінці є, точність, влучність, час- тка позитивно-негативних результатів, від- соток помилок над множиною змагальних прикладів і т.д. Як і випливає з назви, такі властивості не надають жодних гарантій якості моделі, а лише показують статистику роботи моделі на доступній вибірці. Інший метод верифікації є перевірка виконання глобальних обмежень (constraints satisfaction). Такі властивості визначаються у формі системи жорстких обмежень накладених на простір вхідних та вихідних даних моделі. А верифікація здій- снюється не на фіксованому наборі вхідних даних, а на повному теоретично можли- вому підпросторі з простору входів. Прик- ладом такої властивості у випадку багато- класової класифікації може бути певна умова. А саме: якщо модель класифікації вже віднесла певний об’єкт до якогось класу, то показник впевненості для всіх ін- ших класів має буде нижчим за певний по- ріг. Метод, який розглядається в даній роботі – це верифікація локальної надійно- сті (robustness). Якщо модель є локально на- дійною (стійкою), очікується, що за умови, коли для певного елементу з області входу модель продукує коректний результат, то під час внесення відносно незначних пер- 255 Машинне навчання та нейронні мережі турбацій в значення ознак даного вхідного елементу, результат змінюється лише в очі- куваних межах. Наприклад, у випадку за- дачі класифікації, обидві – оригінальна та змінена точки мають бути віднесені мо- деллю до однакового класу. Ця властивість часто розглядається в контексті стійкості моделі до змагальних атак, однак може бути розширена до перевірки узагальнюю- чих властивостей моделі щодо довільних збурень вхідних даних в допустимих ме- жах. У роботі [1] наводяться 4 типи класів надійності в порядку посилення їхніх умов та обмежень: 1. Надійність класифікації, що передбачає збереження класу для всіх елементів з околу точки з простору вхідних даних. 2. Стандартна надійність полягає в тому, що для околу вхідної то- чки вихідне значення моделі ва- ріюватиметься також у певному околі. 3. Надійність Ліпшица вирізня- ється тим, що під час внесення змін у значення ознак вхідного елементу, вихід змінюється про- порційно. 4. Жорстка надійність класифіка- ції передбачає, що в околі вхідної точки значення на виході класи- фікатора для коректного класу буде вище певного порогу. За реалізацією методи верифікації можна розділити на п’ять наступних класів. Емпіричне тестування. Найпрості- ший клас методів, суть якого - перевірка ре- зультатів виходів моделі на множині зазда- легідь відомих вхідних елементів. Тестова множина може бути отримана разом із нав- чальним набором даних, або згенерована через тривіальні методи розширення даних (як-от деформації, накладання випадкових шумів тощо). До цього класу належать й інші класичні методи такі, як фазинг [2] чи тестування на основі покриття [3]. Пошук контрприкладів. У даному класі різними евристичними методами здійснюється пошук правдоподібних вхід- них елементів, для яких модель порушує властивості, що перевіряються. Одним із класичних способів є перетворення почат- кових вірно класифікованих елементів вхі- дної вибірки на “змагальні приклади” за до- помогою градієнтних методів (наприклад, “методом швидкого градієнту” (FGSM) [4]). Даний клас методів однак не обґрунто- вує стійкості моделі, а лише може виявити її вразливість. Рішення задачі оптимізації. Якщо модель можна звести до системи лінійних рівнянь та нерівностей, то для верифікації можна застосувати методи лінійного чи змішаного цілочислового програмування. Слід зауважити однак, що через наявність нелінійних функцій активації нейронів, як правило, неможливо застосувати даний клас методів до нейронних мереж “як-є”. Відповідно їх зазвичай використовують у комбінації з іншими підходами, такими як застосування SMT (Satisfiability Modulo Theories) розв’язувача [5][6]. Формування абстрактної інтерп- ретації моделі. Цей метод зазвичай допов- нює інші. Його суть у перебудові структури нейронної мережі, що розглядається як се- мантично схожа, але простіша [7]. Резуль- туюча модель є під- або над- апроксима- цією оригінальної. Мета такої операції – спрощення обчислювальної складності у подальшому доведенні виконання (чи пору- шення), накладених обмежень іншими ме- тодами. Очікується, що з виявлення пору- шення обмеження для підапроксимованої моделі, випливає порушення даного обме- ження і для оригінальної. Водночас дове- дення стійкості підапроксимованої моделі, не гарантує стійкості оригінальної. У випа- дку надапроксимації все з точністю до на- впаки. Доведення за допомогою SMT – розв’язувача. В даному методі обчислюва- льний граф моделі представляється у ви- гляді SMT формули. Далі на входи та ви- ходи моделі накладаються певні обме- ження, після чого SMT-розв’язувач дово- дить або спростовує їх виконуваність. За- звичай цей метод вимагає попередньої ап- роксимації всіх нелінійних функцій актива- ції нейронів через лінійні сегменти. В даній роботі застосовується комбі- нація методу абстрактної інтерпретації та 256 Машинне навчання та нейронні мережі доведення властивостей моделі за допомо- гою SMT розв’язувача (Microsoft Z3 [8]). 1. Постановка задачі верифікації в околі точки Ми продемонструємо автоматиза- цію перевірки локальної стійкості (надійно- сті) класифікатора мережевого трафіку ме- тодом верифікації у відносному околі точки з вхідного простору. Класифікатор вважа- ється стійким в околі точки, якщо для будь- якої точка в межах даного околу зберіга- ється вихідний клас. Нехай х – n-вимірний вектор на вхі- дному просторі ознак, F – множина індексів ознак, для яких здійснюється верифікація, ε – параметр, що задає величину околу (0 ≤ ε ≤ 1). Тоді позначимо відносний окіл точки х за ознаками F як E(x, ε, F). ( ) 0 ,, , nE x F  (1) Будемо важати, що в разі, якщо то- чка із вхідного простору x' лежить в цьому околі: ( ), , x E x F , то (1 () ,1 ) , i i i i i я і кщоx x x x x накш i F е      − = +   (2) Нехай N – бінарний класифікатор, t – вихідний поріг класифікації. Тоді модель вважатимемо стійкою у відносному околі точки х якщо: ( ) ( ) ( , , ), ( ) ( ) N x t N x t x E x F N x t N x t          (3) 2. Задача виконуваності обмежень Для доведення (або спростування) властивості стійкості моделі у відносному околі точки, зведемо задачу верифікації до задачі виконуваності системи обмежень. У систему включатимемо 3 класи обмежень: Обмеження належності точки до відносного околу над підмножиною ознак визначають базову форму регіону вхідних даних над яким проводиться верифікація. ( ) ( ) ( ) ): 1 (1ieps F i i i F i i C x x x x x     − +           =   Λ Λ Семантичні обмеження над вхід- ними ознаками необхідні для забезпечення правдоподібності вхідних даних. Ці обме- ження відсікають теоретично недосяжні ре- гіони в просторі ознак шляхом встанов- лення міжознакових відношень. :semantic mi j k l hC x x x x x x                  =    Λ Λ Λ де , , , , ,i j k l h m F . Вихідне обмеження – це обмеження, яке констатує, що передбачуваний мо- деллю клас для оригінальної точки та точок з її околу мають співпадати. ( ) , ( ) : ( ) , ( )output N x t якщо N x t C N x t якщо N x t        (4) Тоді, враховуючи всі зазначені об- меження, сформуємо задачу виконуваності у вигляді: , ( ) ( ) ( )eps semantic outputx С x С x С x     → (5) Якщо SMT-розв’язувачу вдається довести загальнозначимість формули вище, то модель є стійкою на заданому околі з урахуванням накладених семантичних об- межень. Додатково зазначимо, що на прак- тиці може бути корисним позбавлення ква- нтора загальності. В такому разі задачу ви- конуваності можна переформулювати у то- тожну задачу «невиконуваності» (тобто до- ведення, що не існує жодної інтерпретації, за якого формула є істиною). Для цього ви- разимо імплікацію через диз’юнкцію, після чого до отриманого виразу застосуємо запе- речення і друге правило де Моргана. Тепер задача верифікації звелася до доведення не- виконуваності оберненої формули: ( ) ( ) ( )eps semantic outputС x С x С x    (6) Розглянемо приклад обмежень для класифікатора мережевих потоків. Нехай мережевий потік характеризується векто- ром із 5 ознак ["Duration", "IAT Std", "IAT Min", "IAT Max", "Bytes"]. Маємо бінарний класифікатор потоків N, з поро- гом t = 0.51, у разі перевищення якого гіпо- 257 Машинне навчання та нейронні мережі теза класифікації приймається і потік зара- ховується до класу «шкідливих». Припус- тимо, необхідно довести стійкість моделі N у відносному околі «шкідливого» потоку х = [0.3, 0.1, 0.01, 0.05, 0.5] за варіювання мі- жпакетних інтервалів (IAT – “inter-arrival time”) для ε = 0.4. Тоді індекси ознак, для яких проводиться верифікація: F = {1, 2, 3} (нумерація починається з 0). Єдине семан- тичне обмеження над ознаками: "IAT Min" ≤ "IAT Max". Сформулюємо обмеження для цієї задачі: Обмеження відносного околу: 0 1 1 2 2 3 3 4 : 0.3 (1 0.4) 0.1 (1 0.4) 0.1 (1 0.4) 0.01 (1 0.4) 0.01 (1 0.4) 0.05 (1 0.4) 0.05 0.5 epsС x x x x x x x x  =   −     +    −     +    −     +    = Семантичне обмеження над озна- ками 2 3:semanticС x x  . Вихідне обмеження : ( ) 0.51outputС N x  . Для автоматичної перевірки викону- ваності даних обмежень необхідно ство- рити символьне представлення повного об- числювального графу нейронної мережі N(x) у вхідній мові SMT-розв’язувача. В на- ступному розділі описано принцип побу- дови такого представлення для подальшої обробки розв’язувачем Microsoft Z3. 3. Застосування Z3 для верифікації нейронної мережі В даній роботі ми обмежились пов- нозв’язною мережею з 50 входами, 3 при- хованими рівнями по 24 нейронами в кож- ному та одним вихідним нейроном. Функції активації прихованих рівнів - ReLU, а вихі- дного нейрону - Sigmoid. Для аналізу нейронної мережі SMT- розв’язувачем Z3 необхідно побудувати її тотожну інтерпретацію через структурні елементи Z3. Для взаємодії із Z3 в даній ро- боті використовується інтерфейс Z3Py (Python Z3 API). Побудова абстрактного синтаксич- ного дерева нейромережі відбувається порі- внево, починаючи від вхідного рівня і за- кінчуючи вихідним, за базовими правилами обрахунку активацій нейронів для пов- нозв’язних мереж: вектор-рядок активацій попереднього рівня множиться на вагову матрицю наступного з додаванням вектора- рядка зміщень. Після чого до отриманого вектора поелементно застосовується функ- ція активації. Значення кожного параметра моделі «загортаються» в об’єкт z3.RealVal, який представляє дійсне чи- сло-константу. Значення вільних змінних (нейрони вхідного шару мережі) представ- ляються через z3.Real. Як приклад, на Рис.1 показана триві- альна нейромережа з 2 входами, одним при- хованим рівнем та одним вихідним нейро- ном. Рис. 1. Приклад графу нейромережі. На Рис.2 наведено структурну ітерп- ретацію обчислювального графу вихідного нейрону такої мережі, виражену елемен- тами Z3Py (для простоти сприйняття, обго- ртки «z3.RealVal» над дійсними констан- тами пропускаються). Рис. 2. Представлення вихідного нейрону в Z3Py. В побудованому обчислювальному графі відсутня функція активації вихідного нейрону (яка у випадку нашої задачі - сиг- моїда). Для представлення сигмоїди необ- хідна трансцендентна функція, а тому її не можна тотожно представити лише ліній- 258 Машинне навчання та нейронні мережі ною арифметикою та булевою алгеброю. Зазвичай, для представлення таких неліній- них функцій використовують апроксима- цію лінійними сегментами. Однак у кон- тексті нашої задачі ми пропонуємо скорис- татися тим, що сигмоїда є монотонно зрос- таючою на всій множині визначення, а тому порівняння її значення з очікуваним поро- гом класифікації (threshold) можна замі- нити на порівняння її аргументу (лінійної комбінації активацій нейронів передостан- нього рівня) зі значенням оберненої функції від порогу (inv_sigmoid(threshold)). Та- ким чином ми уникаємо апроксимації і таке представлення мережі залишається матема- тично тотожним оригінальному. Зауважимо, що ідея “наївної” конве- рсії повнозв’язної нейронної мережі у вираз Z3 вже застосовувалась (як-от в Sapphire[9]). Таке представлення є надзвичайно потуж- ним, адже дозволяє задавати довільні обме- ження над вхідними змінними та вихід- ними значеннями в рамках теорій відомих Z3 (лінійна, нелінійна, булева арифметика і т.д.). Однак цей підхід поки не набув знач- ного розвитку через неприйнятну часовит- ратність під час обробки SMT розв’язува- чем такого обчислювального графу, що особливо помітно у процесі зростання кіль- кості шарів в нейромережі. В наступному розділі запропоновано спосіб вирішення цієї задачі для випадку локальної верифіка- ції мережі. 4. Алгоритм спрощення структури нейромережі Одним зі шляхів до скорочення часу необхідного для доведення чи спросту- вання властивостей нейронної мережі SMT-розв’язувачем є спрощення представ- лення її обчислювального графу, а саме ви- явлення та вилучення нелінійностей. Розглянемо ситуацію, коли всі фун- кції активації нейронів мережі є глобально нелінійними, але водночас кусково-ліній- ними (тобто лінійними на інтервалах). Для визначення рельєфу кордону ухвалення рі- шень класифікатора над усім вхідним прос- тором необхідна повна композиція неліній- них активацій усіх нейронів мережі. Однак на відносно малому локальному проміжку вхідних значень кількість нелінійних функ- цій, необхідних для тотожного представ- лення нейронної мережі, значно скорочу- ється. В такому випадку обчислювальний граф нейромережі можна спростити. Для кожного нейрону розглядається можли- вість спрощення через заміни його неліній- ної функції активації на лінійну, тотожну на даному інтервалі оригінальній. Це стає мо- жливим, якщо діапазон можливих значень функції активації лежить повністю в межах інтервалу її лінійності. Чим вужчий діапа- зон входів мережі, тим більше спрощень нейронних активацій на ньому можна про- вести. В той же час у випадку звуження вхі- дного діапазону до єдиної точки, обчислю- вальний граф вироджується в цільну лі- нійну функцію. На рис. 3 продемонстрована ідея ло- кальної апроксимації кусково-лінійної фун- кції до нової, тотожної оригінальній лише на певному інтервалі. Як видно, під час зву- ження інтервалу, глобальна складність ап- роксимованої функції зменшується, адже зменшується кількість точок зламу («куто- вих точок»). Рис. 3. Приклади локальних апрок- симацій кусково-лінійної функції. Для нейронних мереж властивість нелінійності забезпечується функціями ак- тивації нейронів - в нашому випадку це ReLU. Водночас, саме функції активації є найбільшим фактором складності у процесі аналізу графу нейромережі SMT-розв’язу- вачем, адже кількість можливих шляхів по- роджених умовними розгалуженнями («if- else», в які транслюється ReLU), у графі ко- мібнаторно зростає разом зі зростанням глибини мережі. 259 Машинне навчання та нейронні мережі ReLU складається лише з двох ліній- них сегментів, які визначаються на проміж- ках (-inf, 0], та (0, +inf). Якщо на певній пі- дмножині вхідних значень моделі діапазон значень, що подаються на вхід нейрона, ле- жить повністю в одному з цих двох промі- жків, то функція активації ReLU для даного нейрону рівноцінна константі 0 (x = 0), або ж тотожній функції (x = x). Таким чином у разі заміни ReLU на одну з тривіальних аль- тернатив в побудованому обчислюваль- ному графі нейронної мережі, задача дове- дення властивостей SMT-розв’язувачем значно спрощується, адже зменшується кі- лькість розгалужень. Можливість такого спрощення згадується в [5], щоправда в контексті звуження можливих меж входів, використовуючи симплекс-метод. У нашій роботі, пропонується альте- рнативний метод для знаходження можли- востей спрощення функцій активації ReLU шляхом розв’язання локальної SMT-задачі для кожного окремого нейрону. Нехай не- обхідно провести верифікацію повнозв’яз- ної нейромережі в околі точки х з вхідного набору даних. Як і раніше, окіл позначимо як E(x,ε,F). Спрощення здійснюється порів- нево в один прохід по графу мережі, почи- наючи з першого прихованого рівня. Для кожного рівня алгоритм виконує 2 фази. Перша фаза – це спроба провести попередню «наївну» оптимізацію функцій активації нейронів без розв’язування SMT- задач. Для нейрона проводиться оцінка найширших теоретично можливих меж його вхідних значень, виходячи з обрахова- них меж активацій нейронів попереднього рівня. Очевидно, що отримані межі не обов’язково є практично досяжними і за- звичай будуть значно ширші, ніж реально можливі. Якщо нижня межа вхідних зна- чень нейрону > 0, то ReLU заміняється на тотожну функцію, а якщо верхня межа ≤ 0, то ReLU заміняється на константу 0. Вод- ночас межі для вхідного рівня визнача- ються безпосередньо обраним околом E(x,ε,F). Якщо для нейрону на першій фазі спрощення не відбулося, то для нього буде застосована друга фаза. В другій фазі, SMT-роз’язувач про- водить повний аналіз обчислювального графу кожного з неспрощених нейронів да- ного рівня над околом E(x,ε,F). Нам уже ві- доме значення, що подається на вхід функ- ції активації нейрона для вхідної точки х. Позначимо це значення як n(x). Задача пе- ревірки можливості спрощення ReLU зво- диться до доведення відсутності такої то- чки x' ∈ E(x,ε,F) для якої значення, що по- дається на вхід даного нейрону n(x') лежа- тиме по протилежний бік від 0 відносно n(x). Це можна виразити у формі обме- ження: ( ) 0, ( ) 0 : ( ) 0, ( ) 0neuron n x якщо n x C n x якщо n x        (7) Якщо SMT-роз’язувач доводить невикону- ваність даного обмеження, то діапазон зна- чень n(x') повністю лежить в одному з ін- тервалів лінійності ReLU для ( ), , x E x F  , що дозволяє провести спрощення. ReLU замінюється на тотожну функцію, якщо n(x) > 0, або ж на константу 0, якщо n(x) ≤ 0. В іншому випадку спро- щення для даного нейрона не відбувається. Зауважимо, що ідея такого спро- щення є евристичною. Очікується, що ви- трати на інкрементальне спрощення шля- хом понейронного ров’язування SMT-задач на вже спрощених підграфах є менш часо- витратними, ніж одноразовий аналіз оригі- нального графу нейромережі. Крім того, очевидно, що зі збільшенням вхідного околу зменшується кількість можливостей спрощення функцій активації, і тому ефек- тивність такого підходу буде падати. В най- гіршому випадку час виконання буде біль- шим, ніж під час аналізу неоптимізованого графу мережі. Незважаючи на це, в кон- тексті задачі верифікації моделі класифіка- ції мережевих потоків саме така оптиміза- ція дозволила проаналізувати повну мно- жину точок інтересу за прийнятний час, про що йдеться в наступному розділі. 5. Експериментальні результати Ми розглядали модель класифікації мережевих потоків на предмет виявлення активності ботнетів, які є джерелом атак на інтернет ресурси та WEB-застосунки. Модель представлена нейронною мережею, навченою на мережевих потоках 260 Машинне навчання та нейронні мережі виділених з набору даних ISCX Botnet 2014 [10]. Кожен мережевий потік представле- ний набором з 50 ознак, отриманих за допо- могою інструменту CIC Flow Meter V4.0 [11]. Поріг класифікації встановлено в 0.51 – якщо значення на вихідному нейроні ме- режі перевищує цей поріг, потік вважається «шкідливим», тобто таким, що містить ак- тивність ботнетів. Після цього з навчальної вибірки було виділено всі потоки, які мо- дель класифікувала вірно, але вони лежать близько до межі ухвалення рішень (тобто для них прогнозована впевненість > 0.51, але < 0.55) – всього 836 потоків (тобто 0.76% від повної вибірки). Верифікація у відносному околі то- чок здійснювалась над семантично зв’яза- ною групою із 9 ознак, а саме, «загальна тривалість» та статистики «міжпакетних ін- тервалів» потоків (інші ознаки залишались фіксованими): "Flow Duration", "Fwd IAT Total", "Fwd IAT Std", "Fwd IAT Max", "Fwd IAT Min", "Bwd IAT Total", "Bwd IAT Std", "Bwd IAT Max", "Bwd IAT Min" Водночас накладались додаткові об- меження правдоподібності: "Fwd IAT Max" >= "Fwd IAT Min", "Bwd IAT Max" >= "Bwd IAT Min" Верифікація проводилась для відно- сних околів з параметром ε: 0.05, 0.1 та 0.15. Таблиця 1 Результати верифікації класифікатора мережевих потоків ε # verified # failed Time Avg. final ReLU count 0.05 763 73 6m 32s 0.23 0.1 722 114 15m 8s 0.48 0.15 711 125 92m 22s 0.83 У Табл. 1, колонка “# verified” пока- зує кількість мережевих потоків, для яких доведено, що завжди зберігається клас під час довільного варіювання міжпакетних ін- тервалів у зазначених межах. Колонка “# failed” відображає кількість випадків, для яких існує така варіація, за якої передбачу- ваний моделлю клас не співпадає з оригіна- льним. Як і очікувалось, у процесі зрос- тання ε, також зростає і кількість можливо- стей помилки класифікації. В останній ко- лонці наведено середня кількість функцій ReLU, які лишились після спрощення обчи- слювального графу мережі. Як видно, для більшості випадків достатньо щонайбільше однієї ReLU для математично-тотожного представлення моделі на даних вхідних ді- апазонах. Висновки В даній роботі було розроблено ме- тод для доказової перевірки надійності ней- ромереж-класифікаторів. Було показано практичне застосування даного методу для верифікації системи аналізу мережевого трафіку на предмет активності ботненів. Це є важливим результатом, адже застосу- вання ШІ в галузі кібербезпеки суттєво об- межене обсягом наявних наборів даних для їх емпіричного тестування. Крім того, да- ний метод дає можливість гарантувати ло- кальну стійкість класифікаторів до змагаль- них атак, тобто навмисних спроб ухиляння хакерів від виявлення їх дій. Було показано, що алгоритм здатен як довести коректність роботи моделі класифікації на певних регі- онах вхідного простору даних, так і ви- явити проблемні зони, де модель може при- пуститися помилки. Крім того, отримані експеримента- льні дані підтверджують ефективність за- пропонованої оптимізації обчислюваль- ного графу мережі через порівневе спро- щення функцій активації шляхом рішення локальних SMT-задач. Описаний підхід верифікації нейро- мереж може бути застосований не лише в задачах кібербезпеки, а й у будь-яких сис- темах класифікації, де точність є критич- ною, зокрема, в розпізнаванні образів або мови. Одним із напрямків подальших дос- ліджень, є використання запропонованого методу верифікації для мереж із довіль- ними функціями активації. Наприклад, че- рез їх апроксимацію лінійними сегментами. 261 Машинне навчання та нейронні мережі Крім того запропонований спосіб ін- крементальної оптимізації графу мережі та- кож має значний потенціал для подальшого розвитку. Зокрема, саму процедуру спро- щення обчислювального графу можливо значно прискорити, якщо послідовне рі- шення понейронних SMT-задач в межах од- ного рівня замінити на паралельне. Такі за- дачі не потребують між-потокової синхро- нізації. Також при вилученні нелінійностей можливо брати до уваги межі можливих вхідних значень не якогось окремого ней- рону, а комбінації меж кількох нейронів да- ного рівня. Нарешті, самим важливим напрям- ком подальших досліджень у галузі кібер- безпеки є створення методів по півищенню надійності та стійкості моделей виявлення мережевих загроз, як до змагальних атак, так і до випадкових флуктуацій в мереже- вих даних. Література 1. Casadio, M. et al. (2022). Neural Net- work Robustness as a Verification Property: A Principled Case Study. In: Shoham, S., Vizel, Y. (eds) Computer Aided Verification. CAV 2022. Lec- ture Notes in Computer Science, vol 13371. Springer, Cham. https://doi.org/10.1007/978-3-031- 13185-1_11 2. Odena, A., Olsson, C., Andersen, D., Goodfellow, I.. (2019). TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing. Proceed- ings of the 36th International Confer- ence on Machine Learning, in Proceed- ings of Machine Learning Research 97:4901-4911. https://doi.org/10.48550/arXiv.1807.1 0875 3. Z. Yang, J. Shi, M. Asyrofi and D. Lo, "Revisiting Neuron Coverage Metrics and Quality of Deep Neural Net- works," in 2022 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), Honolulu, HI, USA, 2022 pp. 408-419. 10.1109/SANER53432.2022.00056 4. Goodfellow, Ian & Shlens, Jonathon & Szegedy, Christian. (2014). Explaining and Harnessing Adversarial Examples. https://doi.org/10.48550/arXiv.1412.6 572 5. Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J. (2017). Relu- plex: An Efficient SMT Solver for Ver- ifying Deep Neural Networks. In: Ma- jumdar, R., Kunčak, V. (eds) Computer Aided Verification. CAV 2017. Lec- ture Notes in Computer Science(), vol 10426. Springer, Cham. https://doi.org/10.1007/978-3-319- 63387-9_5 6. Katz, G. et al. (2019). The Marabou Framework for Verification and Anal- ysis of Deep Neural Networks. In: Dil- lig, I., Tasiran, S. (eds) Computer Aided Verification. CAV 2019. Lec- ture Notes in Computer Science(), vol 11561. Springer, Cham. https://doi.org/10.1007/978-3-030- 25540-4_26 7. Elboher, Y.Y., Gottschlich, J., Katz, G. (2020). An Abstraction-Based Frame- work for Neural Network Verification. In: Lahiri, S., Wang, C. (eds) Computer Aided Verification. CAV 2020. Lec- ture Notes in Computer Science(), vol 12224. Springer, Cham. https://doi.org/10.1007/978-3-030- 53288-8_3 8. de Moura, L., Bjørner, N. (2008). Z3: An Efficient SMT Solver. In: Rama- krishnan, C.R., Rehof, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Sci- ence, vol 4963. Springer, Berlin, Hei- delberg. https://doi.org/10.1007/978-3- 540-78800-3_24 9. Sapphire. Accessed: 01.04.2024. https://github.com/wenkokke/sapphire 10. Beigi, E.B., Jazi, H.H., Stakhanova, N., Ghorbani, A.A.: Towards effective fea- ture selection in machine learning- based botnet detection approaches. In: 2014 IEEE Conference on Communi- cations and Network Security. pp. 247– 255 (2014) 262 Машинне навчання та нейронні мережі https://dx.doi.org/10.1109/CNS.2014. 6997492 11. CICFlowMeter (formerly ISCXFlow- Meter). Accessed: 01.04.2024. https://www.unb.ca/cic/research/appli cations.html Одержано: 10.04.2024 Внутрішня рецензія отримана: 18.04.2024 Зовнішня рецензія отримана: 25.04.2024 Про авторів: 1Панчук Богдан Олександрович, аспірант. https://orcid.org/0000-0002-5389-359X. Місце роботи авторів: 1 Інститут кібернетики ім. В.М. Глушкова НАН України, Тел. (+38) (044) 526-20-08 E-mail: incyb@incyb.kiev.ua, Сайт: www.incyb.kiev.ua

Formal verification of deep neural networks

Institution

Ähnliche Einträge