Halting Recurrent GNNs and the Graded $μ$-Calculus
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909734772146176 |
|---|---|
| author | Bollen, Jeroen Bussche, Jan Van den Vansummeren, Stijn Virtema, Jonni |
| author_facet | Bollen, Jeroen Bussche, Jan Van den Vansummeren, Stijn Virtema, Jonni |
| contents | Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for recurrent GNNs. We prove that our halting model can express all node classifiers definable in graded modal mu-calculus, even for the standard GNN variant that is oblivious to the graph size. To prove our main result, we develop a new approximate semantics for graded mu-calculus, which we believe to be of independent interest. We leverage this new semantics into a new model-checking algorithm, called the counting algorithm, which is oblivious to the graph size. In a final step we show that the counting algorithm can be implemented on a halting recurrent GNN. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_11050 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Halting Recurrent GNNs and the Graded $μ$-Calculus Bollen, Jeroen Bussche, Jan Van den Vansummeren, Stijn Virtema, Jonni Machine Learning Artificial Intelligence Logic in Computer Science Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for recurrent GNNs. We prove that our halting model can express all node classifiers definable in graded modal mu-calculus, even for the standard GNN variant that is oblivious to the graph size. To prove our main result, we develop a new approximate semantics for graded mu-calculus, which we believe to be of independent interest. We leverage this new semantics into a new model-checking algorithm, called the counting algorithm, which is oblivious to the graph size. In a final step we show that the counting algorithm can be implemented on a halting recurrent GNN. |
| title | Halting Recurrent GNNs and the Graded $μ$-Calculus |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2505.11050 |