Введение 4
SMT-формулы 4
SMT-логики 6
SMT-решатели 9
Применения 10
Символьное исполнение 11
Постановка задачи 13
Обзор литературы и предметной области 15
Устройство GNN 15
FastSMT 18
GNN for Scheduling of SMT Solvers 21
NeuroSAT 23
1. Датасет 26
1.1. SMT-COMP 26
1.2. USVM 27
1.3. Метрики 31
2. Подход с использованием GNN 33
2.1. Архитектура нейронной сети для решения задачи 33
2.2. Начальные состояния вершин 35
2.3. Вычисление состояний вершин 40
2.3.1 SAGE Convolution 40
2.3.2 Transformer Convolution 41
2.3.3 Учёт начального состояния вершины 41
2.4. Классификатор и функция потерь 42
3. Эксперименты и результаты 43
3.1. Первый эксперимент 43
3.2. Второй эксперимент 44
3.3. Третий эксперимент 46
3.4. Четвёртый эксперимент 46
4. Дальнейшее развитие 49
Заключение 51
Список литературы 52
Приложение 57
SMT-формулы (от англ. Satisfiability Modulo Theories) являются одним из наиболее важных объектов в области практических применений математической логики. Они позволяют сначала формальным образом записать разнообразные утверждения из различных предметных областей, а затем с помощью специальных вычислительных методов проверить логическую выполнимость (состоятельность) этих утверждений.
SMT-формула является некоторым расширением SAT-формулы, которое позволяет использовать не только логические переменные и связки с ними, а ещё и выражения с участием объектов из некоторого домена (например: целые числа, вещественные числа, битовые векторы, массивы) и различными операциями с ними (например: числовая арифметика, битовые операции, взятие элемента массива по индексу и т. д.).
Более формально, SMT-формула является формулой в логике первого порядка, где у каждой константы и у каждого символа переменной или функции есть некоторый заранее определенный тип (домен), а в качестве функциональных символов используются функции и операторы из разных доменов (например, те же битовые операции или взятия элемента массива по индексу). Задача проверки выполнимости1 такой формулы состоит в том, чтобы выяснить, можно ли для каждой свободной (не находящейся под квантором) переменной подобрать значение соответствующего ей типа так, чтобы при подстановке данных значений формула была истинна. Помимо этого, чаще всего, если формула выполнима, требуется также для каждой свободной переменной выдать значение, сопоставляемое ей. Это отображение из множества свободных переменных в множество их значений называют моделью.
Чтобы стало более понятно, покажу несколько примеров.
Пример формулы:
(x + y + z = 2) Л (x + 2y + 3z = 2) Л (x + 2y + 4z = 1), (1)
где х, у и z — целые числа. Эта формула является выполнимой, поскольку при подстановке значений х —- 1, у —- 2, z — 1 формула превращается
в истинное утверждение.
Ещё пример:
(х = 2у) Л (х = 2z + 1). (2)
Если потребовать, чтобы х, у и z в этой формуле были целыми числами, то формула, очевидно, не будет выполнимой (т. к. в этом случае написанное здесь обозначает высказывание х является чётным и х является нечётным). Однако, если разрешить переменным быть вещественными (или хотя бы рациональными), формула станет выполнимой. Этот пример показывает, что свойство выполнимости зависит от типовых (доменных) ограничений, наложенных на переменные и функциональные символы.
Пример формулы с кванторами:
9 х,у^ : (п > 0) Л (х > 0) Л (у > 0) Л (z > 0) Л (хп + уп = zn), (3)
где все переменные являются целыми числами. В этой формуле присутствует только одна свободная переменная — п, поэтому искать подходящее значение нужно только для неё. Нетрудно заметить, что нам подходят значения п = 1 и п = 2, поэтому формула является выполнимой (но если условие п > 0 заменить на п > 3, формула станет невыполнимой согласно Великой теореме Ферма).
Примером формулы с битовыми векторами является формула (4).
(х > #Ь01000000) Л (х + (х shl2 #Ь00000001) + #Ь11111111 < #Ь00100000), (4)
где переменная х является битовым вектором размера 8 (фактически, это беззнаковое числом размером 1 байт). Аналогично, все константы3 в формуле тоже являются битовыми векторами размера 8 и записываются в бинарном формате. Стоит также отметить, что каждый битовый вектор можно однозначно отождествить с числом через его запись в двоичной системе счисления (например, таким образом происходит сравнение векторов на больше-меньше).
...
В рамках данной работы была предпринята попытка создать нейронную сеть для предсказания выполнимости SMT-формулы: собрать подходящий да- тасет, реализовать архитектуру нейронной сети, провести ряд экспериментов с обучением и валидацией моделей и сделать выводы.
Я считаю, что сформулированная в работе задача выполнена — основные шаги для решения поставленной поставленной задачи, описанные в соответствующем разделе, пройдены, и требуемое исследование проведено.
В процессе работы было выяснено, что для решения задачи в общем случае протестированных методов недостаточно, и нужно использовать более умные подходы к построению векторного представления формулы, о чём написано в главе 4.
Однако, в контексте практического применения (решения формул, возникающих в процессе символьного исполнения на движке USVM) данная задача может быть решена с относительно хорошими результатами при помощи более-менее базовых методов (таблицы 5, 6 и 7). Скорее всего, это происходит из-за того, что в практической задаче возникают очень специфические формулы, которые значительно отличаются от общего случая в лице SMT-COMP, и для которых гораздо проще предсказывать ответ из-за того, что модель привязывается на некоторые особенности возникающих формул. Я думаю, что перспектива практического использования полученных результатов во многом может опираться на этот факт.
Также в процессе исследования было протестировано несколько возможных архитектур нейронной сети (разделы 2.3.1 и 2.3.2).
Сравнение полученного решения с аналогами не проводилось, поскольку таковых на данный момент не существует (я не считаю аналогом модель NeuroSAT, так как в той задаче существенно отличаются ограничения и ожидаемый результат).
Проведённое исследование можно существенно расширять и дополнять. О методах и возможных путях развития написано в главе 4.
