The Logical Expressiveness of Graph Neural Networks
Authors: Pablo Barceló
Egor V. Kostylev
Mikael Monet
Jorge Pérez
Juan Reutter
Juan Pablo Silva
Venue:  (2020)
Keywords: Graph Neural Networks
First Order Logic
Expressiveness

Abstract: The ability of graph neural networks (GNNs) for distinguishing nodes in graphs has been recently characterized in terms of the Weisfeiler-Lehman (WL) test for checking graph isomorphism. This characterization, however, does not settle the issue of which Boolean node classifiers (i.e., functions classifying nodes in graphs as true or  false) can be expressed by GNNs.  We tackle this problem by focusing on Boolean classifiers expressible as formulas in the logic FOC2, a well-studied fragment of first order logic. FOC2 is tightly related to the WL test, and hence to GNNs. We start by studying a popular class of GNNs, which we call AC-GNNs, in which the features of each node in the graph are updated, in successive layers, only in terms of the features of its neighbors.  We show that this class of GNNs is too weak to capture all FOC2 classifiers, and provide a syntactic characterization of  the largest subclass of FOC2 classifiers that can be captured by AC-GNNs. This subclass coincides with a logic heavily used by the knowledge representation community. We then look at what needs to be added to AC-GNNs for capturing all FOC2 classifiers. We show that it suffices to add readout functions, which allow to update the features of a node not only in terms of its neighbors, but also in terms of a global attribute vector. We call GNNs of this kind ACR-GNNs. We experimentally validate our findings showing that, on synthetic data conforming to FOC2 formulas, AC-GNNs struggle to fit the training data while ACR-GNNs can generalize even to graphs of sizes not seen during training.

Published as a conference paper at ICLR 2020
THE LOGICAL EXPRESSIVENESS OF GRAPH NEURAL NETWORKS
Pablo Barceló IMC, PUC & IMFD Chile
Egor V. Kostylev
Mikaël Monet IMFD Chile
University of Oxford
Jorge Pérez DCC, UChile & IMFD Chile
Juan Reutter
Juan-Pablo Silva DCC, UChile
DCC, PUC & IMFD Chile
ABSTRACT
The ability of graph neural networks (GNNs) for distinguishing nodes in graphs has been recently characterized in terms of the Weisfeiler-Lehman (WL) test for checking graph isomorphism. This characterization, however, does not settle the issue of which Boolean node classifiers (i.e., functions classifying nodes in graphs as true or false) can be expressed by GNNs. We tackle this problem by focusing formulas in the logic FOC2, well-studied
Boolean classifiers expressible fragment of first order logic. FOC₂ is tightly related to the WL. test, and hence to GNNs. We start by studying popular class of GNNs, which we call AC-GNNs, in which the features each node in the graph are updated, in successive layers, only in terms of the features of its neighbors. We show that this class GNNs is too weak to capture all FOC, classifiers, and provide a syntactic characterization of the largest subclass of FOC₂ classifiers that can be captured by AC-GNNs. This subclass coincides with a logic heavily used by the knowledge representation community. We then look at what needs to be added to AC-GNNs for capturing all FOC₂ classifiers. We show that it suffices to add readout functions, which allow to update the features of a node not only in terms of its neighbors, but also in terms of global attribute vector. We call GNNs of this kind ACR-GNNs. We experimentally validate our findings showing that, on synthetic data conforming to FOC₂ formulas, AC-GNNs struggle to fit the training data while ACR-GNNs can generalize even to graphs of sizes not seen during training.
INTRODUCTION
Graph neural networks (GNNs) (Merkwirth Lengauer, 2005; Scarselli et al., 2009) are a class of neural network architectures that has recently become popular for wide range of applications dealing with structured data, c.g., molecule classification, knowledge graph completion, and Web page ranking (Battaglia et al., 2018; Gilmer et al., 2017; Kipf & Welling, 2017; Schlichtkrull al., 2018). The main idea behind GNNs is that the connections between neurons are not arbitrary but reflect the structure of the input data. This approach is motivated by convolutional and recurrent neural networks and generalize both of them (Battaglia et al., 2018). Despite the fact that GNNs have recently been proven very efficient in many applications, their theoretical properties are not yet well-understood. In this paper we make step towards understanding their expressive power by establishing connections between GNNs and well-know logical formalisms, We believe these connections to be conceptually important, they permit us to understand the inherently procedural behavior of some fragments of GNNs in terms of the more declarative flavor of logical languages.
Two recent papers (Morris et al., 2019; Xu et al., 2019) have started exploring the theoretical prop- erties of GNNs by establishing a close connection between GNNs and the Weisfeiler-Lehmar (WL) test for checking graph isomorphism. The WL test works by constructing labeling of the nodes of the graph, in an incremental fashion, and then decides whether two graphs are isomorphic by com- paring the labeling of each graph. To state the connection between GNNs and this test, consider the simple GNN architecture that updates the feature vector of each graph node by combining with the aggregation of the feature vectors of its neighbors. We call such GNNs aggregate-combine GNNs,

---

Published as a conference paper at ICLR 2020
or AC-GNNs. The authors of these papers independently observe that the node labeling produced by the WL test always refines the labeling produced by any GNN. More precisely, if two nodes are labeled the same by the algorithm underlying the WL test, then the feature vectors of these nodes produced by any AC-GNN will always be the same. Moreover, there are AC-GNNs that can repro- duce the WL. labeling, and hence AC-GNNs can be powerful the WI. test for distinguishing nodes. This does not imply, however, that AC-GNNs can capture every node classifir--that is, a function assigning true or false to every node-that is refined by the WL test. In fact, it is not difficult to see that there are many such classifiers that cannot be captured by AC-GNNs; one simple example a classifier assigning true to every node if and only if the graph has an isolated node. Our work aims to answer the question of what are the node classifiers that can be captured by GNN architectures such as AC-GNNs.
To start answering this question, we propose to focus on logical classifiers that is, on unary formu- las expressible in first order predicate logic (FO): such formula classifies each node e according to whether the formula holds for not. This focus gives us an opportunity to link GNNs with declarative and well understood formalisms, and to establish conclusions about GNNs drawing upon the vast amount of work logic. For example, if one proves that two GNN architectures are cap- tured with two logics, then one can immediately transfer all the knowledge about the relationships between those logics, such as equivalence or incomparability of expressiveness, the GNN setting.
For AC-GNNs, a meaningful starting point to measure their expressive power is the logic FOC,, the two variable fragment of first order predicate logic extended with counting quantifiers of the form 32N yp which state that there are at least N nodes satisfying formula (Cai et al., 1992). Indeed, this choice of FOC₂ is justified by classical result due to Cai et al. (1992) establishing tight connection between FOC, and WL: two nodes in a graph are classified the same by the WL test if and only they satisfy exactly the same unary FOC₂ formulas. Moreover, the counting capabilities of FOC₂ can be mimicked in FO (albeit with more than just two variables), hence FOC₂ classifiers are fact logical classifiers according to our definition.
Given the connection between AC-GNNs and WL on the one hand, and that between WL and FOC, on the other hand, one may be tempted to think that the expressivity of AC-GNNs coincides with that of FOC₂. However, the reality is not as simple, and there are many FOC₂ node classifiers (e.g., the trivial one above) that cannot be expressed by AC-GNNs. This leaves us with the following natural questions. First, what is the largest fragment of FOC₂ classifiers that be captured by AC-GNNs? Second, is there an extension of AC-GNNs that allows to express all FOC₂ classifiers? In this paper we provide answers to these two questions. The following are our main contributions.
We characterize exactly the fragment of FOC₂ formulas that can be expressed as AC- GNNs. This fragment corresponds to graded modal logic (de Rijke. 2000), equivalently, to the description logic ALCO, which has received considerable attention in the knowledge representation community (Baader et al., 2003; Baader & Lutz, 2007).
Next we extend the AC-GNN architecture in a very simple way by allowing global read- outs, where in each layer we also compute a feature vector for the whole graph and combine it with local aggregations; we call these perrggate-combin--eeddee
GNNs (ACR-GNNA These networks are a special case of the ones proposed by Battaglia et al. (2018) for re- lational reasoning over graph representations. In this setting, we prove that each FOC, formula can be captured by an ACR-GNN.
We experimentally validate our findings showing that the theoretical expressiveness of ACR- as well as the differences between AC-GNNs and ACR-GNNs, can be observed when we learn from examples. In particular, we show that on synthetic graph data conforming to FOC, formulas, AC- GNNs struggle to fit the training data while ACR-GNNs can generalize even to graphs of sizes not seen during training.
2 GRAPH NEURAL NETWORKS
In this section we describe the architecture of AC-GNNs and introduce other related notions. We concentrate on the problem of Boolean node classification: given (simple, undirected) graph G = (V, E) in which each vertex e E V has an associated feature vector z,, we wish to clas- sify each graph node true or false; in this paper, we assume that these feature vectors are one-hot
2

---

Published as a conference paper at ICLR 2020
encodings of node colors in the graph, from a finite set of colors. The neighborhood Na(u) of node v E is the set {u) {u, u) E E}.
The basic architecture for GNNs, and the one studied in recent studies GNN expressibility (Mor- ris et al., 2019; Xu et al., 2019), consists of a sequence of layers that combine the feature vectors of every node with the multiset of feature vectors of its neighbors. Formally, let {AGG H== and (COMO) 1
be two sets of aggregation and combination functions. An aggregate-combiee GNN (AC-GNN) computes vectors a!!") for every node v of the graph G. via the recursive formula
x = COM
2 2 AGG! (f=l
(ENc(o)))
for i = -.....,
(I)
where each x. is the initial feature vector Ey of v. Finally, each node v of G is classified according to Boolean classification function CLS applied to z!" Thus, AC-GNN with L layers is defined as tuple A ((AGG)) J (COM 1= CLS), ), and we denote by A(G, u) the class (i.e., true or false) assigned by A each node v in G.
There are many possible aggregation, combination, and classification functions, which produce dif- ferent classes of GNNs (Hamilton et al., 2017: Kipf & Welling, 2017; Morris et al., 2019; Xu al., 2019). A simple, yet common choice is to consider the sum of the feature vectors as the aggregation function, and a combination function as
COM (x1, = 1 [2² (1)) + x2 + B(O),
(2)
where C and A (6) are matrices of parameters, (+0) a bias vector, and f is non-linearity func- tion, such relu or sigmoid. We call simple AC-GNN using these functions. Furthermore, we say that AC-GNN is homogeneous if all (GG are the same and all COM are the same (share the same parameters across layers). In most of our positive results we construct simple and homoge- neous GNNs, while our negative results hold in general (i.e., for GNNs with arbitrary aggregation, combining, and classification functions).
The Weisfeille-Lehman (WL) test is powerful heuristic used solve the graph isomorphism prob- lem (Weisfeiler & Leman, 1968), or, for our purposes, to determine whether the neighborhoods of two nodes in graph are structurally close or not. Due to space limitations, we refer (Cai al., 1992) for a formal definition of the underlying algorithm, giving only its informal description: start- ing from colored graph, the algorithm iteratively assigns, for a certain number of rounds, new color to every node in the graph; this is done in such a way that the color of a node in each round has a one to one correspondence with its own color and the multiset of colors of its neighbors in the previous round. An important observation is that the rounds of the WI. algorithm can be seen as the layers of an AC-GNN whose aggregation and combination functions are all injective (Morris et al., 2019; Xu al., 2019). Furthermore, as the following proposition states, an AC-GNN classification can never contradict the WL test.
Proposition 2.1 (Morris et al., 2019; Xu et al., 2019). If the WL test assigns the same color to two nodes in a graph, then every AC-GNN classifies either both nodes as true or both nodes false.
CONNECTION BETWEEN GNNs AND LOGIC
3.1 LOGICAL NODE CLASSIFIERS
Our study relates the power of GNNs to that of classifiers expressed in first order (FO) predicate logic over (undirected) graphs where each vertex has a unique color (recall that we call these classifiers logical classifiers). To illustrate the idea of logical node classifiers, consider the formula
a(x) = Red(x) A By (E(r, v) A Blue(y)) ^ 3z (B(x, z) A Green(=)).
Forr graph classification, which we do not consider in this paper. the classification function CLS inputs the multiset {x v E } and outputs a class for the whole graph. Such a function is often called readout in previous work (Morris et al., 2019; Xu et al., 2019). In this paper, however, we use the term readout to refer to intermediate global operations performed while computing features for nodes (see Section 5).
3

---

Published as a conference paper at ICLR 2020
This formula has one free variable, z, which is not bounded by any quantifier of the form 3 or V, and two quantified variables and z. In general, formulas with one free variable are evaluated over nodes of given graph. For example, the above formula evaluates true exactly in those nodes whose color is Red and that have both a Blue and a Green neighbor. In this case, we say that node v of G satisfies a, and denote this by (G, e) F
Formally, a logical (node) classifier is given by a formula ((()) in FO logic with exactly one free variable. This formula classifies as true those nodes in G such that (G. F sp, while all other nodes (i.e., those with (G,v) v) i s) are classified as false. We say that GNN classifier captures a logical classifier when both classifiers coincide over every node in every possible input graph.
Definition 3.1. A GNN classifier A captures logical classifier pp()) if for every graph G and node v in G, holds that A(G, v) = true if and only if (G,,) v) F F..
3.2 LOGIC FOC2
Logical classifiers are useful as declarative formalism, but will see, they are too powerful to compare them to AC-GNNs. Instead, for reasons we explain later we focus on classifiers given by formulas in FOC2, the fragment of FO logic that only allows formulas with two variables, but in turn permits to use counting quantifiers.
Let us briefly introduce FOC₂ and explain why it is restriction of FO logic. The first remark is that reducing the number of variables used in formulas drastically reduces their expressive power. Consider for example the following FO formula expressing that a red node, and there is another node, that is not connected to x and that has at least two blue neighbors, and 22:
B(x)= Red(z) A By(-EE<: v) A E(y, 21) E 22) A2
22 Blue (2(2)))BBBB))) Blue(22)) (22) I)-
The formula ((x) uses four variables, but it is possible to find an equivalent one with just three: the trick is reuse variable and replace every occurrence of z2 in B(x)) by x. However, this is far as we can go with this trick: ((x) does not have an equivalent formula with less than three variables. In the same way, the formula (xx) given in Equation (3) can be expressed using only two variables, and y, simply by reusing in place of 2.
That being said, it is possible extend the logic so that some node properties, such as the one defined by ((z), can be expressed with even less variables. To this end, consider the counting quantifier 3N for every positive integer N. Analogously to how the quantifier E expresses the existence of node satisfying a property, the quantifier PEt expresses the existence of at least N different nodes satisfying a property. For example, with 222 we can express ((x) by using only two variables by means of the classifier
7x) = Red(x)) A 3y(-E(I, v) A 3 Ely, x) A Blue())])
(4)
Based on this idea, the logic FOC, allows for formulas using all FO constructs and counting quanti- fiers, but restricted to only two variables. Note that, in terms of their logical expressiveness, we have that FOC₂ is strictly less expressive than FO (as counting quantifiers can always be mimicked in FO by using more variables and disequalitics), but is strictly more expressive than FO2, the fragment of FO that allows formulas use only two variables (as (1x) belongs to FOC₂ but not to FO2).
The following result establishes a classical connection between FOC₂ and the WL test. Together with Proposition 2.1, this provides justification for our choice of logic FOC₂ for measuring the expressiveness of AC-GNNs.
Proposition 3.2 (Cai et al., 1992). For any graph G and nodes u, u G. the WL test colors u and the same after any number of rounds iff and v are classified the same by all FOC₂ classifiers.
3.3 FOC₂ AND AC-GNN CLASSIFIERS
Having Propositions 2.1 and 3.2, one may be tempted to combine them and claim that every FOC, classifier can be captured by AC-GNN. Yet, this is not the case shown in Proposition 3.3 below. In fact, while it is true that two nodes are declared indistinguishable by the WL test if and only if they are indistinguishable by all FOC, classifiers (Proposition 3.2), and if the former holds then such nodes cannot be distinguished by AC-GNNs (Proposition 2.1). this by no means tells us that every FOC, classifier can be expressed as AC-GNN.
4

---

Published as a conference paper at ICLR 2020
Proposition 3.3. There is an FOC₂ classifier that is not captured by any AC-GNN.
One such FOC₂ classifier is (ax) in Equation (4), but there are infinitely many and even simpler FOC₂ formulas that cannot be captured by AC-GNNs. Intuitively, the main problem that an AC- GNN has only fixed number L of layers and hence the information of local aggregations cannot travel further than at distance L of every node along edges in the graph. For instance, the red node in (xx may be farther away than the node with the blue neighbours, which means that AC-GNNs would never be able to connect this information. Actually, both nodes may even be in different connected components of a graph, in which case no number of layers would suffice.
The negative result of Proposition 3.3 opens up the following important questions.
1. What kind of FOC2 classifiers can be captured by AC-GNNs? 2. Can we capture FOC₂ classifiers with GNNs using a simple extension of AC-GNNs?
We provide answers these questions in the next two sections.
4 THE EXPRESSIVE POWER OF AC-GNNS
Towards answering our first question, we recall that the problem with AC-GNN classifiers is that they are local, in the sense that they cannot see across distance greater than their number of layers. Thus, if we want to understand which logical classifiers this architecture is capable of expressing, we must consider logics built with similar limitations in mind. And indeed, in this section we show that AC-GNNs capture any FOC₂ classifier as long as we further restrict the formulas so that they satisfy such a locality property. This happens to be a well-known restriction of FOC₂, and corresponds to graded modal logic (de Rijke, 2000) or, equivalently, to description logic ALCQ (Baader et al., 2003), which is fundamental for knowledge representation: for instance, the OWL 2 Web Ontology Language (Motik et al., 2012 2; W3C OWL Working Group, 2012) relies on ALCQ.
The idea of graded modal logic is to force all subformulas to be guarded by the edge predicate F. This means that one cannot express in graded modal logic arbitrary formulas of the form Ayy(()) ie., whether there is some node that satisfies property y. Instead, one is allowed to check whether some neighbor y of the node where the formula is being evaluated satisfies yp That is, we are allowed to express the formula By (E(r, y) A (py)) in the logic as in this case (Py)) is guarded by E(x,y) v). We can define this fragment of FO logic using FO syntax follows. A graded modal logic formula is either Co)( for Col a node color, or one of the following, where sp and to are graded modal logic formulas and N is positive integer:
-p(x),
p(z) A p(x), 3NN y (E(x,)) v) A ((1)).
Notice then that the formula 8(x) Red(x)) A By (E(x, v) A Blue(v)) is in graded modal logic, but the logical classifier 7(x) in Equation (4) is not, because the use of (xx y) as a guard is disallowed. As required, we can now show that AC-GNNs can indeed capture all graded modal logic classifiers.
Proposition 4.1. Each graded modal logic classifier is captured by a simple homogeneous AC-GNN.
The key idea of the construction is that the vectors' dimensions used by the AC-GNN to label nodes, represent the sub-formulas of the captured classifier. Thus, if a feature in node is then the node satisfies the corresponding sub-forman formuul,,,, and the opposite holds after evaluating L layers, where L the "quantifier depth" of the classifier (which does not depend on the graph). The construction uses simple, homogeneous AC-GNNs with the truncated relu non-linearity max(0, min(r, 1)). The formal proof of Proposition 4.1, as well as other formal statements, can be found in the Appendix. An interesting question that leave as future work is to investigate whether the same kind of construction can be done with AC-GNNs using different aggregate and combine operators than the ones we consider here; for instance, using max instead of sum to aggregate the feature vectors of the neighbors, or using other non-linearity such as sigmoid, etc.
The relationship between AC-GNNs and graded modal logic goes further: modal logic is the "largest" class of logical classifiers captured by AC-GNNs. This means that the only FO formulas that AC-GNNs are able learn accurately are those in graded modal logic.
show that graded
5

---

Published as a conference paper at ICLR 2020
Theorem 4.2. A logical classifier is captured by AC-GNNs if and only if it can be expressed in graded modal logic.
The backward direction of this theorem is Proposition 4.1, while the proof of the forward direction based on a recently communicated extension of deep results in finite model theory (Otto, 2019). We point out that the forward direction holds no matter which aggregate and combine operators are considered, i.e., this is limitation of the architecture for AC-GNNs, not of the specific functions that one chooses to update the features.
5 GNNS FOR CAPTURING FOC₂
5.1 GNNS WITH GLOBAL READOUTS
In this section tackle our second question: which kind of GNN architecture need to capture all FOC₂ classifiers? Recall that the main shortcoming of AC-GNNs for expressing such classifiers is their local behavior. A natural way break such behavior is to allow for global feature com- putation on each layer of the GNN. This is called a global atribute computation in the framework of Battaglia et al. (2018). Following the recent GNN literature (Gilmer et al., 2017; 2019; Xu et al., 2019), we refer to this global operation as readout.
Morris et al.,
Formally, an aggregate-combine--rddde
GNN (ACR-GNN) extends AC-GNNs by specifying read- ouf functions (READ = which aggregate the current feature vectors of all the nodes in a graph. Then, the vector a!! of each node in G on each layer i, is computed by the following formula, generalizing Equation (I):
( COM "U-"",AGG (H=!!-1) e Nc(())).
(H=! /u GB)). (5)
Intuitively, every layer in an ACR-GNN first computes (i.e., "reads out") the aggregation over all the nodes in G; then, for every node v, it computes the aggregation over the neighbors of uq and finally it combines the features of v with the two aggregation vectors. All the notions about AC- GNNs extend ACR-GNNs in straightforward way; for example, simple ACR-GNN uses the sum as the function ( each layer, and the combination function C (æ), 22, 0:3) = A()
f( C(0) + x2 (0) + xz R (
( + b(o) with matrix R(0, generalizing Equation (2).
5.2 ACR-GNNS AND FOC₂
To how a readout function could help in capturing non-local properties, consider again the logical classifier ((x) in Equation (4), that assigns true to every red node as long as there is another node not connected with v having two blue neighbors. We have seen that AC-GNNs cannot capture this classifier. However, using a single readout plus local aggregations one can implement this classifier as follows. First, define by the property "having least 2 blue neighbors". Then an ACR-GNN that implements (x)) can (1) use one aggregation to store in the local feature of every node if the node satisfies B, then (2) use a readout function to count how many nodes satisfying the whole graph, and (3) use another local aggregation to count how many neighbors of every node satisfiy B. Then 7 is obtained by classifying as true every red node having less neighbors satisfying B than the total number of nodes satisfying B in the whole graph. It turns out that the usage of readout functions is enough to capture all non-local properties of FOC, classifiers.
exist in
Theorem 5.1. Each FOC₂ classifier can be captured by simple homogeneous ACR-GNM
The construction is similar to that of Proposition 4.1 and uses simple, homogeneous ACR-GNNs that is, the readout function is just the sum of all the local node feature vectors. Moreover, the readout functions are only used to deal with subformulas asserting the existence of node that is not connected to the current node in the graph, just as we have done for classifier y(x). As an characterization of FOC₂ using extended version of
intermediate step in the proof, we graded modal logic, which was obtained by Lutz et al. (2001). We leave as a challenging open problem whether FOC, classifiers are exactly the logical classifiers captured by ACR-GNNs.

---

Published as a conference paper at ICLR 2020
5.3 COMPARING THE NUMBER OF READOUT LAYERS
The proof of Theorem 5.1 constructs GNNs whose number of layers depends on the formula being captured-thal that is, readout functions are used unboundedly many times in ACR-GNNs for captur- ing different FOC₂ classifiers. Given that a global computation can be costly, one might wonder whether this is really needed, or if is possible to cope with all the complexity of such classifiers by performing only few readouts. We next show that actually just one readout is enough. However, this reduction the number of readouts comes at the cost of severely complicating the resulting GNN.
GNN with final readout ACC-FR-GNY results out of using any number of layers as in the AC-GNN definition, together with a final layer that uses readout func- tion, according to Equation (5).
Formally, an
Theorem 5.2. Each FOC₂ classifier is captured by an AC-FR-GNN.
The AC-FR-GNN in the proof of this theorem is not based on the idea of evaluating the formula incrementally along layers, in the proofs of Proposition 4.1 and Theorem 5.1, and it is not simple (note that AC-FR-GNNs are never homogeneous). Instead, it is based on a refinement of the GIN architecture proposed by Xu et al. (2019) to obtain as much information as possible about the local neighborhood in graphs. followed by a readout and combine functions that use this information to deal with non-local constructs in formulas. The first component we build is an AC-GNN that computes an invertible function mapping each node to a number representing its neighborhood (how big is this neighborhood depends on the classifier to be captured). This information is aggregated so that we know for each different type of neighborhood how many times it appears in the graph. We then use the combine function to evaluate FOC₂ formulas by decoding back the neighborhoods.
EXPERIMENTAL RESULTS
We perform experiments with synthetic data to empirically validate results. The motivation of this section is to show that the theoretical expressiveness of ACR ACR-GNNs, as well as the differences between AC- and ACR-GNNs, can actually be observed when we learn from examples. We perform two sets of experiments: experiments to show that ACR-GNNs can learn a very simple FOC₂ node classifier that AC-GNNs cannot learn, and experiments involving complex FOC2 classifiers that need more intermediate readouts to be learned. We implemented our experiments in the PyTorch Geometric library (Fey & Lenssen, 2019). Besides testing simple AC-GNNs, we also tested the GIN network proposed by Xu et al. (2019) (we consider the implementation by Fey & Lenssen (2019) and adapted it to classify nodes). Our experiments use synthetic graphs, with five initial colors encoded as one-hot features, divided in three sets: train set with 5k graphs of size up to 50-100 nodes, test set with 500 graphs of size similar to the train set, and another test set with 500 graphs of size bigger than the train set. We tried several configurations for the aggregation, combination and readout functions, and report the accuracy on the best configuration. Accuracy in our experiments is computed the total number of nodes correctly classified among all nodes in all the graphs in the dataset. In every case we run up to 20 epochs with the Adam optimizer. More details on the experimental setting, data, and code can be found in the Appendix. We finally report results real benchmark (PPI) where we did not observe an improvement of ACR-GNNs over AC-GNNs.
We consider very simple FOC₂ formula defined by a(x) == Red(x)) A By Blue which is satisfied by every red node in a graph provided that the graph contains at least one blue node. We tested with line-shaped graphs and Erdös-Renyi (E-R) random graphs with different connectivities. In every set (train and test) we consider 50% of graphs not containing any blue node, and 50% containing at least one blue node (around 20% of nodes are in the true class in every set), For both types of graphs, already single-layer ACR-GNNs showed perfect performance (ACR-I in Table 1). This was what we expected given the simplicity of the property being checked. In contrast, AC-GNNs and GINs (shown in Table as AC-L and GIN- L, representing AC-GNNs and GINs with L layers) struggle to fit the data. For the case of the line-shaped graph, they were not able to fit the train data even by allowing layers. For the case of random graphs, the performance with layers was considerably better. In a closer look at the performance for different connectivities of E-R graphs, we found an improvement for AC-GNNs when we train them with more dense graphs (details in the Appendix). This is consistent with the fact that AN-GNNs able to move information of local aggregations to distances up to their
Separating AC-GNNs and ACR-GNNs
7

---

Published as a conference paper at ICLR 2020
Line Train
Line Test
E-R Train
E-R Test
same-size
bigger
same-size
bigger
AC-5
0.887
0.886
0.892
0.951
0.949
0.929
AC-7
0.892
0.892
0.897
0.967
0.965
0.958
GIN-5
0.861
0.861
0.867
0.830
0,831
0,817
GIN-7
0.863
0.864
0.870
0.818
0.819
0.813
ACR-1
1.000
1.000
1.000
1.000
1.000
1.000
Table I: Results on synthetic data for nodes labeled by classifier a(x) = Red(w) By Blue(y)
a1 Train
01 Test
02 Train
022 Test
as Train
03 Test
same-size
bigger
same-size
bigger
same-size
bigger
AC
0.839
0.826
0.671
0.694
0.695
0.667
0.657
0.636
0,632
GIN
0.567
0.566
0.536
0.689
0.693
0.672
0.656
0.643
0.580
AC-FR-2
1,000
1.000
1,000
0,863
0.860
0,694
0.788
0.775
0.770
AC-FR-3
1.000
1,000
0.825
0.840
0.823
0.604
0.787
0.767
0.771
ACR-1
1.000
1.000
1.000
0.827
0.834
0.726
0.760
0.762
0,773
ACR-2
1,000
1.000
1,000
0.895
0.897
0.770
0,800
0.799
0.771
ACR-3
1.000
1.000
1.000
0.903
0.902
0.836
0.817
0.802
0.748
Table 2: Results E-R synthetic data for nodes labeled by classifiers (x) in Equation (6)
number of layers. This combined with the fact that random graphs that dense make the maximum distances between nodes shorter, may explain the boost performance for AC-GNNs.
Complex FOC₂ properties
In the second experiment consider classifiers (3(21) constructed as ao(x) == Blue(r),
a++1(x) II.
v(a+(v) 3IN,Mly(ar(s) -E (x).)))
(6)
where ](NMM] stands for "there exist between N and M nodes" satisfying a given property. Observe that each (z) is in FOC2, as J(NMM can be expressed by combining M and -32M+1, We created datasets with E-R dense graphs and labeled them according to an (z). a=2(x), and (3(2),, ensuring in each case that approximately half of all nodes in our dataset satisfy every property. Our experiments show that when increasing the depth of the formula (existential quantifiers with nega- tions inside other existential quantifiers) more layers (see Table 2). We report ACR-GNNS performance up to 3 layers (ACR-L in Table 2) as beyond that we did not see any significant improvement. We also note that for the bigger test set, AC-GNNs and GINs are unable to substantially depart from a trivial baseline of 50%. We tested these networks with up to 10 layers but only report the best results on the bigger test set. We also test AC-FR- with two and three layers (AC-FR-L in Table 2). As we expected, although theoretically using single readout gives the same expressive power as using several of them (Theorem 5.2), in practice more than a single readout can actually help the learning process of complex properties.
needed increase train and test accuracy
We also tested AC- and ACR-GNNG on the Protein-Protein Interaction (PPI) benchmark (Zit- nik& & Leskovec, 2017). We chose PPI since it is node classification benchmark with different graphs in the train set (as opposed to other popular benchmarks for node classification such as Core or Citeseer that have single graph). Although the best results for both classes of GNNs on PPI were quite high (AC: 97.5 F1, ACR: 95.4 Fl in the test set), we did not observe an improvement when using GNRN. Chen al. (2019) recently observed that commonly used benchmarks are inadequate for testing advanced GNN variants, and ACR-GA CRRGNNNs might be suffering from this fact.
PPI
7 FINAL REMARKS
Our results show the theoretical advantages of mixing local and global information when classifying nodes in graph. Recent works have also observed these advantages in practice, e.g., Deng et al.
8

---

Published as a conference paper at ICLR 2020
(2018) use global-context aware local descriptors to classify objects in 3D point clouds, You et al. (2019) construct node features by computing shortest-ped -att distances to a set of distant anchor nodes, and Haonan et al. (2019) introduced the idea of a "star node" that stores global information of the graph. As mentioned before, our work is close in spirit to that of Xu et al. (2019) and Morris et al. (2019) establishing the correspondence between the WI. test and GNNs. In contrast our work, they focus on graph classification and do not consider the relationship with logical classifiers.
Regarding our results on the links between AC-GNNS and graded modal logic (Theorem 4.2), we point out that very recent work of Sato et al. (2019) establishes close relationships between GNNs and certain classes of distributed local algorithms. These in turn have been shown to have strong correspondences with modal logics (Hella et al., 2015). Hence, variants of our Proposition 4.1 could be obtained by combining these two lines of work (but it not clear if this combination would yield AC-GNNs that are simple). However, these works do not investigate the impact of having non-local computations (such the readouts that we consider), hence our results on the relationships between FO an ACR-GNNs (Theorem 5.1 and 5.2) do not follow from these.
Morris et al. (2019) also studied k-GNNs, which are inspired by the k-dimensional WL test. In k-GNNs, graphs are considered as structures connecting k-tuples of nodes instead of just pairs of them. We plan to study how our results on logical classifiers relate to k-GNNs, in particular, with respect to the logic FOC; that extends FOC₂ by allowing formulas with k variables, for each fixed > Recent work has also explored the extraction of finite state representations from recurrent neural networks Fernández, 2019). We would like to study how our results can be applied for extracting logical formulas from GNNs as possible explanations for their computations.
way of explaining them (Weiss al., 2018; Koul et al., 2019; Oliva & Lago-
ACKNOWLEDGMENTS
This work was partly funded by the Millennium Institute for Foundational Research on Data?.
REFERENCES
Franz Baader and Carsten Lutz. Description logic. In Handbook of modal logic, pp. 757-819. North-Holland, 2007.
Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel- Schneider (eds.). The description logic handbook: theory, implementation, and applications. Cambridge University Press, 2003.
Peter W. Battaglia, Jessica B. Hamrick, Victor Bapst, Alvaro Sanchez-Gonzalez, Vinícius Flores Zambaldi, Mateusz Malinowski, Andrea Tacchetti, David Raposo, Adam Santoro, Ryan Faulkner, Çaglar Gülçchre, H. Francis Song, Andrew J. Ballard, Justin Gilmer, George E. Dahl, Ashish Vaswani, Kelsey R. Allen, Charles Nash. Victoria Langston, Chris Dyer, Nicolas Heess, Daan Wierstra, Pushmeet Kohli, Matthew Botvinick, Oriol Vinyals, Yujia Li, and Razvan Pascanu. Relational inductive biases, deep learning, and graph networks. CoRR, abss/8806011/ 2018. URL http: http://arxiv..oo org/ abs 110/118666.0 01261.
Jin-Yi Yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4))389 410, 1992.
Ting Chen, Song Bian, and Yizhou Sun. Are powerful graph neural nets necessary? A dissection on graph classification. CoRR, abs/1905.04579 2019. URL aattps:/arree org/ abss/ 1905. 04579.
Maarten de Rijke. A Note on graded modal logic. Studia Logica, 64(2):271-283, 2000.
Haowen Deng, Tolga Birdal, and Slobodan Ilie. PPFnet: Global context aware local features for robust 3d point matching. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, June 18-22, 2018, pp. 195-205, 2018.
hhups//imfd.elle//

---

Published as a conference paper at ICLR 2020
Matthias Fey and Jan Eric Lenssen. Fast graph representation learning with PyTorch Geometric. CoRR, abs/1103.022288, 2019. URL htt.s::/// http//aawiii.a/.aaa//////a/oaa/t orggabs//909 02428.
Justin Gilmer, Samuel S. Schoenholz, Patrick F. Riley, Oriol Vinyals, and George E. Dahl. Neural message passing for quantum chemistry. Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August, 2017, pp. 1263-1272, 2017.
William L. Hamilton, Zhitao Ying, and Jure Leskovec. Inductive representation learning on large graphs. In Advances in Neural Information Processing Systems 30: Annual Conference Neural Information Processing Systems, NIPS 2017, Long Beach, CA, USA, December 4-9, 2017, pp- 1024-1034, 2017.
Lu Haonan, Seth H Huang, Tian Ye, and Guo Xiuyan. Graph star net for generalized multi-task learning. arXiv preprini arXiv: 12X.::3006./2330, 2019.
Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempääinen, Kerkko Lu- osto, Jukka Suomela, and Jonni Virtema. Weak models of distributed computing, with connec- tions to modal logic. Distributed Computing, 28(1):31-53, 2015.
Thomas N. Kipf and Max Welling. Semi-supervised classification with graph convolutional net- works. In Proceedings of the 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, 2017.
Anurag Koul, Sam Greydanus, and Alan Fern. Learning finite state representations of recurrent pol- icy networks. In Proceedings of the 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019.
Carsten Lutz, Ulrike Sattler, and Frank Wolter. Modal logic and the two-variable fragment. In Proceedings of the International Workshop on Computer Science Logic, CSL 2001, Puris, France, September 10-13, 2001, pp. 247-261. Springer, 2001.
Christian Merkwirth and Thomas Lengauer. Automatic generation of complementary descriptors with molecular graph networks. J. of Chemical Information and Modeling, 15(9):1159-1168 2005.
Christopher Morris, Martin Ritzert, Matthias Fey, William I.. Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe. Weisfeiler and Leman go neural: higher-order graph neural networks. In Proceedings of the 33rd AAAI Conference on Artificial Intelligence, AAAI 2019, Honolulu, Hawaii, USA, January 27 February 1, 2019, pp. 4602 4609, 2019.
Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, Achille Fokoue, and Carsten Lutz. OWL 2 Web ontology language profiles (second edition). W3C recommendation, W3C, 2012.
URL http: / www. w3 wwwoorrrrr.... TR/ ow1--poffiles//
Christian Oliva and Luis Fago--Feráánez. On the interpretation of recurrent neural networks as finite state machines. In Part of the Proceedings of the 28th International Conference on Artificial Neural Networks, ICANN 2019, Munich, Germany, September 17-19, 2019, pp. 312- 323. Springer, 2019.
Martin Otto. Graded modal logic and counting bisimulation. https: /ttp///wwww//// ma mattematikk. Cu-darmstades -ote/ootte /apprrs/////////pa/peeeeee ccmmmm999 19. pdf, 2019.
Ryoma Sato, Makoto Yamada, and Hisashi Kashima. Approximation Ratios of Graph Neural Net- works for Combinatorial Problems. arXiv preprint arXiv: /905. 10261, 2019. 2019.
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Trans. Neural Newworks, 20(1):61-80, 2009.
Michael Sejr Schlichtkrull, Thomas N. Kipf, Peter Bloem, Rianne van den Berg, Ivan Titov, and Max Welling, Modeling relational data with graph convolutional networks. In Proceedings of The Semantic Web 15th International Conference, ESWC 2018, Heraklion, Crete, Greece, June 3-7, 2018, pp. 593 607, 2018
10

---

Published as a conference paper at ICLR 2020
W3C OWL Working Group. OWL 2 Web ontology language document overview (second edition). W3C recommendattion, W3C, 2012. URL https:/ /www. . w3 2twp/////o/22-ovvvveeee
Boris Yu. Weisfeiler and Andrei A. Leman. A Reduction of graph to a canonical form and an algebra arising during this reduction. Kauuchno-Technicheskaya Informatsia. 2(9):12-16, 1968. Translated from Russian.
Gail Weiss, Yoav Goldberg, and Eran Yahav. Extracting automata from recurrent neural networks using queries and counterexamples. In Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmüssan, Stockholm, Sweden, July 10-15, 2018, pp- 5244-5253, 2018.
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How Powerful are graph neural networks? In Proceedings of the 7th International Conference Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019.
Jiaxuan You, Rex Ying, and Jure Leskovec. Position- graph neural networks. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, Long Beach, California, USA, June 9-15, 2019, pp. 7134-7143, 2019.
Marinka Zitnik and Jure Leskovec. Predicting multicellular function through multi-layer tissue networks. CoRR, abs//a/0..///0// 04768488, 2017. URL http: // //arxvv.. wrg./bs/g abs//70b 04638.

---

Published as a conference paper at ICLR 2020
APPENDIX
A PROOF OF PROPOSITION 3.3
We first recall the proposition.
Proposition 3.3. There is an FOC₂ classifier that is not captured by any AC-GNN.
Proof. Consider the following FOC₂ node property a(v) = Red(v) A Br Green(x). We will show by contradiction that there is AC-GNN that captures no matter which aggregation, combining, and final classification functions are allowed. Indeed, assume that AA is an AC-GNN capturing a, and let L be its number of layers. Consider the graph G that is chain of L + 2 nodes colored Red, and consider the first node up in that chain. Since A captures a, and since (G, Up) J/z a. we have that A labels vo with false, i.e., A(G, vo) = false. Now, consider the graph G' obtained from G by coloring the last node in the chain with Green (instead of Red). Then one can easily show that A again labels vo by false in G". But we have (G", vo) } a. a contradiction.
The above proof relies on the following weakness of AC-GNNs: if the number of layers is fixed (i.e., does not depend on the input graph), then the information of the color of a node cannot travel further than at distance L from v. Nevertheless, we can show that the same holds even when we consider AC-GNNs that dispose of an arbitrary number of layers (for instance, one may want to run homogeneous AC-GNN for S((El) layers for each graph G (V, E). for fixed function J)- Assume again by way of contradiction that A such an extended AC-GNN capturing a. Consider the graph G' consisting of two disconnected nodes u, with colored Red and y colored Green. Then, since (G, v) == a, we have A(G, v) = true. Now consider the graph G' obtained from G by changing the color of from Green to Red. Observe that, since the two nodes not connected, will again have A(G', = true, contradicting the fact that (G', v) ffr a and that A is supposed to capture a.
By contrast, it is easy to see that this formula can be done with only one intermediate readout, using the technique in the proof of Theorem 5.1.
B PROOF OF PROPOSITION 4.
We first recall the proposition. Proposition 4.1. Each graded modal logic classifier is captured by a simple homogeneous homogeneoussA-GGMM AC-GNV.
We first define formally the semantics of the graded modal logic (de Rijke, 2000) simple undi- rected node-colored graphs (de Rijke, 2000), assuming the FO syntax introduced the paper.
Definition B.1. We define when a node v in a graph G satisfies a graded modal logic formula spxx), written = ip G (where "in G" may be omitted when clear), recursively follows:
ff((x) Col(x), then v -= if and only if Col is the color of u in G,
ff(x) :p (x:) (x)), then }= up if and only if }= up and x²", and similarly with (x), and
if if = (2N( v) (v)), then v F y if and only the set nodes {u E (N((v) and == ) has cardinality at least N.
We now proceed to the proof of the proposition.
Proof of Proposition 4.1. Let spz) be a graded modal logic formula. We will construct an AC- GNN A, that is further simple and homogeneous. Let sub({²) (411, (41,, (2,............................. PL. be an enumer- ation of the sub-formulas of oo such that if şp is subformula se then < The idea of the construction of A, is to have feature vectors in R- such that every component of those vectors represents a different formula in sub(p). Then Ap will update the feature vector x:(" of node
ensuring that component & of a gets value 1 if and only if the formula you is satisfied in node
12

---

Published as a conference paper at ICLR 2020
We note that yp PL and thus, the last component of each feature vector after evaluating L layers in every node gets a value if and only if the node satisfies y. We will then be able to use a final classification function CLS that simply extracts that particular component.
Formally, the simple homogeneous AC-GNN Ag has L layers and uses the aggregation and combine functions
AGG(X) = Σ x
wEX
COM(( y) o o YA b))
where A, C E R and b E R are defined next, and the truncated ReLU activation defined by (z) = min(max((,.0) 2), The entries of the f-th columns of A, C, and depend on the sub-formulas of y as follows:
Case 0. if pe(r)) Col(x) with Col one of the (base) colors, then Cze 1,
Case 1. if (p(x)) (z) (z) then Cye Cke and by 11
Case 2. if pe(x) -Pp (z) then Ckt -1 and by 1,
Case 3. if (e(x)) (22N(F(2) y) A (v())) then Ake and by -
and all other values in the ê-th columns of A, C. and b are O.
We now prove that A, indeed captures şp Let G = (V, F)) he a colored graph. For every node e in G we consider the initial feature vector 2!!)) (01,---,,5I, (Tr. such that æy 1 if sub-formula for is the initial color assigned to and
otherwise, By definition, AC-GNN A, will iterate the aggregation and combine functions defined above for rounds (L layers) produce feature vectors
2y for every node v E G and & = 1,..., L as follows:
(t)
a!!)
COM(2! x
AGG (i-1) (uE((())))
(1-
Σ
x (i-1)
A A+b).
uENiu)
We next prove that for every fpr E sub((p), every (L...., , ), and every node in G it holds that
= 1 if - ses and (x!
otherwise,
(8)
where (zx is the l-th component of x (i) that is, the L-th component of x has if and only if
v satisfies yo in G. In the rest of the proof we will be continuously using the value of (x (xx()) whose general expression is
L (
(arl
Σ (
E Σ(ar E be). k=
We proceed to prove (8) by induction on the number of sub-formulas every yg. If (p has one sub-for sub-formula, then (r((x) Col(x) with Col base color. We next prove that (a. ) 1 if and only e has Col as its initial color. Since fp((x) = Col(x)) we know that Ca: and Cur = 0 for every h: + & (see Case 0 above). Moreover, we know that by 0 and Age 0 for every k. Then, from Equation (9) we obtain that
L
(x("))e = o (
a 0 [x
( Cke+ {v.))Ek==
Σ (a= + be) = ((
1=1
Then, given that (2o )r
if the initial color of is Col and (x: (0) O otherwise, have that (x (1) = if (G,v) v) } SP and (x!"), = otherwise. From this is easy to prove that for
(0)
every i > 1 the vector (x ) satisfies the same property. Now assume that 4o has more than
13

---

Published as a conference paper at ICLR 2020
sub- formula, and assume that for every Ps with k the property (8) holds. Let 2 l. We are left to consider the following cases, corresponding to the cases for the shape the formula above.
Case 1. Assume that (e(()) (x) A (x). Then Cje Cse 1 and by -1. Moreover, we have Cmu = 0 for every m o j. k and Ane 0 for every n (see Case above). Then, from Equation (9) we obtain that
(ar (((a + ()) -x
Since the number of each proper sub-formula of Pe is strictly less than both and i, by in- duction hypothesis know that (x) (x) 1 if and only if v - Pj and (x) (2- D) 0
otherwise. Similarly, (xl (xx(111) ) = if and only if v F sP and (w ( ) = 0 otherwise. Now, since (ar ) ((xb-)))
1 if and only if (xe! (elf-"));= + (x) ((((-11) -1 1 that can only happen if (x:"-"); = (x 1-11) )a = 1. Then (x 1 =1
(8)
(o.--)) --1) 1) we have that (al (1) )e
and only v F P4 and F pa- that is, if and only if v == pe (since pe(x) p)(x) (x(()),
and (x: (8) 2 = 0 otherwise. This is exactly what we wanted to prove.
Case 2. Assume that (p(()) (x)( Then Cke for every f k and Ane for every (see Case above). Then, from Equation (9) we obtain that
and be = Moreover, we have Cim
(xr!i- (m = σ - +1)
By induction hypothesis we know that (w (
if and only if -= spu and (a!! (x ) = oth- we have that (a:!"), ) = 1 if and only if 1- (a )) 2
erwise. Since (x: (8) )e o-- (xx (f-1)) )x +1)
shx-that that can only happen if (a.)- (= ) O. Then (xr²)) )r if and only if if yok that is, and only
(8) 0 otherwise. This is exactly what we if v == Pk, which holds if and only if v + spe, and (ar wanted to prove.
Case 3. Assume that (pe(ar) = 9NP (F( v) A (v)). Then Are = 1 and by = - 1. Moreover for every m we have that Cmn (see Case above). Then, from Equation (9) we obtain that
(ol))e o CC-N+1+
Σ (a(- {u.oEE
By induction hypothesis we know that (x: (1-1)) )bc 1 if and only if v -= spk and (x ( 0 otherwise. Then we can write (a )2 o--N + m) where
(u u E (wv) and -= xpx)
() )e = 1 if and only if m > N, that is if and only if there exists at least N nodes connected with that satisfy (pk, and (zo ) otherwise. From that obtain that (x (e) )r = if and only if o } sor since (e(x) = 2N (E(æ, v) A px(y)), which is what we wanted prove.
Thus, we have that (x
To complete the proof we only need to add a final classification after the L iterations of the aggregate and combine layers that simply classifies node true if the component of ((()) corresponding to holds 1.
C PROOF OF THEOREM 4.2
We first recall the theorem.
Theorem 4.2. logical classifier is captured by AC-GNNs if and only if it can be expressed in graded modal logic.
Note that one direction follows immediately from Proposition 4.1, so we only need to show the following proposition.
14

---

Published as a conference paper at ICLR 2020
Proposition C.I. If a logical classifier is not equivalent any graded modal logic formula, then there is no AC-GNN that captures a.
To prove this proposition, we will need the following definition, which standard modal logics theory.
Definition C.2. Let G be graph (simple, undirected and node-colored), be a node G, and N. The unravelling of u in G at depth L, denoted by (nra(v), is the (simple undirected node- colored) graph that is the tree having
node (u, u1..... for each path (v, Ui,...,, Us) in G with S L,
an edge between (v, u1,..., u1-1) and (v, oyy.. u.) when {ue-1, (,t-,,,5) us} is an edge in G (assuming that is v), and
each node (v, u.) colored the same as us in G.
We then observe the following.
Observation C.3. Let G and G' be two graphs, and and of be two nodes in G and G', respectively. Then for every T. E N, the WI. test assigns the same color to and of at round I. if and only if there is an isomorphism between Unr (v) and Unr (v') sending to v'.
We will write (v) = Unr (u") to denote the existence of the isomorphism as in this observa- tion. To prove Proposition C.I, we first rephrase Proposition 2.1 in terms of unravellings.
Proposition C.4. Let G and G' be two graphs with nodes in G and v' in G' such that (v) (1') for every L N. Then for any AC-GNN A, we have A(G, u) A(G'',
Proof. Follows directly from Proposition 2.1 and Observation C.3.
The crucial part of the proof of Proposition C.I is the following non-trivial result, intuitively es- tablishing that the fragment of unary FO formulas that only depend on the unravelling of node is exactly the graded modal logic.
Theorem C.5 (Otto, 2019). Let a be a unary FO formula. If a is not equivalent to a graded modal logic formula then there exist two graphs G, G' and nodes in G and ut in G' such that (v) Unrig (v') for every L E N and such that F= in G but ut If in G¹.
Proof. This directly follows from the van Benthem & Rosen characterization obtained in (Otto, 2019, Theorem 2.2) for finite structures (graphs), by noticing that for the notion of graded bisimula- tion + introduced in this note, we have that G, ~ G', u' if and only if we have that (v) Unrt, (v') for every
N. We point out here that the fact that the edge relation G is undirected in our setting (as opposed to E being directed in (Otto, 2019)), and the fact that every node can only have one color in our setting (as opposed to being able to satisfy multiple "unary predicates" in (Otto, 2019)) are inessential, and that the proof of (Otto, 2019, Theorem 2.2) carries over to this setting.
We can now gather all of these to prove Proposition C.I.
Proof of Proposition C.I. Let be logical classifier (i.e., unary FO formula) that is not equiva- lent to any graded modal logic formula. Assume for a contradiction that there exists an AC-GNN A, that captures a. Since is not equivalent to any graded modal logic formula, by Theorem C.5 there exist two graphs G, G' and two nodes in G' and w' in G' such that Unr (1)) ~ Unr (v") for ev- ery L N and such that (+) For in G but ue f in G'. Since we have that Unr F. (v) Unr (v') for every L E N. by Proposition C.4 we should have that A, (G, u) = A,,",, w²). But this contra- diets (x) and the fact that Ar is supposed capture a.
15

---

Published as a conference paper at ICLR 2020
D PROOF OF THEOREM 5.1
We first recall the theorem.
Theorem 5.1. Each FOC₂ classifier can captured by a simple homogeneous ACR-GNN.
To prove the theorem, will characterization of the unary FOC₂ formulas provided by (Lutz et al., 2001) that uses a specific modal logic. That logic is defined via what are called modal param- eters. We adapt the definitions of (Lutz et al., 2001) deal with simple undirected node-colored graphs.
Definition D.I. A modal parameter is an expression built from the following grammar:
S ::=id id IISSSS Sns -S.
Given undirected colored graph G = (V, F) and node v of G, the interpretation of S on is the set Es(v) C V defined inductively as follows:
if S id then es(v) = {u);
ifS S e then Es( = {u {u, v) E):
S 51 S2 then Es(U) Es, (o) (v);
S = S1 S2 then Es(U) = Es, (v) n nes
- Sf = -S' then Es(U) = (Es(U).
The modal logic EMCC consists of all the unary formulas that are built with the following g grammar:
9 == C' llp -ip ( S
where C ranges over node colors, S over modal parameters, and N over N. The semantics of the first four constructs is defined as expected, and for an undirected colored graph G == (V, E) and node E V. we have (G,v) - (S)2N if and only if there exist at least N nodes u in ES(U) such that (G, u) 1 sp.
Example D.2. On undirected graph G EV, the EMCC formula (-e) ((e)22
holds on node E V if v has at least two nonadjacent nodes u (and since our graphs have no self-loops, could be u) such that has at least three green neighbors.
The following theorem is essentially reformulation of (Lutz et al., 2001, Theorem 1) to our context (Lutz al. (2001) show this for FO2 without counting quantifiers and for EMLCC without counting, but an inspection of the proof's reveals that the result extends to counting quantifiers).
Theorem D.3 (Lutz et al., 2001, Theorem 1). For every EMCC formula, there exists an equiv- alent FOC₂ unary formula. Conversely, for every unary FOC₂ formula, there exists an equivalent EMLC formula.
In order to simplify the proof, we will use the following lemma.
EMLCCoorull Lemma D.4. Let yp be an EMLC formula. Then there exists an EMCC formula sp' equivalent ip such that each modal parameter appearing in yo! is one of the following:
a) id, thus representing the current node;
b) e, thus representing the neighbours of the current node;
c) -e n n thus representing the nodes distinct from the current node and that are not neighbours of the current node;
d) id c, thus representing the current node and its neighbors;
e) id, thus representing all the nodes distinct from the current node:
f) -e thus representing the nodes that are not neighbours of the current node (note that this in- cludes the current node);
16

---

Published as a conference paper at ICLR 2020
g) U -e, thus representing all the nodes;
h) en -e, thus representing the emptyset.
Proof. Let e be node in graph G, and consider the following three disjoint sets of nodes:
1. the singleton set consisting of e itself,
2. the set of neighbors of v,
3. the set of nodes that are not neighbors of e and that are not v.
These sets can be expressed by modal parameters: the first is obtained by taking S = id; the second obtained by taking S e, and the third is obtained by taking S = -e -id. It is straightforward to verify by induction on S that, for any modal parameter S, if Es(v) contains the three sets, then it must contain all the elements of that set. But then, this implies that a modal parameter only represent (possibly empty) disjoint union of these three sets. Conversely, it is clear that any disjoint union over these three sets can be represented by a modal parameter. It is then routine check that the 8 cases (a)-(h) are obtained as all the 2 possible unions of these three sets (including the empty union, i.e., the emptyset). For instance, case (f) is the union of sets and 3. n
element of one of
Proof of Theorem 5.1. The proof is similar to that of Proposition 4.1. Let yp be an EMCC formula equivalent to the targeted FOC₂ unary formula that is of the form given by Lemma D.4, and let sub(yp = (4P), (P,,...................... (P2;.....P)))................... Pr.) be an enumeration of the sub-formulas of yp such that if you is a sub- formula of Po then k S E. We will build simple homogencous ACR-GNN Ap computing feature vectors x in RT such that every component of those vectors represents a different formula in sub(p). In addition, we will also make use of global feature vectors TG in R., The GNN Ap will update the feature vector x of each node e in a graph ensuring that component é of (.()) gets a value 1 if and only if the formula fe is satisfied in node (and 0 otherwise). Similarly, DG will be updated to make sure that every component represents the number of nodes in G that satisfy the corresponding subformula. The readout and aggregate functions simply sum the input feature vec- tors. When for is of the form described by Cases 0-3 in the proof of Proposition 4. 1, we define the f-th columns of the matrices A, C and bias b as in that proof, and the f-th column of R (the matrix that multiplies the global readout feature vector) as the zero vector. We now explain how we define their 8-th columns when ye of the form (5) 2 ypu, according the 8 cases given by Lemma D.4:
(x)
(e)
Case a. if pr = (id) 2N sp. then Cit = 1 if N = and otherwise;
Case b. if 1: (e)22 Sk. then Aue = 1 and b. = - + 1;
Case if 4e (-e 0 id N pp. then R&z = and Cse = Ase = -1 and by -N + 1;
Case d. if 12 (id U e) N sk. then Cse 1 and A = 1 and b -N + 1;
Case e. if 42 (-id) 2 pk. then R&s and Ckt 1 and be - + 1:
Case f. if 40 (-e) 2 pp then Rgg 1 and Aue -1 and by NN + 1:
Case 8. if up (e U -e) 22 pkk
then R&t and b - 1;
Case h. if up = (e n - Sr. then all relevant values are O;
and all other values in the é-th columns of A, C, R. and b are 0. The proof then goes along the same lines as the proof of Proposition 4.1.
E PROOF OF THEOREM 5.2
We first recall the theorem.
Theorem 5.2. Each FOC₂ classifier is captured by an AC-FR-GNN.
17

---

Published as a conference paper at ICLR 2020
In the following proof we will use the machinery introduced in Appendices C and D. We will also make use of a particular AC-GNN with L layers, which we call A Aprimess that maps every node v in graph G' to a natural number representing the complete unravelling of of depth L in G (note that we do not claim that this AC-GNN can be realized in practice, this construction is mostly for theoretical purposes). Let primes N N be the function such that primes(i) is the i-th prime number indexed from O. For instance, we have that primes(O) = 2. primes(() = 3, etc. Now consider the function -(:-)) that has input pair (c, where c e N and X is multiset of numbers in N, and produces a number in N as output, defined as follows
f(c, 11 F2.
D = 2 x II primes(2; + 1).
It is not difficult to prove that, as defined above, f(.. -) is an injective function. Thus using the results by Xu al. (2019) (see the proof of their Theorem 3) we know that can be used to implement the combine and aggregate operators of an AC-GNN such that for every graph G, after L layers, the color (natural number) assigned to every node in has a one to one correspondence with the color assigned to that node in the L-th iteration of the WL test over G. We call this AC-GNN Aprimes.
Observation E.1. We note that Xu et al. (2019) also constructed an injective function that has (c, X) as inputs where c E N and is a multiset of elements in N (see their Lemma 5 and Corollary 6). Nevertheless we cannot directly use that construction it assumes the existence of fixed N such that the size of all multisets are bounded by N. This would pul also a bound of N on the maximum number of neighbors in the imput graphs. Thus we developed new function (using an encoding based on prime numbers) to be able to deal with general graphs of unbounded degree.
Proof of Theorem 5.2. Let a be an FOC, unary formula, and let şo be an equivalent &M formula that uses only modal parameters of the form given by Lemma D.4. We construct an ACR-FR-GNN Ap capturing yp and hence a.
Let L. be the quantifier depth of yp (i.e., the deepest nesting of (5)2N quantifiers). For a subfor- mula yp of yp, we also define the nesting depth ((p') of y in yp to be the number of modal param- eters under which vf is in yp. The first L layers of Ap are the same as those of Apriues which do not use readouts. With Observation C.3 hand and using the fact that the inverses of the aggregation and combination functions of Aprimes
computable, this ensures that, after L 1 layers, for any graph G and node v in G. we can compute from A primes (G, v) the unravelling Unrg Unrt-1(u) (w). Thus, we can assume without loss of generality (by modifying the last combination function for instance), that after L 6-11 layers Ag computes Unr (v) in every node v of G. We then use readout whose out- put is a natural number representing the multiset Unrr 4-11 11(() (w) | node in G for instance, we can encode this multiset using the same technique that we use for Aprimes. Again, since this technique uses functions with computable inverses, we can assume without loss of generality that the output of this readout is actually the multiset { Unri (v)) e node in GJ. Finally, we use final combination function (4M that uses only the feature of the current node and the output of the readout- is, the final feature of node u COM (Unr' (v)), { (Unra='(ur (u) node in G
We now explain how we define ( By induction on the structure of for every subformula o of yp. we do the following: for every node in and every node u in Unr Aur--1(6 (v) that is at depth (i.c., the distance from v) at most (d'(""") in the tree Unry (v), we will label u by either sp' or by -up.. We do so to ensure that (x) for every node in G and every node = (v, u1...., u;) in Unr--1 (v)) we label u by sf if and only if (G, u,) F vp. We explain our labeling process by induction on the structure of sp, and one can easily check in each case that (+) will hold by induction. Let be node in G and be a node in Unrg- A-1 (v) that is at depth at most (yg" ) in the unravelling.
Case 1. If yp is color Col, we label u by yp if u of that color, and by myy otherwise.
(d2)) so that is at depth at most both (P1) and nd in the unravelling Unr f.- (v). Thus, we know that have already labeled u by either i or mip and also by either (o2 or 442 We then label u by of if u is already labeled by foi and 42, and we label it by mpp otherwise.
Case 2. If op is 40 A 92, then observe that we have (x') = nd (d1(
18

---

Published as a conference paper at ICLR 2020
Case 3. The case when y' is negation is similar.
Case 4. If o is (S) p", then we only explain the case when the modal parameter S'is -e A iid, as the other cases work similarly. First, observe that for every node v' in G, we have labeled the root of Unrk-1(p Unrd by either s" or by -pp:: this is because the root of Unrg-t is always at depth 0 S ndd( in Unrg-t(u)). Let m be the number of nodes w' G such that have labeled the root of Unrg-1 (1') ) by y". Next, note that for every children u' of u in Unrg- (v), we have that u' is at depth at most ndp()"") in Unrg-' (v), so that we have already labeled u' by either yp" or =pp.. Let n be the number of children of u (in Unra 144--((0 (c)) that we have labeled by s". Then we label by of if
N, and by -up' otherwise.
We then simply define COM (Unrd) [Unr (u) | u node in GB) to be if the root of Un) is labeled with sp, and 0 otherwise, which concludes the proof.
(v)
F DETAILS ON THE EXPERIMENTAL. SETTING AND RESULTS
All code and data be accessed online at https::/ggttub..cmm// GNN-logic
In all our experiments tested different aggregate, combine and readout functions. For aggregate and readout we only consider the sum, average, and max functions. For the combine function we consider the following variants:
COM (z. v) = f(x.A + B + 2C + b),
COM2 xz, y. 2) f(MLP (z) + MLP2(y) + MLP3(z)+ + b).
COM y. = MLP((z + y + b),
COM (2, y. MLP(#A+ + yB bb)
The above definitions are for ACR-GNNs. For AC-GNNs we consider similar variants but without the z input. We also used batch normalization in between every GNN and MLP layer. We did not use any regularization. When processing synthetic data a batch-size of 128, and the Adam optimizer with PyTorch default parameters for 50 epochs. We did not do any hyperparameter search besides changing the aggregation, combination, and readout functions. For the activation functions we always used relu. We observed a consistent pattern in which sum aggregator and readout produced better results compared with the others. This is line with our constructions in Proposition 4.1 and Theorem 5.1. The choice of the combination function did not produce a significant difference in the performance.
hidden size of 64 and trained with
DATA FOR THE EXPERIMENT WITH CLASSIFIER axx) == RED(z) (z) A By BLUE(V)
For training and testing we constructed three sets of graphs: (a) Train set containing 5k graphs with nodes between 50 and 100, (b) Test set, same size, containing 500 graphs with the same number of nodes as in the train set (between 50 and 100 nodes), and (c) Test set, bigger size, containing 500 graphs with nodes between 100 and 200. All graphs contain up to 5 different colors. To force the models to try to learn the formula, in every set (train and test) consider 50% of graphs not containing any blue node, and 50% containing at least one blue node. The number of blue nodes in every graph fixed to a small number (typically less than 5 nodes). Moreover, to ensure that there is a significant number of nodes satisfying the formula, we force graphs to contain at least I/4 of its nodes colored with red. The colors of all the other nodes are distributed randomly. With all these restrictions, every dataset that we created had at least a 18% of nodes satisfying the property. We consider two classes of graphs: line graphs and Ardös-Renyl graphs.
Line graphs these are connected graphs in which every node in the graph has degree 2 except for two nodes (the extreme nodes) that have degree To mimic the impossibility proof in Propo- sition 3.3 we put the blue nodes in one of the "sides" of the line, and the red nodes in the other "side". More specifically, consider the line graph with N nodes vi,...,20 uN such that e; is connected with U1+1. Then, we ensure that every blue node appears in one of uI,..., uy and every red node appears in one of +13--rg UN-
19

---

Published as a conference paper at ICLR 2020
# Graphs
Avg. # Nodes
Avg. Edges
Avg. # Positive
Line train
5,000
75
74
18
Line test
500
74
18
Line test bigger
500
148
147
36
Erdös-Renyi train
5,000
18
Redös-RReyi test
500
75
115
18
Pedös--Reyi test bigger
500
148
226
36
Table 3: Synthetic data for the experiment with classifier a(x) = Red(x) By Blue(y)
Frdös-Renyi 20%
Frdös-Renny 50%
Erdös-Renyi 100%
Train Acc.
Test Acc.
Train Acc.
Test Acc.
Train Acc.
Test Acc.
same-size
bigger
same-size
bigger
same-size
bigger
AC-2
0.810
0.807
0.778
0,829
0.835
0.791
0.861
0.864
0.817
AC-5
0,940
0,937
0,901
0,975
0.971
0,958
0.994
0,994
0,993
AC-7
0,963
0.961
0.946
0.983
0.978
0.981
0.995
0.995
0.995
GIN-2
0.797
0.795
0.771
0,813
0.818
0.784
0.838
0.840
0.803
GIN-5
0.838
0.836
0.819
0.846
0.847
0.833
0.841
0.844
0.838
GIN-7
0.838
0.840
0.803
0.841
0.844
0.838
0.784
0.788
0.773
ACR-1
1.000
1.000
1.000
1.000
1.000
1.000
1.000
1,000
1.000
Table 4: Detailed results for Erdös-Renyi synthetic graphs with different connectivities
Brrdös-Renyi graphs These are random graphs in which one specifies the number N of nodes and the number M of edges. For this experiment consider as extreme cases the case in which graphs contain the same number of nodes and edges and graphs in which the number of edges is twice the number of nodes.
Some statistics of the datasets are shown in Table 3.
EXPERIMENTS FOR DENSE ERDÖS-RENY GRAPIS
We also took a closer look the performance for different connectivities of random graphs (Table 4). We define the set "Erdös-Rens larger than the number nodes. For example, "Erdös-Renyi + 100%" contains random graphs in which the number of egdes doubles the number of nodes. We see consistent improvement in the performance of AC-GNNs and GINs when we train and test them with more dense graphs and more layers (Table 4).
1%% as set of graphs in which the number of edges is 1%
DATA THE EXPERIMENT WITH CLASSIFIER (1x()) IN EQUATION (6)
For this case we only consider dense Erdös Erdös-Renyi synthetic graphs. For the train set we consider graphs with nodes varying from 40 to 50 nodes and edges from 280 to 350 and similarly for the first test set. For the bigger test set, we consider graphs with nodes from 51 to 60 with edges ranging from 360 and 480. For labeling consider the following formulas (starting from ax Blue(x))::
(1(x)
8. y(ao()) -E(x,))),
a2(x) = I 3000200 ((a -E(z, y))
ax(x) = =10.80 A E(x. v))
The choices of the intervals for every classifier were for the pourpose of having approximately half of the nodes in the random graphs marked as true. Statistics of the datasets shown in Table 5.
20

---

Published as a conference paper at ICLR 2020
Graphs
Avg. # Nodes
Avg. # Edges
Pos. 01
Pos. dz
Pos. 0g
Train
5,000
45
315
47%
63% 64%
57%
Test 500
45
315
47%
56%
Test bigger
500
56
420
49%
40%
23%
Table 5: Synthetic data for the experiment with classifier (z in Equation (6)
F1 Test
AC-2
97.2 + 0.3
AC-3
97.5 + 0.3
AC-4
97.5 0.2
ACR-2
93.5 0.3
ACR-3
94.2 + 1.2
ACR-4
95.4 0.9
Table 6: Performance of AC-GNN and ACR-GNN in the PPI benchmark
PPI EXPERIMENTS
We consider the standard train/validation/ees split for this benchmarck (Fey Lenssen, 2019). We use hidden size of 256 and the Adam optimizer for 500 epochs with early stopping when the validation set did not improve for 20 epochs. We did not do any hyperparameter search besides changing the aggregation, combination, and readout functions. As opposed to the synthetic case, in this case we observed a better performance when the average or the max functions are used for aggregation. Table 6 shows the best results for different layers (average of 10 runs). As ACR-GNNs do not imply an improvement over AC-GNNs for this benchmark.
see,
21


Reviews:
[{"review_id": "r1x495CRqH", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper establishes novel theoretical connections between Boolean node classifiers on aggregate-combine Graph Neural Networks (AC-GNNs) and first-order predicate logic (FOC2). It shows that current boolean node classifiers on AC-GNNs can only represent a subset of FOC2 but that a simple extension taking into global information can generalise AC-GNNs to the full FOC2.\n\nThe style of the manuscript is mixed: the abstract and introduction are quite dense for non-experts; a motivating real-world example could help here. The other sections, on the other hand, are quite good to follow and most concepts have a good high-level introduction as well as a little example to follow the arguments.\n\nThe theoretical connections connection between GNNs and first-order logic strike me as interesting. I did not, however, understand the results reported in table 2: ACR reaches optimal performance only on alpha_1 but not on alpha_2 and alpha_3. Does this happen because the latter two expressions are not part of FOC2?\n\n---\nI increased my rating due to the author rebuttal.", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I made a quick assessment of this paper.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "r1egYwC6tr", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper utilizes recent insights into the relationship between the Weisfeiler-Lehman (WL) test for checking graph isomorphism and Graph Neural Networks (GNNs) in order to characterize the class of node classifiers that can be captured by a specific GNN architecture, called aggregate-combine GNN (AC-GNN). \n\nThe primary contribution of this work is the identification of the logical classifiers that can be represented within an AC-GNN, a fragment of first order logic called graded modal logic, as well as an extention of AC-GNNs with the ability to capture a strictly more expressive fragment of first order logic, called ACR-GNN. Both of these results are supported by formal proofs and derivations, adding not only theoretical value to the presented work, but also intuitive insights behind the reasons of the AC-GNN limitations. In addition, the presented experiments demonstrate the practical implications of the results, with the exception of some datasets where no significance difference in performance between AC-GNNs and ACR-GNNs was found.\nI believe that the contributions of this paper are significant. On the one hand, studying theoretical properties of GNNs facilitates their transparency and highlights the range of applications they can be used in. On the other hand, although the GNN variant introduced by the author is a special case of an existing class of GNNs, the motivation behind its introduction is different and follows naturally from the discussion within the paper.\n\nThe fact that no actual difference in performance between AC-GNNs and ACR-GNNs was noticed in the only non-synthetic dataset used in the experiment should prompt the author to run experiments with more real life datasets, in order to empirically verify the results, but this is a minor point.", "extra_scores": {"experience_assessment": "I have published one or two papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I did not assess the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "H1ezHHmAtB", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper elaborates on the expressivity of graph neural networks (GNNs). More precisely, the authors show that expressivity of AC-GNNs (aggregate and combine) can only express logical classifiers that can be expressed in graded modal logic. By adding readouts, ACR-GNNs (aggregate, combine and readout) can capture FOC2 which is logical classifiers expressed with 2 variables and counting quantifiers. The second theorem leaves open the question of whether ACR-GNNs can capture logical classifiers beyond FOC2.\n\nThe paper is written nicely, its easy on the eyes, and delegates the proofs to the appendix. I was a bit surprised by the lack of a discussion connecting the choice of the aggregate and combine operations to the representation power of GNNs. One has to delve deep into the proofs to find out if the choice of these operations affects expressivity.", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper focuses on characterizing the expressiveness of graph neural networks. The reviewers were satisfied that the authors answered their questions suffciiently and uniformly agree that this is a strong paper that should be accepted.
Decision: Accept (Spotlight)