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