ГОСТ Р 70462.1—2022
быть неустойчивым, а в других — устойчивым. Поскольку сложно охватить каждый регион области,
чтобы найти эти неустойчивые поведения, то весьма вероятно, что такие области будут упущены, и
это снизит робастность. Такое незапланированное поведение составляет неопределенность в оценке
качества интерполяционной способности нейронной сети.
6.2.3 Максимальное стабильное пространство для сопротивления возмущениям
Для снижения рисков, связанных с возмущениями данных, которые также называются неблаго
приятными (adversarial) примерами, можно доказать устойчивость классификатора до определенного
момента. Для достижения этой цели используют свойство максимального стабильного пространства.
Считают, что для конкретного входного сигнала отсутствует неблагоприятный пример. Понятие рассто
яния необходимо для определения набора входных данных, которые находятся «вокруг» конкретной
точки. В приложении А приведено описание нескольких типов искажений данных, а также соответству
ющих метрик расстояния для оценки нейронных сетей.
В настоящем пункте описаны три общих подхода, которые могут продемонстрировать свойство
максимального стабильного пространства, используемое для измерения робастности нейронной сети,
выполняющей классификацию. Это свойство может быть доказано следующими способами:
1) как логическая задача, разрешаемая с использованием решателя;
2) как числовая проблема, решаемая с помощью алгоритма оптимизации, посредством которого
вычисляют максимум;
3) как математическое свойство, которое аппроксимируется путем абстрактной интерпретации.
Каждый метод был адаптирован с учетом специфики нейронных сетей.
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] рассмотрена комбинация решения
выполнимости и линейного программирования на линейной аппроксимации общего поведения сети. В
этих работах отражена возможность адаптировать общие технологии решателей для подтверждения
свойств в нейронных сетях, доказать робастность классификаторов, а также использовать данные ме
тоды для решения других задач нейронных сетей.
13