Towards a Complete Logical Framework for GNN Expressiveness

Authors: Tuo Xu
Primary area: learning on graphs and other geometries & topologies
Keywords: graph neural networks, logic

Abstract:
Designing expressive Graph neural networks (GNNs) is an important topic in graph machine learning fields. Traditionally, the Weisfeiler-Lehman (WL) test has been the primary measure for evaluating GNN expressiveness. However, high-order WL tests can be obscure, making it challenging to discern the specific graph patterns captured by them. Given the connection between WL tests and first-order logic, some have explored the logical expressiveness of Message Passing Neural Networks. This paper aims to establish a comprehensive and systematic relationship between GNNs and logic. We propose a framework for identifying the equivalent logical formulas for arbitrary GNN architectures, which not only explains existing models, but also provides inspiration for future research. As case studies, we analyze multiple classes of prominent GNNs within this framework, unifying different subareas of the field. Additionally, we conduct a detailed examination of homomorphism expressivity from a logical perspective and present a general method for determining the homomorphism expressivity of arbitrary GNN models, as well as addressing several open problems.

Decision: accept (oral)
Reviewer scores: 8, 8, 8

Reviews and discussion:
<thread>
creation date:
1729351226747

thread_type:
official_review

<thread_object>
creator: reviewer_pxbi

<content>
summary:
The paper first proposes GACNNs, a generalisation of several GNN architectures, using sequences of combination and aggregation functions over node tuples. This allows them to subsume several existing GNNs models. They then prove the logical expressivity of GACNNs and apply those results to find the equivalent logic sets for 8 GNN variants. Finally, they show how the logical expressivity can be used to also find the homomorphism expressivity and k-WL expressivity of the model.

strengths:
1. The contribution is significant and will be of interest to the ICLR community. It unifies existing work on logical expressivity of GNNs, as well as showing the consequences that this has for two other important methods of analysing GNN expressivity.
2. The paper makes good use of space, sticking to the recommended 9 pages and rarely making redundant statements.
3. The quality of the work appears to be good, although I haven't been able to properly verify the soundness of the proofs.
4. The authors have made it clear where their work fits into the existing literature, and what their contribution is.

weaknesses:
Major:
1. The main section of the paper lacks intuitions as to why the theorems are true, as well as proof sketches. These would greatly benefit the reader, particularly for a central result such as Theorem 3.
2. Due to a mixture of typos and imprecision, it is sometimes unclear what the authors are intending to stay from a technical perspective. This is particularly problematic in a paper that consists solely of theory. For example: on L262, the "logic sets at the bottom" have so far only been presented to be able to be atp(u), so what else could this refer to? And on L171, what does 'u' refer to? One might reasonably assume a node, but further down it also appears to refer to node tuples.
3. I have many other smaller concerns with the paper, which altogether come together into a major concern.

Medium:
1. L187 the example is far too simple and doesn't do enough to explain the idea of having a sequence of operations within each layer. It is not obvious how other real GNNs can be made from these building blocks. Using a more complex example like Local 2-GNN would be more beneficial.
2. In Theorem 3, equivalent logic sets are being used for each x_i, but they have so far only been defined for GNNs, not these building blocks. A more general definition of equivalent logic sets is needed.
3. L327 "auxiliary logic set". One might assume that this relates to global readouts, given that these greek letters were just used above. However, that interpretation does not seem to fit with the proposition. It is not clear, and should be stated explicitly what this logic set is for, as well as using different notation to separate it from global readouts if that is not what it intends to represent.
4. L331 the jump from the GNN models to their expressivity is not clear. It would be helpful to see an example of the whole pipeline in effect: GNN model -> GACNN -> equivalent logic -> simplification of the logic
5. L406 the construction is presented in a somewhat clunky manner, and would benefit from being both more precise and concise. E.g. the enumeration (a-c) is just the definition of a graph that can be done inline

Minor:
1. L35 "many studies" needs a citation
2. L38 it is unclear why k-WL lacks interpretability
3. L49 "although provides"
4. L55 MPNNs are already a generalisation of several GNNs models, so it is misleading to say they analyse different GNN models separately.
5. L76 "is denoted"
6. L97 "leave"
7. L105 "predicate", "corresponds"
8. In section 3.1, GNNs are referred to without having been defined yet.
9. L140 "district"
10. L152 "the elements" -> "each element"
11. L166 no need for "etc", since you already said "including"
12. L172 should be clearer that it's a sequence of two operations, not just two operations
13. L182 "variants", but only one is described
14. L187 the appendix should be referenced here for the construction of the other GNN models within this framework
15. L254 "existed"
16. L255 "edges" -> "neighbourhoods", since we're generalising to node tuples
17. L270 "function", "Similar as previous"
18. L281 "is" = "are"
19. L298 "its layers" -> "a layer", since all layers have been assumed to have the same structure
20. L309 "provides"
21. L323 "prediction"
22. L365 "although computes"
23. L376 "tasks"
24. L392 should this not be "homomorphism expressivity"? Homogenous has other connotations. Also "beautiful" is emotive language and should be avoided
25. L404 full stop should not be there
26. L464 - 466 is a bit verbose, and restating the obvious

questions:
1. L134 the GNN outputs "true" for a node. Does this mean that GNNs are restricted to those that do binary classification on nodes? If so, this is not stated explicitly anywhere.
2. L140 why are logic sets "quantitative" but k-WL or homomorphism tests are not?
3. L171 - what does "u" refer to? This needs to be more explicit.
4. L179 I find it strange that the computation counts down (from K + 1) within a GACNN layer, but at the layer level it counts up from 0. Is there a good reason for this?
5. L180 "generalised neighbour" has not been defined. What does this precisely refer to?
6. L196 why not use an example of an existing GNN model here?
7. L262 "logic sets at the bottom" have so far only been presented to be able to be atp(u), so what else could this refer to?
8. L351 "more general v". In what sense is it more general? And why is it obviously more powerful?
9. L450 how useful is the construction, given its recursive nature?
10. L472 why is the WL bound on SEAL so weak, given proposition 9? Shouldn’t we be able to exactly specify it’s WL expressivity?
11. Is the paper claiming to have generalised all GNNs? L482 seems to suggest so.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730467016619

thread_type:
official_review

<thread_object>
creator: reviewer_odss

<content>
summary:
The authors introduce a framework to assess the logical expressivity of Graph Neural Network (GNN) models by analyzing their underlying combination and aggregation operations. By constructing sets of logical formulas that each GNN model can capture, this method provides insights into the types of logical properties these models can represent and distinguish. Intuitively, a GNN captures a formula $\phi$ in FO if, for any graph G, the results of $\phi$ applied on G are fully reproduced by the representations computed by the GNN.
By mapping GNN operations to logical formulas, the framework identifies the set of logical statements a GNN can inherently represent. This is a more fine-grained approach to understanding the expressivity of GNNs compared to the WL hierarchy. The paper explores GNN expressivity across different prediction tasks—graph-level, node-level, and link-level—highlighting the logical distinctions between models when applied to tasks at each of these levels.

strengths:
- A new theoretical framework for assessing the expressive power of GNNs by relating it to fragments of FO
- Classification of existing MPNNs, subgraph GNNs
- Ability to assess the expressive power wrt to the ability to capture certain substructures (motifs) in graphs
- Affirms conjecture from prior work

weaknesses:
- The presentation could be improved in several places. For instance, there could be more illustrations and examples throughout the paper. 
- Nitpick: I would refrain from assigning very positive attributes, "simple," "elegant," etc., to your own results and proofs.

questions:
- There should be a limitations section. For instance, do these results apply to graphs with node attributes as well? What other limitations has the proposed framework for assessing expressiveness of GNNs? What could be future work?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730555625464

thread_type:
official_review

<thread_object>
creator: reviewer_ar9b

<content>
summary:
The paper presents a novel framework aimed at systematically assessing the logical expressiveness of GNNs. It proposes a comprehensive relationship between GNNs and logic, offering a method to construct logical formulas equivalent to arbitrary GNN architectures. The paper also discusses the implications of this framework for understanding existing models, comparing expressiveness across models, and estimating WL test bounds.

strengths:
**Solid Theory**: The paper constructs a solid theoretical foundation through extensive mathematical proofs and derivations.

**Unified Framework**: By establishing a connection between GNNs and first-order logic, the paper proposes a theoretical framework that can unify different GNN models. This framework allows for a systematic comparison of the expressiveness of different GNN models.

**Novel Perspective**: The paper analyzes and explains the expressiveness of GNN models from the perspective of first-order logic, providing a new perspective for understanding these models.

weaknesses:
**Limited Comparison and Analysis**: The paper does not specifically analyze what each operation in first-order logic implies about what the model has learned, nor does it directly compare with other existing expressiveness assessment frameworks, such as the work mentioned by Zhang et al.

**Practical Guidance for Model Development**: Although the paper provides an assessment framework, it lacks specific guidance on how to use this framework to guide the development of high-expressiveness GNN models.

**Insufficient Experimental Validation (Not necessarily a con)**: The paper lacks an experimental section to validate the effectiveness, rationality, and correctness of its framework.

questions:
1. Early work also explained the expressiveness of GNNs from a logical perspective. What new contributions have your contributions made compared to their work? Specifically, what are the differences between the second-order logic they used and the first-order logic used in your work? What are the respective advantages and disadvantages?

2. Please further elaborate and supplement what each operation in first-order logic specifically corresponds to in terms of what the model learns from the graph?

3. Zhang et al. proposed a refined framework for assessing the expressiveness of GNNs in "Beyond Weisfeiler-Lehman: A Quantitative Framework for GNN Expressiveness." Compared to the assessment method proposed in the paper, what are the respective strengths and weaknesses? Could you provide a detailed comparative analysis?

4. The paper compares several typical GNN models using a unified framework. Could you further explain how the differences in logical expressions of different GNN models correspond to the actual capabilities of the models in practice?

5. Please supplement experiments to prove the completeness, rationality, and correctness of the theoretical aspects of the paper. This would be very helpful for understanding the differences between models and selecting models suitable for specific tasks.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732882878714

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
General Response: New results & Updates

comment:
We sincerely thank all the reviewers for their great efforts in reviewing our paper. Below we would like to summarize major updates during discussion period and highlight that we have enhanced two key theoretical results originally presented in the initial paper, which we believe can further strengthen this work.

## The Definition of Equivalent Logic Set

In the inital submission, we define the equivalent logic set $\Phi$ of a family of graph function $\mathcal{X}$ (e.g. a class of GNNs) is:
- The order of each $\varphi\in\Phi$ is $k$;
- For all $\varphi\in\Phi$, there exists $\chi\in\mathcal{X}$ such that for arbitrary graphs $G$ and $\mathbf{u}\in\mathcal{V}^k_G$,  $\varphi(\mathbf{u})=true$ iff $\chi(\mathbf{u})=true$, and we say $\chi$ captures $\varphi$.
- Given any graphs $G,H$ and $\mathbf{u}\in\mathcal{V}_G^k,\mathbf{v}\in\mathcal{V}_H^k$, all $\chi\in\mathcal{X}$ cannot distinguish $\mathbf{u},\mathbf{v}$ iff all logic formulas $\varphi\in\Phi$ classify $\mathbf{u},\mathbf{v}$ the same.

During the discussion period, we found this definition limited in that:
1. The definition does not state that whether there exists a one-to-one correspondence between one GNN model $\chi\in\mathcal{X}$ and one logic formula $\varphi\in\Phi$. It only states that all GNNs are equivalent to all logic formulas.
2. The definition does not state the completeness of $\Phi$, i.e. whether all logic formulas captured by $\mathcal{X}$ are in $\Phi$. This property has been discussed by Barcelo et al. [1] for MPNNs.

We have now successfully addressed the above limits and extended our results (see Definition 2 in the paper). We believe that the equivalent logic sets can now more completely characterize the logical expressivity of different models. We added two statements in the defintion of equivalent logic sets:
### About one-to-one correspondence between $\chi\in\mathcal{X}$ and $\varphi\in\Phi$.
We have shown that there exists a GNN model which is not captured by any logic formula. Therefore, to disscuss this property, we defined a weaker version of one-to-one correspondence:
- Given arbitrary positive integer $N$ and $\chi\in\mathcal{X}$, there exists $\varphi\in\Phi$ satisfying: for any graphs $G$ with no more than $N$ nodes and $\mathbf{u}\in\mathcal{V}_G^k$, $\varphi(\mathbf{u})=true$ iff $\chi(\mathbf{u})=true$.

This is weaker than saying $\varphi$ is always captured by $\chi$, as it only considers finite situations. However, using this defintion we are able to give a one-to-one correspondence between GNNs and logic formulas. This property is already proved in the initial paper.
### About the completeness of $\Phi$.
We have now successfully proved the following results for equivalent logic sets:
- A FOC formula is captured by $\mathcal{X}$ iff it is in $\Phi$.

The proof is a direct generalization of the proof of Theorem 2.1 in [2], in which we generalized the discussion of first-order logic and $\sim_\sharp $-invariance (which is invariance under 1-WL where node colors are refined by neighbors) into the discussion of first-order logic and GACNNs(where node tuple colors are refined by generalized neighbors). One can see that the above results establish stronger relationship between GNNs and logic.

## Experiments

We have conducted experiments to empirically test the logical expressivity of GNNs validate our theory, which is presented in Appendix D.

## About writting / clarity of the paper

We have revised the main body of the paper to improve the writting and the clarity of the presentation. This includes:

- A more precise definition of the symbols / terms used in this paper (Section 2).
- A more precise definition of GACNNs (Section 3, 4).
- Examples about the structure of GACNNs (Section 4), the relation between logic operators and GNNs (Section 5.1).
- A more concise description of the construction of homomorphism expressivity (Section 6).
- Proof sketches for main theorems in the main text.
- Extended related works (Appendix A).
- Discussion of link prediction and logic (Appendix F).
- Rewrite of proofs.
- Other minor changes, including fixing typos, etc.






[1] Barcelo et al. THE LOGICAL EXPRESSIVENESS OF GRAPH NEURAL NETWORKS. ICLR 2020. \
[2] Martin Otto, Graded modal logic and counting bisimulation, 2023.
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper provides a novel, extensive lens on the logical expressiveness of GNN models. Its strengths are recognised unanimously by all three reviewers, who all recommend strong acceptance. A talk feature at ICLR is recommended!