2025-11-21T04:31:15.286585

Lecture Notes on Verifying Graph Neural Networks

Schwarzentruber

In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic.

academic

그래프 신경망 검증에 관한 강의노트

기본정보

논문ID: 2510.11617
제목: Lecture Notes on Verifying Graph Neural Networks
저자: François Schwarzentruber (ENS de Lyon)
분류: cs.LO (컴퓨터과학의 논리), cs.LG (기계학습)
발표시간: 2025년 10월 14일
논문링크: https://arxiv.org/abs/2510.11617

초록

본 강의노트는 먼저 그래프 신경망, Weisfeiler-Lehman 테스트와 1차 논리, 계층적 양상논리 등 논리체계 간의 연관성을 검토한다. 이후 선형 부등식에서 계수 양상이 나타나는 양상논리를 제시하여 그래프 신경망의 검증 작업을 해결한다. 이 논리의 충족가능성 문제에 대한 알고리즘을 기술하며, 이 알고리즘은 전통적인 양상논리의 표 방법에서 영감을 받았으며, 양자화자 자유 단편 부울 대수와 Presburger 산술의 추론을 확장한다.

연구 배경 및 동기

문제 배경

그래프 신경망(GNNs)은 소셜 네트워크 추천, 지식 그래프, 화학 분자 분석, 신약 발견 등 다양한 분야에 광범위하게 적용되고 있다. 그러나 GNN의 검증 문제는 다음과 같은 중대한 도전에 직면해 있다:

표현 능력 제한: GNN의 표현 능력은 1-WL(Weisfeiler-Lehman) 테스트에 의해 제한되며, 특정 비동형 그래프를 구별할 수 없다
검증 작업의 복잡성: GNN이 안전성, 정확성 등 특정 사양을 만족하는지 검증해야 한다
이론적 기초 부족: GNN의 동작을 기술하고 검증하기 위한 체계적인 논리 프레임워크가 부족하다

연구 동기

실제 필요성: 안전 관련 애플리케이션에서 GNN의 신뢰성과 정확성을 보장해야 한다
이론적 공백: 기존 검증 방법은 통일된 논리 이론적 기초가 부족하다
기술적 도전: GNN의 집계 연산과 계수 제약을 처리해야 한다

핵심 기여

이론적 연관성 확립: GNN, Weisfeiler-Lehman 테스트와 논리체계(FO, FOC, GML) 간의 심층적 연관성을 체계적으로 설명
K# 논리 제시: GNN의 계수 및 집계 연산을 표현할 수 있는 새로운 양상논리 K# 설계
알고리즘 설계: 표 방법과 QFBAPA 추론에 기반한 K# 논리 충족가능성 문제의 PSPACE 알고리즘 개발
복잡성 분석: 서로 다른 활성화 함수 하에서 GNN 검증 문제의 계산 복잡성 경계 증명
실용적 프레임워크: GNN 검증 작업을 논리 충족가능성 문제로 축약하는 완전한 프레임워크 제공

방법 상세 설명

작업 정의

GNN 검증의 핵심 작업은 다음을 포함한다:

충족가능성: 주어진 GNN N에 대해 출력이 양수인 입력이 존재하는가?
사양 검증: GNN이 주어진 논리 사양 φ를 만족하는가?
동등성 검사: 두 GNN이 모든 입력에서 동등한가?

K# 논리 구조

구문 정의

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

의미 정의

1φ: φ가 참이면 값은 1, 거짓이면 0
#φ: φ를 만족하는 후속 노드의 개수 계산
선형 표현식: 덧셈과 스칼라 곱셈 지원

주요 특성

표현 능력: K# 논리는 계층적 양상논리(GML)를 부분집합으로 포함
대응 관계: truncReLU-GNN과의 다항식 시간 양방향 변환 존재
계수 제약: 복잡한 계수 관계와 집계 연산 표현 가능

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 기초

양자화자 자유 부울 대수와 Presburger 산술(QFBAPA)을 사용하여 계수 제약 처리:

Venn 다이어그램 기법: 집합 표현식을 영역 변수로 변환
Carathéodory 경계: 다항식 개수의 영점이 아닌 영역만 고려하면 됨을 증명
NP 복잡성: QFBAPA 충족가능성 문제는 NP 내에 있음

K# 표 알고리즘

procedure satK#(Γ)
  부울 규칙과 1φ 구성 처리
  선형 부등식 제약 S 추출
  영점이 아닌 영역 B ⊆ {0,1}d 추측, |B| ≤ 2d log₂(4d)
  #ψᵢ를 ∑ρ∈B|ρᵢ=1 sρ로 대체
  QFPA 충족가능성 검사
  각 영역에 대해 재귀적으로 검증