Лекционные заметки по верификации графовых нейронных сетей

Основная информация

• ID статьи: 2510.11617
• Название: Lecture Notes on Verifying Graph Neural Networks
• Автор: François Schwarzentruber (ENS de Lyon)
• Классификация: cs.LO (Логика в информатике), cs.LG (Машинное обучение)
• Дата публикации: 14 октября 2025
• Ссылка на статью: https://arxiv.org/abs/2510.11617

Аннотация

В данных лекционных заметках сначала рассматриваются связи между графовыми нейронными сетями, тестом Вейсфейлера-Лемана и логическими системами, включая логику первого порядка и градуированную модальную логику. Затем предлагается модальная логика, в которой модальности подсчёта появляются в линейных неравенствах для решения задач верификации графовых нейронных сетей. Описывается алгоритм решения проблемы выполнимости этой логики, вдохновлённый табличными методами традиционной модальной логики и расширяющий рассуждения над свободными от кванторов фрагментами булевой алгебры и арифметики Пресбургера.

Исследовательский контекст и мотивация

Постановка проблемы

Графовые нейронные сети (GNN) широко применяются в рекомендательных системах социальных сетей, графах знаний, анализе химических молекул и открытии лекарств. Однако верификация GNN сталкивается со значительными вызовами:

1. Ограничения выразительной способности: Выразительная способность GNN ограничена тестом 1-WL (Вейсфейлера-Лемана) и не может различать некоторые неизоморфные графы
2. Сложность задач верификации: Необходимо проверить, удовлетворяет ли GNN определённым спецификациям, таким как безопасность и корректность
3. Недостаток теоретических основ: Отсутствует систематическая логическая база для описания и верификации поведения GNN

Исследовательская мотивация

• Практические требования: В критичных по безопасности приложениях необходимо обеспечить надёжность и корректность GNN
• Теоретические пробелы: Существующие методы верификации лишены единой логической теоретической основы
• Технические вызовы: Необходимо обрабатывать операции агрегирования и ограничения подсчёта в GNN

Основные вклады

1. Установление теоретических связей: Систематическое изложение глубоких связей между GNN, тестом Вейсфейлера-Лемана и логическими системами (FO, FOC, GML)
2. Предложение логики K#: Разработка новой модальной логики K#, способной выражать операции подсчёта и агрегирования в GNN
3. Разработка алгоритма: Создание PSPACE-алгоритма для проблемы выполнимости логики K#, основанного на табличных методах и рассуждениях QFBAPA
4. Анализ сложности: Доказательство границ вычислительной сложности задач верификации GNN при различных функциях активации
5. Практическая база: Предоставление полной схемы для сведения задач верификации GNN к проблемам выполнимости логики

Детальное описание методов

Определение задач

Основные задачи верификации GNN включают:

• Выполнимость: Для данной GNN N, существует ли вход, при котором выход положителен?
• Верификация спецификации: Удовлетворяет ли GNN данной логической спецификации φ?
• Проверка эквивалентности: Эквивалентны ли две GNN на всех входах?

Архитектура логики K#

Синтаксис

φ ::= p | ¬φ | φ ∨ φ | ξ ≥ 0
ξ ::= c | 1φ | #φ | ξ + ξ | c × ξ

Семантика

• 1φ: значение 1, если φ истинно, иначе 0
• #φ: подсчёт количества преемников, удовлетворяющих φ
• Линейные выражения: поддержка сложения и скалярного умножения

Ключевые характеристики

1. Выразительная способность: Логика K# содержит градуированную модальную логику (GML) в качестве подмножества
2. Соответствие: Существует двусторонний перевод за полиномиальное время с truncReLU-GNN
3. Ограничения подсчёта: Способность выражать сложные отношения подсчёта и операции агрегирования

Соответствие GNN-K#

От K# к GNN

tr(xi = 1) = xi
tr(¬φ) = 1 - truncReLU(tr(φ))
tr(φ ∧ ψ) = truncReLU(tr(φ) + tr(ψ) - 1)
tr(#φ) = agg(tr(φ))

От GNN к K#

tr'(truncReLU(ϑ)) = 1tr'(ϑ)≥1
tr'(agg(ϑ)) = #(tr'(ϑ) ≥ 1)

Алгоритм выполнимости

Основы QFBAPA

Использование свободной от кванторов булевой алгебры и арифметики Пресбургера (QFBAPA) для обработки ограничений подсчёта:

• Техника диаграмм Венна: Преобразование выражений множеств в переменные областей
• Граница Каратеодори: Доказательство того, что достаточно рассмотреть полиномиальное количество ненулевых областей
• NP-сложность: Проблема выполнимости QFBAPA находится в NP

Табличный алгоритм K#

процедура satK#(Γ)
  обработка булевых правил и конструкций 1φ
  извлечение ограничений линейных неравенств S
  предположение ненулевых областей B ⊆ {0,1}d, |B| ≤ 2d log₂(4d)
  замена #ψᵢ на ∑ρ∈B|ρᵢ=1 sρ
  проверка выполнимости QFPA
  рекурсивная верификация различных областей

Экспериментальная установка

Теоретическая верификация

Статья в основном проводит теоретический анализ через конструктивные доказательства:

1. Корректность: Корректность и полнота алгоритма
2. Сложность: Границы временной и пространственной сложности
3. Выразительная способность: Отношения выразительной способности различных логических фрагментов

Результаты сложности

Экспериментальные результаты

Основные теоретические результаты

Отношения выразительной способности

• cr(G,u) = cr(G',u') ⟺ G,u и G',u' удовлетворяют одним и тем же формулам GML
• GML ⊆ K# ⊆ FOC₂
• K# строго сильнее FO

Границы сложности

1. Выполнимость K#: PSPACE-полная
2. Верификация truncReLU-GNN: PSPACE-полная
3. Верификация ReLU-GNN: NEXPTIME-полная
4. Глобальное чтение: Приводит к неразрешимости (случай неориентированных графов)

Эффективность алгоритма

• Пространственная сложность: Полиномиальное пространство
• Количество областей: Максимум 2d log₂(4d) ненулевых областей
• Затраты на перевод: Полиномиальное время (случай целочисленных весов)

Технические идеи

Связь с Вейсфейлером-Леманом

• Алгоритм уточнения цвета захватывает существенный паттерн вычислений GNN
• Иерархия k-WL соответствует выразительной способности GNN различных порядков
• Модальная логика предоставляет естественный язык для описания этой иерархии

Обработка ограничений подсчёта

• QFBAPA предоставляет эффективную базу для обработки операций агрегирования
• Техника диаграмм Венна упрощает сложные ограничения подсчёта до линейного программирования
• Граница Каратеодори гарантирует полиномиальную пространственную сложность алгоритма

Связанные работы

Теоретические основы GNN

• Выразительная способность: Xu и др. (2019), Morris и др. (2019) установили связи между GNN и тестом WL
• Логическая характеризация: Barceló и др. (2020) впервые установили соответствие между GNN и логикой
• Методы верификации: Benedikt и др. (2024) предложили процедуры решения, но без единой базы

Верификация модальной логики

• Традиционные методы: Процедуры решения модальной логики, основанные на табличных методах
• Расширения подсчёта: Алгоритмы выполнимости для градуированной модальной логики
• Теория сложности: Анализ сложности различных фрагментов модальной логики

Верификация нейронных сетей

• SMT-методы: Использование SMT-решателей для верификации свойств нейронных сетей
• Абстрактная интерпретация: Анализ поведения сети через абстрактные области
• Символическое выполнение: Символическое исследование путей выполнения сети

Заключение и обсуждение

Основные выводы

1. Теоретическое единство: Установление единой теоретической базы для GNN, теста WL и логических систем
2. Алгоритмический вклад: Предоставление эффективного алгоритма верификации GNN с оптимальной сложностью
3. Выразительная способность: Логика K# точно захватывает вычислительную способность truncReLU-GNN
4. Разделение сложности: Различные функции активации приводят к значительно различающейся сложности верификации

Ограничения

1. Ограничения функций активации: Основные результаты сосредоточены на truncReLU, случай ReLU более сложен
2. Проблемы квантификации: Рациональные веса требуют экспоненциально больших общих знаменателей
3. Сложность реализации: Практическая реализация алгоритма всё ещё сталкивается с проблемами эффективности
4. Область применения: Основное внимание уделяется задачам классификации узлов, задачи на уровне графов требуют дополнительного рассмотрения

Направления будущих исследований

1. Расширение функций активации: Исследование методов верификации для более общих функций активации
2. Оптимизация алгоритма: Улучшение практической производительности и масштабируемости алгоритма
3. Разработка инструментов: Создание практических инструментов верификации GNN
4. Расширение приложений: Распространение на более широкий спектр архитектур GNN и типов задач

Глубокая оценка

Преимущества

1. Теоретическая глубина: Установление глубоких теоретических связей, заполнение важного теоретического пробела
2. Методологическая инновация: Искусное проектирование логики K#, балансирующее выразительную способность и разрешимость
3. Элегантность алгоритма: Естественное и эффективное сочетание табличных методов и рассуждений QFBAPA
4. Полнота результатов: Предоставление полного анализа сложности и доказательства соответствия
5. Педагогическая ценность: Как лекционные заметки, структурированы ясно и подходят для обучения и преподавания

Недостатки

1. Отсутствие экспериментальной верификации: Нехватка практической экспериментальной верификации и оценки производительности
2. Недостаток деталей реализации: Недостаточное обсуждение конкретной реализации алгоритма и стратегий оптимизации
3. Отсутствие прикладных примеров: Нехватка конкретных сценариев применения и тематических исследований
4. Отсутствие инструментальной поддержки: Отсутствие доступного инструмента верификации или прототипной системы

Влияние

1. Теоретический вклад: Установление прочной теоретической базы для области верификации GNN
2. Методологическое вдохновение: Предоставление важного методологического руководства для последующих исследований
3. Образовательная ценность: Как отличный учебный материал, способствует подготовке кадров в области
4. Практические перспективы: Хотя теоретически ориентирована, указывает направление для разработки практических инструментов

Применимые сценарии

1. Критичные по безопасности системы: Приложения GNN, требующие строгой верификации
2. Теоретические исследования: Теоретический анализ выразительной способности и сложности GNN
3. Обучение и подготовка: Преподавание графовых нейронных сетей и верификации логики
4. Разработка инструментов: Теоретическая база для разработки инструментов верификации GNN

Библиография

Статья цитирует 65 важных работ, охватывающих:

• Теоретические основы GNN (Grohe 2021, Barceló et al. 2020)
• Тест Вейсфейлера-Лемана (Morris et al. 2019, Xu et al. 2019)
• Модальная логика (Blackburn et al. 2001, Tobies 1999)
• Теория сложности (Grädel et al. 1997, Kuncak and Rinard 2007)
• Верификация нейронных сетей (Benedikt et al. 2024, Haase and Zetzsche 2019)

Общая оценка: Это отличная статья, сочетающая теоретическую глубину и педагогическую ценность. Она не только решает важные теоретические проблемы верификации GNN, но и закладывает прочную основу для последующих исследований и практических приложений. Хотя экспериментальная верификация отсутствует, значимость её теоретического вклада неоспорима.