ГОСТ Р 70462.1-2022/ISO/IEC TR 24029-1-2021. Национальный стандарт Российской Федерации. Информационные технологии. Интеллект искусственный. Оценка робастности нейронных сетей. Часть 1. Обзор

6.3 Проведение тестирования формальными методами

6.3.1 Использование анализа неопределенности для доказательства стабильности интерполяции

Анализ неопределенности - это метод, обычно используемый для управления поведением математических функций. Цель состоит в том, чтобы определить, на каких входах функция имеет внезапные и существенные изменения. Для нейронных сетей - это действенный способ обнаружить проблемы, описанные в 6.2.2, в частности: можно сравнить измеренное поведение с представлением о фактическом поведении. Цель состоит в том, чтобы измерить способность нейронной сети моделировать в пределах допустимого диапазона отклонений явление, которое она предназначена моделировать. Это способствует измерению вариации отклика сети, чтобы убедиться в отсутствии нестабильного поведения.

Проделана фундаментальная работа по формализации стабильности нейронной сети. Например, в [17] описан метод расчета распространения неопределенности в сети, позволяющий таким образом обнаруживать регион, в котором ответ нейронной сети является ненормальным, а неробастное поведение должно быть ожидаемым. В [18] представлен метод, показывающий влияние или важность входных переменных на выход, независимо от природы переменных (непрерывная или дискретная). В [19] приведено несколько источников неопределенности, включая неопределенность входных данных, чувствительность сети и влияние случайности разбиения наборов данных для обучения и тестирования. Таким образом, можно определить условия, при которых сеть не является робастной, и установить причину неопределенности в отклике сети.

6.3.2 Использование решателя для доказательства свойства максимального стабильного пространства

Известно, что нейронные сети, как правило, достаточно большие, нелинейные, невыпуклые и недоступны для универсальных инструментов, таких как решатели линейного программирования или существующие теории выполнимости по модулю (satisfiability modulo theories, SMT). Тем не менее получено несколько достижений при использовании технологий решателей для подтверждения свойств в нейронных сетях. В качестве примера в [20] представлен подход к эффективному доказательству свойств над некоторыми классами нейронных сетей [с использованием функций активации ReLU (Rectified Linear Unit), определенной как ReLU(x) = max(0, x)] посредством варианта симплекс-алгоритма. В [21] решатель SMT применяют для доказательства отсутствия или существования неблагоприятного примера, включая возможность его демонстрации. В [22] рассмотрена комбинация решения выполнимости и линейного программирования на линейной аппроксимации общего поведения сети. В этих работах отражена возможность адаптировать общие технологии решателей для подтверждения свойств в нейронных сетях, доказать робастность классификаторов, а также использовать данные методы для решения других задач нейронных сетей.

6.3.3 Использование методов оптимизации для доказательства свойства максимально стабильного пространства

Общие методы оптимизации также позволяют верифицировать нейронную сеть, при этом любая проблема выполнимости преобразуется в задачу оптимизации. Затем становится возможным применить обычные методы оптимизации, такие как алгоритм "ветвления и границы" (Branch and Bound), чтобы решить эту проблему.

Свойство максимально стабильного пространства, как правило, выражается в виде булевой формулы над линейными неравенствами. Например, выход сети должен быть больше некоторой части входного пространства. Чтобы доказать это с помощью метода оптимизации, предполагаемое свойство выражается в виде дополнительных слоев в конце сети. Таким образом, после нахождения решения задачи оптимизации осуществляется решение проблемы выполнимости путем проверки знака решения. В [23] описано построение данной задачи оптимизации на основе задачи выполнимости в нейронной сети, сочетающей классический градиентный спуск для нахождения локального минимума, а также оптимизатор ветвей и границ для определения глобального оптимума.

Еще один пример методов оптимизации для доказательства устойчивости нейронных сетей касается использования программирования с ограничениями [24]. Вначале нейронная сеть аппроксимируется ее моделированием как линейной программы (с использованием сети, составленной из кусочно-линейных функций), затем аппроксимируя возможные состояния, применяя только выпуклые множества и итеративно решатель ограничений, чтобы доказать свойство робастности.

6.3.4 Использование абстрактной интерпретации для доказательства свойства максимального стабильного пространства

Абстрактная интерпретация - это вид формального метода, основанного на теории построения контролируемых аппроксимаций (см. приложение B для получения дополнительной информации). Данный метод часто используют для доказательства сложных свойств программ [25]. Абстрактные интерпретации занимают значительное место в сообществе верификации и валидации программного обеспечения, особенно в контексте критически важного для безопасности программного обеспечения, такого как встроенное программное обеспечение для самолетов [26], автомобилей [27] и космических аппаратов [28].

В работах [29], [30], [31], [32] представлены конструкции новых абстрактных областей, специально адаптированных под поведение нейронных сетей. Нелинейная природа нейронных сетей имеет тенденцию делать некоторые из существующих абстрактных областей неэффективными, особенно это касается областей, использующих аффинную динамику системы для определения абстрактных областей. Так обстоит дело, например, с новой зонотопической областью, описанной в [30], которая отражает специфическую динамику функций активации ReLU, обычно используемых в нейронных сетях обработки изображений.

Для того чтобы доказать устойчивость принимаемого решения по некоторому региону входного пространства, нужно сначала выразить регион входного пространства, подлежащий анализу, с использованием абстрактной области. Затем необходимо определить абстрактную семантику, способную выполнять символьные вычисления нейронной сети в данной абстрактной области. Выходом является абстрактное значение, представляющее аппроксимацию возможных выходных данных классификатора на этом регионе входного пространства. Результатом служит вектор, элементами которого становится достоверность классификации для каждого класса. Любой элемент сам по себе абстрактное значение (например, интервал). После вычисления выхода возможны два случая: либо один из элементов больше другого, либо отсутствует класс, который бы доминировал при принятии решения.