Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats
Veeti Ahvonen, Damian Heiman, Antti Kuusisto, Carsten Lutz
TL;DR
This work provides precise logical characterizations of recurrent GNNs under floating-point and real arithmetic. It proves that $GNN[F]$ is expressively equivalent to the counting modal logic $GMSC$, while $GNN[ℝ]$ is equivalent to the infinitary $ω$-GML, with absolute (background-free) characterizations under natural arithmetic assumptions and connections to distributed automata CMPA/FCMPA. Relative to MSO, the floats and reals yield the same expressive power for MSO-expressible properties, with both variants aligning with a finitary $GMSC$ characterization. By linking GNNs with automata and MSO via tree automata and unraveling, the paper provides a robust framework for comparing recurrent GNNs to classical logical formalisms and circuit-like models. The results clarify when float-based GNNs suffice to capture MSO-expressible properties and establish a unified view of recurrent GNN expressivity across arithmetic regimes and acceptance conditions.
Abstract
In pioneering work from 2019, Barceló and coauthors identified logics that precisely match the expressive power of constant iteration-depth graph neural networks (GNNs) relative to properties definable in first-order logic. In this article, we give exact logical characterizations of recurrent GNNs in two scenarios: (1) in the setting with floating-point numbers and (2) with reals. For floats, the formalism matching recurrent GNNs is a rule-based modal logic with counting, while for reals we use a suitable infinitary modal logic, also with counting. These results give exact matches between logics and GNNs in the recurrent setting without relativising to a background logic in either case, but using some natural assumptions about floating-point arithmetic. Applying our characterizations, we also prove that, relative to graph properties definable in monadic second-order logic (MSO), our infinitary and rule-based logics are equally expressive. This implies that recurrent GNNs with reals and floats have the same expressive power over MSO-definable properties and shows that, for such properties, also recurrent GNNs with reals are characterized by a (finitary!) rule-based modal logic. In the general case, in contrast, the expressive power with floats is weaker than with reals. In addition to logic-oriented results, we also characterize recurrent GNNs, with both reals and floats, via distributed automata, drawing links to distributed computing models.