ГОСТ Р 70462.1—2022
Приложение В
(справочное)
Принцип абстрактной интерпретации
В.1 Принцип абстрактной интерпретации
Принцип представлен следующим образом. Во-первых, этот подход обычно рассматривает все возможные
варианты (следы) выполнения программы с использованием семантики, например детонационная [88] или аксио
матическая [89] семантика. Набор всех следов выполнения, выраженный семантикой, образует решетку (полный
частичный порядок, определенный для набора всех следов) или, по крайней мере, набор частичного порядка. Та кая
решетка называется конкретной областью и, как известно, является трудноразрешимой. Затем определяется вторая
область, называемая абстрактной областью, поскольку это абстракция конкретной области. Абстрактная область
также представляет собой решетку или, по крайней мере, набор частичного порядка. Оказывается, что аб стракция
верна, когда связь Галуа определена (и доказана) между двумя областями. Связь Галуа осуществляется путем
определения двух конкретных функций: одна называется абстракцией
а
(переход от конкретной области к
абстрактной), а другая — конкретизацией
у
(переход от абстрактной области к конкретной). Эти функции обладают
специфическими свойствами, которые необходимо доказать заранее, в основном монотонность
а
и
у,
расширяе
мость
у°а
и сжимаемость
а°у.
Как только связь Галуа между двумя областями доказана, абстрактная область становится осмысленным
чрезмерным приближением всех конкретных исполнений, которое также является разрешимым (tractable, по по
строению). Затем можно доказывать свойства на абстрактной области и автоматически переносить их на соответ
ствующие конкретные следы, представленные абстракцией. Основная трудность при абстрактной интерпретации
состоит в том, чтобы определить достаточно простую, но выразительную абстрактную область. Абстрактная об
ласть предназначена быть как разрешимой, так и репрезентативной по отношению к конкретным следам системы.
Существует обширный объем публикаций по определениям абстрактных областей для представления численных
расчетов. Например, можно использовать интервалы [90], пятиугольники [91], восьмиугольники [92], шаблоны [93],
многогранники [94], зонотопы [95] и т. д. Каждый из вариантов является результатом различного компромисса меж ду
точностью абстракции и стоимостью ее расчета.
Пример. Рассмотрим черно-белое изображение размером 2><2, каждый пиксель
(pv
р2, р3, р4) находится в
диапазоне от 0 до 255. Предположим, что существует обученная нейронная сеть, которая выполняет классифи
кацию таких изображений между классами А и В, а также то, что изображение / со значениями (100, 100, 50, 150)
классифицируется как А с достоверностью 90 % и В с достоверностью 10 %. Наконец, предположим, что к изо
бражению применяется однородный шум с интенсивностью 5. Целью обеспечения стабильности нейросети явля
ется доказательство того, что любое изображение /’, полученное из / посредством добавления такого однородного
шума, также в первую очередь относится к классу А. Используя интервальную абстрактную область и определение
однородного шума, строят следующее абстрактное изображение
ft
со значениями ([95; 105], [95; 105], [45; 55],
[145; 155]). Изображение
ft
представляет все возможные изображения /’, которые можно получить из / с однород ным
шумом с интенсивностью, равной 5. Например, оно представляет изображения (102, 104, 45, 150), (98, 100, 53,
155)... Количество изображений, представленных
ft,
достаточно велико, в данном случае это (5 * 2 + 1)2 * 2, в общем
случае это (К* 2 + 1)L х
w(с
максимальной интенсивностью
К
примененного однородного шума,
L * W
— это размер
изображений). Используя абстрактную семантику, можно вычислить абстрактный вывод нейронной сети.
В этом случае предположим, что результат будет следующим ([75; 92], [7; 34]). Первая часть — это достоверность
классификации класса А для изображения
ft,
а вторая часть — для класса В. Поскольку изображение / также пред
ставлено в
ft,
значение 90 принадлежит отрезку [75; 92], а значение 10 также содержится в отрезке [7; 34]. В этом
случае все изображения, представленные
ft,
всегда имеют строго большую уверенность в классе А, чем в клас се
В, поэтому классификация сети не меняется ни на одном из этих изображений. Однако минимум достоверности
класса А составляет 75, что в некоторых случаях ниже порога, необходимого для присвоения класса. Это допуска ет,
что определенные изображения, представленные
ft,
не отнесены к какому-либо классу. Это не обязательно, по
скольку абстрактное значение является переаппроксимацией конкретного результата. Чтобы иметь более жесткие
границы возможных выходных данных, требуется более сложные абстрактные области, например зонотопическая
область вместо интервальной области.
22