Lecture Notes on Verifying Graph Neural Networks
This work addresses verification challenges for graph neural networks, which is an incremental contribution to formal methods in machine learning.
The authors tackled the problem of verifying graph neural networks by developing a modal logic with counting modalities in linear inequalities, and they described an algorithm for its satisfiability problem based on extended tableau methods.
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.