Recurrent graph neural networks connected to verifiable logical formulas

Recurrent GraphNeural NetworkswithSet-BasedAggregation

Artificial Intelligence

Summary

This paper studies a special kind of neural networks called recurrent graph neural networks that process information by passing messages repeatedly until they stabilize. Unlike past work, the authors focus on networks that use set-based aggregation instead of counting, which lets them find clear logical formulas representing what the networks do. They show these networks correspond exactly to a well-studied class of logical properties that can be checked from the network’s weights, without needing extra signals or guesses. This connection means that for networks meeting their conditions, one can explain and verify their behavior using symbolic logic.

What this means in practice

  • For graph machine learning engineers: Confirm stability and correctness of recurrent graph neural network models by checking their weights against known logical conditions.
  • For formal verification teams: Translate certain recurrent graph neural networks into logical formulas for easier symbolic verification of safety and reachability properties.

A theory result. No direct application yet.

Authors

Blai Bonet

Abstract

Recurrent GNNs iterate message passing to convergence, and their logical characterizations to date rely on multi-set aggregation, graded (counting) logics, and halting or acceptance conditions that cannot be verified from the network's parameters. We study recurrent GNNs with set-based aggregation and identify sufficient conditions checkable from the weights for networks to compile into formulas and formulas into networks. The main result is an effective, two-directional equivalence between a class of networks and the Boolean closure of reachability and safety properties, the fragment B$Σ^{\circ}_1$ of the modal $μ$-calculus. The fragment is not an artifact: it is the exact expressive level of stabilization over finite vocabulary, which supports fixed points of a single polarity and Boolean combinations thereof, but not the composition of fixed points of opposite polarities. The correspondence needs no counting logic, no external halting signal, and no non-effective acceptance condition, yielding a verifiable path from weights to symbolic explanations for networks meeting the conditions.
View PDFOpen arXiv