Graph Learning via Logic-Based Weisfeiler-Leman Variants and Tabularization

Antti Kuusisto; Magdalena Ortiz; Mantas \v{S}imkus; Matias Selin; Reijo Jaakkola; Tomi Janhunen

arxiv: 2508.10651 · v3 · pith:L7XWXO2Bnew · submitted 2025-08-14 · 💻 cs.LG

Graph Learning via Logic-Based Weisfeiler-Leman Variants and Tabularization

Reijo Jaakkola , Tomi Janhunen , Antti Kuusisto , Magdalena Ortiz , Matias Selin , Mantas \v{S}imkus This is my paper

Pith reviewed 2026-05-25 07:42 UTC · model grok-4.3

classification 💻 cs.LG

keywords graph classificationWeisfeiler-Leman algorithmtabular datagraph neural networksexpressive powerbisimulation gamelogic-based methodsgraph transformers

0 comments

The pith

Logic-based Weisfeiler-Leman variants turn graphs into tabular features that match GNN and transformer accuracy on classification tasks up to 40,000 samples.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops new variants of the Weisfeiler-Leman algorithm by altering its underlying logical framework and uses them to convert graph structures into tabular data for standard machine learning classifiers. It provides a theoretical characterization of the variants' expressive power through a generalized bisimulation game that accounts for generalized quantifiers. Experiments across 14 datasets show that the resulting tabular approach reaches predictive performance comparable to graph neural networks and graph transformers. The method requires no GPU and far less hyperparameter tuning, delivering a 5-20 times speedup even when its own tuning time is counted.

Core claim

By modifying the logical basis of the Weisfeiler-Leman procedure, the authors obtain graph-to-table transformations whose features support classification accuracy that generally equals that of GNNs and graph transformers on the tested datasets while eliminating the need for specialized hardware and extensive tuning.

What carries the argument

Logic-based Weisfeiler-Leman variants derived from changes to the logical framework, with expressive power characterized by a novel generalization of the bisimulation game for generalized quantifiers.

If this is right

Graph classification on medium-sized datasets becomes feasible on ordinary CPUs without specialized hardware.
Hyperparameter search effort drops substantially compared with neural graph models.
The approach scales in wall-clock time even when full tuning budgets are included for every method.
Performance parity holds across application domains represented in the 14 datasets.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same tabularization pipeline could be tested on graph regression or link-prediction tasks to check whether the logic-based features transfer.
Combining the method with sampling or sketching techniques might extend it to graphs larger than 40,000 nodes.
The generalized bisimulation characterization could be used to diagnose precisely which graph properties the tabular models capture and which they miss.

Load-bearing premise

The tabular features generated by the new logic-based WL variants carry enough discriminative power, as measured by the generalized bisimulation game, to explain the observed classification accuracy on the 14 datasets.

What would settle it

Finding a dataset of graphs where the new WL variants fail to distinguish pairs that standard GNNs or transformers can separate, resulting in measurably lower tabular-model accuracy.

Figures

Figures reproduced from arXiv: 2508.10651 by Antti Kuusisto, Magdalena Ortiz, Mantas \v{S}imkus, Matias Selin, Reijo Jaakkola, Tomi Janhunen.

read the original abstract

We present a novel approach for graph classification based on tabularizing graph data via new variants of the Weisfeiler-Leman algorithm and then applying methods for tabular data. The variants are obtained by modifying the underlying logical framework, and we establish a precise theoretical characterization of their expressive power using a novel generalization of the bisimulation game for generalized quantifiers. We then test our method on 14 datasets that span a range of application domains. The experiments demonstrate that on datasets with up to 40 000 samples, our approach generally matches the predictive performance of graph neural networks and graph transformers, without requiring a GPU or extensive hyperparameter tuning. Even when our method's tuning time is included and the baselines' is not, our method is 5-20 times faster. When tuning time is included for all methods, the gap is significantly greater in favour of our method.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Logic-based WL variants turn graphs into tabular data with competitive accuracy and speed, but the bisimulation game does not show why the features separate the labels on the 14 datasets.

read the letter

Logic-based WL variants turn graphs into tabular data with competitive accuracy and speed, but the bisimulation game does not show why the features separate the labels on the 14 datasets. The paper modifies the logical framework behind Weisfeiler-Leman to generate new invariants, converts the output into a table, and runs standard tabular classifiers. It also gives a generalized bisimulation game for quantifiers to characterize exactly what each variant can distinguish. Those two pieces are new and do not reduce to the usual WL or GNN literature. The experiments report that the method matches GNN and graph transformer accuracy on 14 datasets up to 40 000 samples, runs 5-20 times faster when tuning time is included for the new method only, and needs no GPU. If the numbers hold, this is a practical option for settings without heavy hardware. The main gap is between the theory and the results. The game tells us the graph properties the features can separate in principle, yet the abstract supplies no argument or check that those properties are the ones that determine the class labels on the chosen datasets. If the labels rely on patterns outside the logic fragment, the accuracy would need a different explanation. The abstract also gives no information on baseline implementations, hyperparameter ranges, or statistical tests, so the empirical support remains moderate. This work is for graph ML users who want simpler, hardware-light pipelines and for logicians interested in descriptive complexity on graphs. A reader who wants to test a non-neural route on mid-sized data would get immediate value from the method and the characterization. The paper is coherent on its own terms and the claims are testable, so it deserves a serious referee.

Referee Report

2 major / 1 minor

Summary. The paper proposes a graph classification method that tabularizes graphs using novel Weisfeiler-Leman variants derived from modified logical frameworks, then applies standard tabular learners. It provides a theoretical characterization of the variants' expressive power via a generalized bisimulation game for generalized quantifiers. Experiments on 14 datasets (up to 40k samples) claim that the approach matches the predictive performance of GNNs and graph transformers while being 5-20x faster (even including tuning) and requiring no GPU or heavy hyperparameter search.

Significance. If the results hold, the work offers an efficient, GPU-free alternative for graph classification that combines logical feature generation with tabular methods. The generalized bisimulation game provides a precise expressivity analysis that is a clear theoretical strength. The approach is notable for avoiding extensive tuning and for its potential interpretability via the underlying logic.

major comments (2)

[Experiments] Experiments section: the central claim that the method 'generally matches' GNN and graph transformer performance on 14 datasets lacks any description of baseline implementations, exact data splits, number of runs, or statistical significance tests; without these the empirical support for the performance-matching assertion remains only moderately grounded.
[Theoretical characterization] Theoretical characterization (generalized bisimulation game): the game precisely defines what the new quantifier-based logics can distinguish, yet the manuscript supplies no argument or auxiliary experiment showing that the class labels on the chosen 14 datasets are determined by properties expressible in these logics rather than by higher-order or global patterns outside the fragment; this leaves the link between the claimed expressive power and the observed accuracy unaddressed.

minor comments (1)

[Abstract] Abstract: the speed-up claim ('5-20 times faster') should explicitly state the hardware baseline and whether baseline tuning times were measured under identical conditions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive report and positive assessment of the work's significance. We address each major comment below with concrete plans for revision where appropriate.

read point-by-point responses

Referee: [Experiments] Experiments section: the central claim that the method 'generally matches' GNN and graph transformer performance on 14 datasets lacks any description of baseline implementations, exact data splits, number of runs, or statistical significance tests; without these the empirical support for the performance-matching assertion remains only moderately grounded.

Authors: We agree that these details should have been included. In the revised manuscript we will expand the Experiments section to specify: (i) baseline implementations (PyTorch Geometric defaults for GNNs with the exact architectures and hyperparameters from the original papers; graph transformers via the implementations in the cited works with their reported settings); (ii) exact data splits (the standard splits or 10-fold CV procedure supplied with each of the 14 datasets); (iii) number of runs (five independent runs per method with distinct random seeds, reporting mean and standard deviation); and (iv) statistical significance (paired Wilcoxon signed-rank tests across the 14 datasets with p-values). These additions will be placed in a new subsection on experimental protocol. revision: yes
Referee: [Theoretical characterization] Theoretical characterization (generalized bisimulation game): the game precisely defines what the new quantifier-based logics can distinguish, yet the manuscript supplies no argument or auxiliary experiment showing that the class labels on the chosen 14 datasets are determined by properties expressible in these logics rather than by higher-order or global patterns outside the fragment; this leaves the link between the claimed expressive power and the observed accuracy unaddressed.

Authors: The generalized bisimulation game gives a precise characterization of the fragment. We acknowledge that the manuscript does not contain an auxiliary experiment or formal argument proving that the dataset labels are determined exclusively by properties inside this fragment. The performance parity with more expressive models supplies only indirect support. In revision we will add a short discussion paragraph after the theoretical section that (a) recalls the characterization, (b) notes that matching accuracy on standard benchmarks is consistent with the relevant distinctions lying inside the fragment, and (c) explicitly states the limitation that we cannot exclude contributions from higher-order patterns on every dataset. No new experiments will be added. revision: partial

Circularity Check

0 steps flagged

No circularity in derivation chain

full rationale

The paper introduces logic-based WL variants, establishes their expressive power via a novel generalized bisimulation game characterization, and reports empirical performance on 14 datasets. The theoretical characterization is presented as an independent logical analysis of what the variants can distinguish; the performance claims rest on direct experimental comparison rather than any reduction of accuracy to fitted parameters, self-citations, or definitional equivalence. No equations or load-bearing steps in the provided abstract or description equate a claimed prediction to its own inputs by construction, and the reader's assessment of score 2 aligns with the absence of any self-citation that carries the central result.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only access prevents exhaustive enumeration; the approach rests on standard assumptions of graph isomorphism testing and supervised classification plus the novel game characterization.

axioms (1)

domain assumption The generalized bisimulation game correctly captures the expressive power of the logic-modified Weisfeiler-Leman variants.
Invoked to establish the theoretical characterization mentioned in the abstract.

pith-pipeline@v0.9.0 · 5701 in / 1230 out tokens · 23031 ms · 2026-05-25T07:42:46.211343+00:00 · methodology

discussion (0)

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Model Comparison Games for Generalized Quantifiers
math.LO 2026-05 unverdicted novelty 7.0

Introduces two model comparison games characterizing separability by first-order formulas with generalized quantifiers.
The Polynomial Counting Capabilities of Message Passing Neural Networks
cs.LG 2026-05 unverdicted novelty 7.0

MPNNs with mean aggregations can check polynomial counting constraints from graded modal logic extensions on graphs, under conditions for local and nested cases.

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages · cited by 2 Pith papers · 1 internal anchor

[1]

Kostylev, Mikaël Monet, Jorge Pérez, Juan L

Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan L. Reutter, and Juan-Pablo Silva. The expressive power of graph neural networks as a query language. SIGMOD Rec., 49(2):6–17, December 2020.doi:10.1145/3442322.3442324

work page doi:10.1145/3442322.3442324 2020
[2]

Jennings, P

Leo Breiman. Random forests.Machine Learning, 45(1):5–32, 2001.doi:10.1023/A: 1010933404324

work page doi:10.1023/a: 2001
[3]

Brewka, T

G. Brewka, T. Eiter, and M. Truszczynski. Answer set programming at a glance. Communications of the ACM, 54(12):92–103, 2011

work page 2011
[4]

A note on graded modal logic

Maarten de Rijke. A note on graded modal logic. Studia Logica: An International Journal for Symbolic Logic, 64(2):271–283, 2000

work page 2000
[5]

Benchmarkinggraphneuralnetworks

Vijay Prakash Dwivedi, Chaitanya K Joshi, Anh Tuan Luu, Thomas Laurent, Yoshua Bengio, andXavierBresson. Benchmarkinggraphneuralnetworks. Journal of Machine Learning Research, 24(43):1–48, 2023

work page 2023
[6]

A fair comparison ofgraphneuralnetworksforgraphclassification

Federico Errica, Marco Podda, Davide Bacciu, and Alessio Micheli. A fair comparison ofgraphneuralnetworksforgraphclassification. In International Conference on Learn- ing Representations, 2020. URL: https://openreview.net/forum?id=HygDF6NFPB

work page 2020
[7]

Matthias Fey and Jan E. Lenssen. Fast graph representation learning with PyTorch Geometric. InICLR Workshop on Representation Learning on Graphs and Manifolds, 2019

work page 2019
[8]

In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

Martin Grohe. The logic of graph neural networks. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–17, 2021.doi:10.1109/ LICS52264.2021.9470677. 13

work page arXiv 2021
[9]

Short Boolean formulas as explanations in practice

Reijo Jaakkola, Tomi Janhunen, Antti Kuusisto, Masood Feyzbakhsh Rankooh, and Miikka Vilander. Short Boolean formulas as explanations in practice. InJELIA 2023, pages 90–105. Springer, 2023

work page 2023
[10]

Kipf and Max Welling

Thomas N. Kipf and Max Welling. Semi-supervised classification with graph con- volutional networks. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. Open- Review.net, 2017. URL: https://openreview.net/forum?id=SJU4ayYgl

work page 2017
[11]

A survey on graph kernels

Nils M Kriege, Fredrik D Johansson, and Christopher Morris. A survey on graph kernels. Applied Network Science, 5:1–42, 2020

work page 2020
[12]

TUDataset: A collection of benchmark datasets for learning with graphs

Christopher Morris, Nils M. Kriege, Franka Bause, Kristian Kersting, Petra Mutzel, and Marion Neumann. Tudataset: A collection of benchmark datasets for learning with graphs. CoRR, abs/2007.08663, 2020. URL: https://arxiv.org/abs/2007.08663, arXiv:2007.08663

work page internal anchor Pith review arXiv 2007
[13]

Graded modal logic and counting bisimulation

Martin Otto. Graded modal logic and counting bisimulation. arXiv preprint arXiv:1910.00039, 2023. URL: https://arxiv.org/abs/1910.00039

work page arXiv 1910
[14]

Pedregosa, G

F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blon- del, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825–2830, 2011

work page 2011
[15]

The graph neural network model.IEEE Transactions on Neural Networks, 20(1):61–80, 2009.doi:10.1109/TNN.2008.2005605

Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model.IEEE Transactions on Neural Networks, 20(1):61–80, 2009.doi:10.1109/TNN.2008.2005605

work page doi:10.1109/tnn.2008.2005605 2009
[16]

Borgwardt

Nino Shervashidze, Pascal Schweitzer, Erik Jan van Leeuwen, Kurt Mehlhorn, and Karsten M. Borgwardt. Weisfeiler-lehman graph kernels.Journal of Machine Learning Research, 12:2539–2561, 2011. URL: https://dl.acm.org/doi/10.5555/1953048. 2078187, doi:10.5555/1953048.2078187

work page doi:10.5555/1953048 2011
[17]

Grakel: A graph kernel library in python.Journal of Machine Learning Research, 21(54):1–5, 2020

GiannisSiglidis, GiannisNikolentzos, StratisLimnios, ChristosGiatsidis, Konstantinos Skianis, and Michalis Vazirgiannis. Grakel: A graph kernel library in python.Journal of Machine Learning Research, 21(54):1–5, 2020

work page 2020
[18]

Boris Weisfeiler and Andrei A. Lehman. A Reduction of a Graph to a Canonical Form and an Algebra Arising During This Reduction.Nauchno-Technicheskaya Informatsia, Ser. 2(N9):12–16, 1968

work page 1968
[19]

Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. A comprehensive survey on graph neural networks. IEEE Trans- actions on Neural Networks and Learning Systems, 32:4–24, 2019. URL: https: //api.semanticscholar.org/CorpusID:57375753

work page 2019
[20]

How powerful are graph neural networks? In International Conference on Learning Representations, 2019

Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In International Conference on Learning Representations, 2019. URL: https://openreview.net/forum?id=ryGs6iA5Km

work page 2019
[21]

Graph neural networks

Yuyu Zhang, Xinshi Chen, Yuan Yang, Arun Ramamurthy, Bo Li, Yuan Qi, and Le Song. Graph neural networks. Deep Learning on Graphs, 2021. URL: https: //api.semanticscholar.org/CorpusID:211031569. 14 A Hyperparameter Setups In this section, we list the hyperparameters used for different methods. For GNNs, the amount of epochs was optimized from the range1 − ...

work page 2021
[23]

If w ∈ M is the node over which the chosen pebble lies, the attacker then chooses a subsetX ⊆ N(w)of the neighbours of the nodew such that(N(w), X) ∈ Q

During each round, the attacker first selects one of the two pebbles and a modality ⟨Q⟩ ∈ Q. If w ∈ M is the node over which the chosen pebble lies, the attacker then chooses a subsetX ⊆ N(w)of the neighbours of the nodew such that(N(w), X) ∈ Q

work page
[24]

The defender may contest this choice by placing one pebble onto a node inP and the other onto a node inN(w), after which a new round begins with the attacker’s move

The attacker then chooses a subsetP ⊆ N(v) of the neighbours of the other pebble. The defender may contest this choice by placing one pebble onto a node inP and the other onto a node inN(w), after which a new round begins with the attacker’s move

work page
[25]

If the defender does not contest the choice ofP, he then chooses a subsetX ′ ⊆ N(v) of the neighbours of the nodev ∈ N under the other pebble such that(N(v), X′) ∈ Q and P ⊆ X ′

work page
[26]

The attacker now has two options. The first is to claim that the defender didn’t pick enough equivalence classes of nodes by moving one pebble onto a node inN(v) \ X ′, the other onto a node inX and taking the role of the defender, after which the next round starts with the attacker’s move. The second is to claim that the defender picked too many equivale...

work page
[27]

X ′) is chosen, the other player may contest the choice by moving one pebble onto a node in the contested set and the other onto a node in the complement N(w) \ X (resp

Whenever a setX (resp. X ′) is chosen, the other player may contest the choice by moving one pebble onto a node in the contested set and the other onto a node in the complement N(w) \ X (resp. N(v) \ X ′), then taking the role of the defender. The next round then starts with the attacker’s move

work page
[28]

If at any point a player must choose a subset but cannot do so, then that player loses

The attacker wins if, at the start of any round, the nodes the pebbles lay on do not satisfy the same proposition symbols. If at any point a player must choose a subset but cannot do so, then that player loses. An infinite-length game is always won by Player 2. In thed-round Q-bisimulation game, Player 2 is declared the winner if Player 1 has not won afte...

work page
[29]

Here M ⊔ N denotes the disjoint union ofM and N

N, v ⊩ φQ,d M⊔N,w. Here M ⊔ N denotes the disjoint union ofM and N. The structure of the proof is1. ⇒

work page
[30]

⇒ 3. ⇒ 1. Lemma 6. M, w ∼d Q N, v =⇒ M, w ≡d PL(Q) N, v. Proof. We show this by induction ond. First, we haveM, w ∼0 Q N, v =⇒ M, w ≡0 PL(Q) N, v since Player 2 winning in round 0 simply means that the nodesw and v satisfy the same proposition symbols. Assume now that M, w ∼d Q N, v =⇒ M, w ≡d PL(Q) N, v for some d ≥ 0 and every pair (M, w), (N, v) of poi...

work page
[31]

SinceN, v′ ⊩ ¬ψ, we havev′ ∈ X ′ \ P

Consider the first case. SinceN, v′ ⊩ ¬ψ, we havev′ ∈ X ′ \ P. Player 1 now simply moves a pebble ontov′, and Player 2 is forced to respond by moving the other pebble onto a nodew′ such that M, w′ ⊩ ψ. Player 1 thus wins the game

work page
[32]

SinceP ⊆ X ′, we havev′ /∈ P and thus N, v′ ≡d PL(Q) M, w′ for some w′ ∈ N(w)

Consider then the second case. SinceP ⊆ X ′, we havev′ /∈ P and thus N, v′ ≡d PL(Q) M, w′ for some w′ ∈ N(w). Hence M, w′ ⊩ ψ, so w′ ∈ X. Player 1 now moves one pebble onto v′ and the other ontow′ and becomes the defender. By the induction hypothesis, N, v′ ∼d Q M, w′, which means Player 1 thus has a winning strategy. Player 1 therefore has a winning stra...

work page
[33]

Let I := {φQ,d M⊔N,w′ | w′ ∈ X} ∪ {φQ,d M⊔N,v′ | v′ ∈ P }

In the first case Player 1 chooses a modality⟨Q⟩ ∈ Q, a subsetX ⊆ N(w) such that (N(w), X) ∈ Q, and a subsetP ⊆ N(v). Let I := {φQ,d M⊔N,w′ | w′ ∈ X} ∪ {φQ,d M⊔N,v′ | v′ ∈ P }. Because of the contestion rules,X must be closed under≡d PL(Q) and P cannot contain a node equivalent to a node inN(w). Hence ⟨Q⟩(W φ∈I φ) occurs in φQ,d+1 M⊔N,w and thus N, v ⊩ ⟨Q...

work page
[34]

Let I := {φQ,d M⊔N,v′ | v′ ∈ X} ∪ {φQ,d M⊔N,w′ | w′ ∈ P }

In the second case, Player 1 chooses a modality⟨Q⟩ ∈ Q , a subset X ⊆ N(v) such that (N(v), X) ∈ Q, and a subsetP ⊆ N(w). Let I := {φQ,d M⊔N,v′ | v′ ∈ X} ∪ {φQ,d M⊔N,w′ | w′ ∈ P }. Now N, v ⊩ ⟨Q⟩(W φ∈I φ) and hence we must have thatM, w ⊩ ⟨Q⟩(W φ∈I φ), because N, v ⊩ φQ,d M⊔N,w. The rest of the proof is similar to that of Case 1. Player 2 thus has a winni...

work page
[35]

Player 1 starts as theattacker and Player 2 as thedefender

The game begins with two pebbles placed on the nodesw and v respectively. Player 1 starts as theattacker and Player 2 as thedefender

work page
[36]

If Q is of widthn, he then choosesn subsets (Xi)1≤i≤n of the neighbours of the node such that(N(w), X1,

During each round, the attacker first selects a pebble that is placed on some nodew as well as a modality⟨Q⟩ ∈ Q. If Q is of widthn, he then choosesn subsets (Xi)1≤i≤n of the neighbours of the node such that(N(w), X1, . . . , Xn) ∈ Q and for eachXi he selects a subsetPi ⊆ N(v) of the neighbours of the other pebble. The defender may contest anyPi in the us...

work page
[37]

, X′ n) ∈ Q and Pi ⊆ X ′ i for all 1 ≤ i ≤ n

If the defender does not contest anyPi, he then chooses n subsets (X ′ i)1≤i≤n such that (N(v), X′ 1, . . . , X′ n) ∈ Q and Pi ⊆ X ′ i for all 1 ≤ i ≤ n

work page
[38]

The first is, for some1 ≤ i ≤ n, to move one pebble onto a node inN(v) \ X ′ i and the other onto a node inXi, then take the role of the defender

The attacker now has two options. The first is, for some1 ≤ i ≤ n, to move one pebble onto a node inN(v) \ X ′ i and the other onto a node inXi, then take the role of the defender. The second is, for some1 ≤ i ≤ n, to move a pebble onto a node in X ′ i, after which the defender responds by moving a pebble onto a node in eitherXi or Pi

work page
[39]

(X ′ i)1≤i≤n) of sets is chosen, the other player may contest any individualXi (resp

Whenever a tuple(Xi)1≤i≤n (resp. (X ′ i)1≤i≤n) of sets is chosen, the other player may contest any individualXi (resp. X ′ i) in the usual way by placing a pebble onto a node in the contested set and the other onto a node in the complementN(w) \ Xi (resp. N(v) \ X ′ i), then taking the role of the defender. The next round then starts with the attacker’s move

work page
[40]

behave similarly

The attacker wins if, at the start of any round, the nodes the pebbles lay on do not satisfy the same proposition symbols. If at any point a player must choose a subset but cannot do so, then that player loses. An infinite-length game is always won by Player 2. Lemma 9. Lemma 6 holds whenQ is a set of finite-width generalized modalities. Proof. The base c...

work page
[41]

Each member Q of Q is a Turing machine that computes the corresponding gen- eralized quantifier. (Note that we use the same symbol for the quantifier and the corresponding Turing machine.) This means that when given a pair(A, P) as in- put, Q decides whether it belongs to the corresponding generalized quantifier. Such generalized quantifiers are calledcomputable

work page
[42]

Such a function is called aneffective representationof Q

There exists a computable function f : N → Pfinite(Q), 22 where Pfinite(Q) is the set of all finite subsets ofQ, such thatf(N) is a representation of Q at width N. Such a function is called aneffective representationof Q. Example 15. Consider the set C := {∃≥k | k ∈ N} of all counting quantifiers. This set is effectively finite, because each quantifier∃≥k...

work page
[43]

Q-WL receives as an input a Kripke modelM and a depthd ∈ N

work page
[44]

We compute the maximum out-degree ofM and store it ask

work page
[45]

We can thus compute the finite set of computable quantifiersQ0 ⊆ Q associated with the effective representationf such that Q0 := f(k)

Because Q is effectively finite, it has an effective representationf : N → P f inite(Q). We can thus compute the finite set of computable quantifiersQ0 ⊆ Q associated with the effective representationf such that Q0 := f(k)

work page
[46]

We runQ0-WL on M and d. Note that if we consider a set of graphs, as we do in the experimental section of the paper, then the input to the algorithm has to be the disjoint union of those graphs (to get the maximum out-degree of all graphs). Alternatively, we could consider aset of graphs as an input to the algorithm and take the maximum out-degree of the ...

work page

[1] [1]

Kostylev, Mikaël Monet, Jorge Pérez, Juan L

Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan L. Reutter, and Juan-Pablo Silva. The expressive power of graph neural networks as a query language. SIGMOD Rec., 49(2):6–17, December 2020.doi:10.1145/3442322.3442324

work page doi:10.1145/3442322.3442324 2020

[2] [2]

Jennings, P

Leo Breiman. Random forests.Machine Learning, 45(1):5–32, 2001.doi:10.1023/A: 1010933404324

work page doi:10.1023/a: 2001

[3] [3]

Brewka, T

G. Brewka, T. Eiter, and M. Truszczynski. Answer set programming at a glance. Communications of the ACM, 54(12):92–103, 2011

work page 2011

[4] [4]

A note on graded modal logic

Maarten de Rijke. A note on graded modal logic. Studia Logica: An International Journal for Symbolic Logic, 64(2):271–283, 2000

work page 2000

[5] [5]

Benchmarkinggraphneuralnetworks

Vijay Prakash Dwivedi, Chaitanya K Joshi, Anh Tuan Luu, Thomas Laurent, Yoshua Bengio, andXavierBresson. Benchmarkinggraphneuralnetworks. Journal of Machine Learning Research, 24(43):1–48, 2023

work page 2023

[6] [6]

A fair comparison ofgraphneuralnetworksforgraphclassification

Federico Errica, Marco Podda, Davide Bacciu, and Alessio Micheli. A fair comparison ofgraphneuralnetworksforgraphclassification. In International Conference on Learn- ing Representations, 2020. URL: https://openreview.net/forum?id=HygDF6NFPB

work page 2020

[7] [7]

Matthias Fey and Jan E. Lenssen. Fast graph representation learning with PyTorch Geometric. InICLR Workshop on Representation Learning on Graphs and Manifolds, 2019

work page 2019

[8] [8]

In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

Martin Grohe. The logic of graph neural networks. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–17, 2021.doi:10.1109/ LICS52264.2021.9470677. 13

work page arXiv 2021

[9] [9]

Short Boolean formulas as explanations in practice

Reijo Jaakkola, Tomi Janhunen, Antti Kuusisto, Masood Feyzbakhsh Rankooh, and Miikka Vilander. Short Boolean formulas as explanations in practice. InJELIA 2023, pages 90–105. Springer, 2023

work page 2023

[10] [10]

Kipf and Max Welling

Thomas N. Kipf and Max Welling. Semi-supervised classification with graph con- volutional networks. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. Open- Review.net, 2017. URL: https://openreview.net/forum?id=SJU4ayYgl

work page 2017

[11] [11]

A survey on graph kernels

Nils M Kriege, Fredrik D Johansson, and Christopher Morris. A survey on graph kernels. Applied Network Science, 5:1–42, 2020

work page 2020

[12] [12]

TUDataset: A collection of benchmark datasets for learning with graphs

Christopher Morris, Nils M. Kriege, Franka Bause, Kristian Kersting, Petra Mutzel, and Marion Neumann. Tudataset: A collection of benchmark datasets for learning with graphs. CoRR, abs/2007.08663, 2020. URL: https://arxiv.org/abs/2007.08663, arXiv:2007.08663

work page internal anchor Pith review arXiv 2007

[13] [13]

Graded modal logic and counting bisimulation

Martin Otto. Graded modal logic and counting bisimulation. arXiv preprint arXiv:1910.00039, 2023. URL: https://arxiv.org/abs/1910.00039

work page arXiv 1910

[14] [14]

Pedregosa, G

F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blon- del, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825–2830, 2011

work page 2011

[15] [15]

The graph neural network model.IEEE Transactions on Neural Networks, 20(1):61–80, 2009.doi:10.1109/TNN.2008.2005605

Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model.IEEE Transactions on Neural Networks, 20(1):61–80, 2009.doi:10.1109/TNN.2008.2005605

work page doi:10.1109/tnn.2008.2005605 2009

[16] [16]

Borgwardt

Nino Shervashidze, Pascal Schweitzer, Erik Jan van Leeuwen, Kurt Mehlhorn, and Karsten M. Borgwardt. Weisfeiler-lehman graph kernels.Journal of Machine Learning Research, 12:2539–2561, 2011. URL: https://dl.acm.org/doi/10.5555/1953048. 2078187, doi:10.5555/1953048.2078187

work page doi:10.5555/1953048 2011

[17] [17]

Grakel: A graph kernel library in python.Journal of Machine Learning Research, 21(54):1–5, 2020

GiannisSiglidis, GiannisNikolentzos, StratisLimnios, ChristosGiatsidis, Konstantinos Skianis, and Michalis Vazirgiannis. Grakel: A graph kernel library in python.Journal of Machine Learning Research, 21(54):1–5, 2020

work page 2020

[18] [18]

Boris Weisfeiler and Andrei A. Lehman. A Reduction of a Graph to a Canonical Form and an Algebra Arising During This Reduction.Nauchno-Technicheskaya Informatsia, Ser. 2(N9):12–16, 1968

work page 1968

[19] [19]

Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. A comprehensive survey on graph neural networks. IEEE Trans- actions on Neural Networks and Learning Systems, 32:4–24, 2019. URL: https: //api.semanticscholar.org/CorpusID:57375753

work page 2019

[20] [20]

How powerful are graph neural networks? In International Conference on Learning Representations, 2019

Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In International Conference on Learning Representations, 2019. URL: https://openreview.net/forum?id=ryGs6iA5Km

work page 2019

[21] [21]

Graph neural networks

Yuyu Zhang, Xinshi Chen, Yuan Yang, Arun Ramamurthy, Bo Li, Yuan Qi, and Le Song. Graph neural networks. Deep Learning on Graphs, 2021. URL: https: //api.semanticscholar.org/CorpusID:211031569. 14 A Hyperparameter Setups In this section, we list the hyperparameters used for different methods. For GNNs, the amount of epochs was optimized from the range1 − ...

work page 2021

[22] [23]

If w ∈ M is the node over which the chosen pebble lies, the attacker then chooses a subsetX ⊆ N(w)of the neighbours of the nodew such that(N(w), X) ∈ Q

During each round, the attacker first selects one of the two pebbles and a modality ⟨Q⟩ ∈ Q. If w ∈ M is the node over which the chosen pebble lies, the attacker then chooses a subsetX ⊆ N(w)of the neighbours of the nodew such that(N(w), X) ∈ Q

work page

[23] [24]

The defender may contest this choice by placing one pebble onto a node inP and the other onto a node inN(w), after which a new round begins with the attacker’s move

The attacker then chooses a subsetP ⊆ N(v) of the neighbours of the other pebble. The defender may contest this choice by placing one pebble onto a node inP and the other onto a node inN(w), after which a new round begins with the attacker’s move

work page

[24] [25]

If the defender does not contest the choice ofP, he then chooses a subsetX ′ ⊆ N(v) of the neighbours of the nodev ∈ N under the other pebble such that(N(v), X′) ∈ Q and P ⊆ X ′

work page

[25] [26]

The attacker now has two options. The first is to claim that the defender didn’t pick enough equivalence classes of nodes by moving one pebble onto a node inN(v) \ X ′, the other onto a node inX and taking the role of the defender, after which the next round starts with the attacker’s move. The second is to claim that the defender picked too many equivale...

work page

[26] [27]

X ′) is chosen, the other player may contest the choice by moving one pebble onto a node in the contested set and the other onto a node in the complement N(w) \ X (resp

Whenever a setX (resp. X ′) is chosen, the other player may contest the choice by moving one pebble onto a node in the contested set and the other onto a node in the complement N(w) \ X (resp. N(v) \ X ′), then taking the role of the defender. The next round then starts with the attacker’s move

work page

[27] [28]

If at any point a player must choose a subset but cannot do so, then that player loses

The attacker wins if, at the start of any round, the nodes the pebbles lay on do not satisfy the same proposition symbols. If at any point a player must choose a subset but cannot do so, then that player loses. An infinite-length game is always won by Player 2. In thed-round Q-bisimulation game, Player 2 is declared the winner if Player 1 has not won afte...

work page

[28] [29]

Here M ⊔ N denotes the disjoint union ofM and N

N, v ⊩ φQ,d M⊔N,w. Here M ⊔ N denotes the disjoint union ofM and N. The structure of the proof is1. ⇒

work page

[29] [30]

⇒ 3. ⇒ 1. Lemma 6. M, w ∼d Q N, v =⇒ M, w ≡d PL(Q) N, v. Proof. We show this by induction ond. First, we haveM, w ∼0 Q N, v =⇒ M, w ≡0 PL(Q) N, v since Player 2 winning in round 0 simply means that the nodesw and v satisfy the same proposition symbols. Assume now that M, w ∼d Q N, v =⇒ M, w ≡d PL(Q) N, v for some d ≥ 0 and every pair (M, w), (N, v) of poi...

work page

[30] [31]

SinceN, v′ ⊩ ¬ψ, we havev′ ∈ X ′ \ P

Consider the first case. SinceN, v′ ⊩ ¬ψ, we havev′ ∈ X ′ \ P. Player 1 now simply moves a pebble ontov′, and Player 2 is forced to respond by moving the other pebble onto a nodew′ such that M, w′ ⊩ ψ. Player 1 thus wins the game

work page

[31] [32]

SinceP ⊆ X ′, we havev′ /∈ P and thus N, v′ ≡d PL(Q) M, w′ for some w′ ∈ N(w)

Consider then the second case. SinceP ⊆ X ′, we havev′ /∈ P and thus N, v′ ≡d PL(Q) M, w′ for some w′ ∈ N(w). Hence M, w′ ⊩ ψ, so w′ ∈ X. Player 1 now moves one pebble onto v′ and the other ontow′ and becomes the defender. By the induction hypothesis, N, v′ ∼d Q M, w′, which means Player 1 thus has a winning strategy. Player 1 therefore has a winning stra...

work page

[32] [33]

Let I := {φQ,d M⊔N,w′ | w′ ∈ X} ∪ {φQ,d M⊔N,v′ | v′ ∈ P }

In the first case Player 1 chooses a modality⟨Q⟩ ∈ Q, a subsetX ⊆ N(w) such that (N(w), X) ∈ Q, and a subsetP ⊆ N(v). Let I := {φQ,d M⊔N,w′ | w′ ∈ X} ∪ {φQ,d M⊔N,v′ | v′ ∈ P }. Because of the contestion rules,X must be closed under≡d PL(Q) and P cannot contain a node equivalent to a node inN(w). Hence ⟨Q⟩(W φ∈I φ) occurs in φQ,d+1 M⊔N,w and thus N, v ⊩ ⟨Q...

work page

[33] [34]

Let I := {φQ,d M⊔N,v′ | v′ ∈ X} ∪ {φQ,d M⊔N,w′ | w′ ∈ P }

In the second case, Player 1 chooses a modality⟨Q⟩ ∈ Q , a subset X ⊆ N(v) such that (N(v), X) ∈ Q, and a subsetP ⊆ N(w). Let I := {φQ,d M⊔N,v′ | v′ ∈ X} ∪ {φQ,d M⊔N,w′ | w′ ∈ P }. Now N, v ⊩ ⟨Q⟩(W φ∈I φ) and hence we must have thatM, w ⊩ ⟨Q⟩(W φ∈I φ), because N, v ⊩ φQ,d M⊔N,w. The rest of the proof is similar to that of Case 1. Player 2 thus has a winni...

work page

[34] [35]

Player 1 starts as theattacker and Player 2 as thedefender

The game begins with two pebbles placed on the nodesw and v respectively. Player 1 starts as theattacker and Player 2 as thedefender

work page

[35] [36]

If Q is of widthn, he then choosesn subsets (Xi)1≤i≤n of the neighbours of the node such that(N(w), X1,

During each round, the attacker first selects a pebble that is placed on some nodew as well as a modality⟨Q⟩ ∈ Q. If Q is of widthn, he then choosesn subsets (Xi)1≤i≤n of the neighbours of the node such that(N(w), X1, . . . , Xn) ∈ Q and for eachXi he selects a subsetPi ⊆ N(v) of the neighbours of the other pebble. The defender may contest anyPi in the us...

work page

[36] [37]

, X′ n) ∈ Q and Pi ⊆ X ′ i for all 1 ≤ i ≤ n

If the defender does not contest anyPi, he then chooses n subsets (X ′ i)1≤i≤n such that (N(v), X′ 1, . . . , X′ n) ∈ Q and Pi ⊆ X ′ i for all 1 ≤ i ≤ n

work page

[37] [38]

The first is, for some1 ≤ i ≤ n, to move one pebble onto a node inN(v) \ X ′ i and the other onto a node inXi, then take the role of the defender

The attacker now has two options. The first is, for some1 ≤ i ≤ n, to move one pebble onto a node inN(v) \ X ′ i and the other onto a node inXi, then take the role of the defender. The second is, for some1 ≤ i ≤ n, to move a pebble onto a node in X ′ i, after which the defender responds by moving a pebble onto a node in eitherXi or Pi

work page

[38] [39]

(X ′ i)1≤i≤n) of sets is chosen, the other player may contest any individualXi (resp

Whenever a tuple(Xi)1≤i≤n (resp. (X ′ i)1≤i≤n) of sets is chosen, the other player may contest any individualXi (resp. X ′ i) in the usual way by placing a pebble onto a node in the contested set and the other onto a node in the complementN(w) \ Xi (resp. N(v) \ X ′ i), then taking the role of the defender. The next round then starts with the attacker’s move

work page

[39] [40]

behave similarly

The attacker wins if, at the start of any round, the nodes the pebbles lay on do not satisfy the same proposition symbols. If at any point a player must choose a subset but cannot do so, then that player loses. An infinite-length game is always won by Player 2. Lemma 9. Lemma 6 holds whenQ is a set of finite-width generalized modalities. Proof. The base c...

work page

[40] [41]

Each member Q of Q is a Turing machine that computes the corresponding gen- eralized quantifier. (Note that we use the same symbol for the quantifier and the corresponding Turing machine.) This means that when given a pair(A, P) as in- put, Q decides whether it belongs to the corresponding generalized quantifier. Such generalized quantifiers are calledcomputable

work page

[41] [42]

Such a function is called aneffective representationof Q

There exists a computable function f : N → Pfinite(Q), 22 where Pfinite(Q) is the set of all finite subsets ofQ, such thatf(N) is a representation of Q at width N. Such a function is called aneffective representationof Q. Example 15. Consider the set C := {∃≥k | k ∈ N} of all counting quantifiers. This set is effectively finite, because each quantifier∃≥k...

work page

[42] [43]

Q-WL receives as an input a Kripke modelM and a depthd ∈ N

work page

[43] [44]

We compute the maximum out-degree ofM and store it ask

work page

[44] [45]

We can thus compute the finite set of computable quantifiersQ0 ⊆ Q associated with the effective representationf such that Q0 := f(k)

Because Q is effectively finite, it has an effective representationf : N → P f inite(Q). We can thus compute the finite set of computable quantifiersQ0 ⊆ Q associated with the effective representationf such that Q0 := f(k)

work page

[45] [46]

We runQ0-WL on M and d. Note that if we consider a set of graphs, as we do in the experimental section of the paper, then the input to the algorithm has to be the disjoint union of those graphs (to get the maximum out-degree of all graphs). Alternatively, we could consider aset of graphs as an input to the algorithm and take the maximum out-degree of the ...

work page