ГОСТ Р 70462.1—2022
6.3.3 Использование методов оптимизации для доказательства свойства максимально
стабильного пространства
Общие методы оптимизации также позволяют верифицировать нейронную сеть, при этом любая
проблема выполнимости преобразуется в задачу оптимизации. Затем становится возможным приме
нить обычные методы оптимизации, такие как алгоритм «ветвления и границы» (Branch and Bound),
чтобы решить эту проблему.
Свойство максимально стабильного пространства, как правило, выражается в виде булевой фор
мулы над линейными неравенствами. Например, выход сети должен быть больше некоторой части
входного пространства. Чтобы доказать это с помощью метода оптимизации, предполагаемое свойство
выражается в виде дополнительных слоев в конце сети. Таким образом, после нахождения решения за
дачи оптимизации осуществляется решение проблемы выполнимости путем проверки знака
решения. В [23] описано построение данной задачи оптимизации на основе задачи выполнимости в
нейронной сети, сочетающей классический градиентный спуск для нахождения локального минимума,
а также оп тимизатор ветвей и границ для определения глобального оптимума.
Еще один пример методов оптимизации для доказательства устойчивости нейронных сетей каса
ется использования программирования с ограничениями [24]. Вначале нейронная сеть аппроксимирует
ся ее моделированием как линейной программы (с использованием сети, составленной из кусочно-ли
нейных функций), затем аппроксимируя возможные состояния, применяя только выпуклые множества
и итеративно решатель ограничений, чтобы доказать свойство робастности.
6.3.4 Использование абстрактной интерпретации для доказательства свойства максималь
ного стабильного пространства
Абстрактная интерпретация — это вид формального метода, основанного на теории построения
контролируемых аппроксимаций (см. приложение В для получения дополнительной информации).
Данный метод часто используют для доказательства сложных свойств программ [25]. Абстрактные
интерпретации занимают значительное место в сообществе верификации и валидации программного
обеспечения, особенно в контексте критически важного для безопасности программного обеспечения,
такого как встроенное программное обеспечение для самолетов [26], автомобилей [27] и космических
аппаратов [28].
В работах [29], [30], [31], [32] представлены конструкции новых абстрактных областей, специально
адаптированных под поведение нейронных сетей. Нелинейная природа нейронных сетей имеет тен
денцию делать некоторые из существующих абстрактных областей неэффективными, особенно это
касается областей, использующих аффинную динамику системы для определения абстрактных обла
стей. Так обстоит дело, например, с новой зонотопической областью, описанной в [30], которая от
ражает специфическую динамику функций активации ReLU, обычно используемых в нейронных сетях
обработки изображений.
Для того чтобы доказать устойчивость принимаемого решения по некоторому региону входного
пространства, нужно сначала выразить регион входного пространства, подлежащий анализу, с исполь
зованием абстрактной области. Затем необходимо определить абстрактную семантику, способную вы
полнять символьные вычисления нейронной сети в данной абстрактной области. Выходом является аб
страктное значение, представляющее аппроксимацию возможных выходных данных классификатора
на этом регионе входного пространства. Результатом служит вектор, элементами которого становится
достоверность классификации для каждого класса. Любой элемент сам по себе абстрактное значение
(например, интервал). После вычисления выхода возможны два случая: либо один из элементов боль ше
другого, либо отсутствует класс, который бы доминировал при принятии решения.
7 Эмпирические методы
7.1 Общие положения
Следующим аспектом робастности, охватываемым в настоящем стандарте, является субъектив
ная оценка робастности. Данная оценка основана на функциональной оценке на системном уровне,
для которой наиболее приемлемы эмпирические методы, с помощью которых проводят сбор
сведений по этому вопросу.
14