Sound Logical Explanations for Mean Aggregation Graph Neural Networks
Authors: Matthew Morris
Ian Horrocks
Venue: NeurIPS 2025 poster ()
Keywords: graph neural networks
explainability
formal logic
expressivity
Primary area: theory
TL;DR: We consider graph neural networks with mean aggregation and non-negative weights, showing which monotonic rules they can learn and constructing sound explanatory rules.

Abstract: Graph neural networks (GNNs) are frequently used for knowledge graph completion.
Their black-box nature has motivated work that uses sound logical rules to explain predictions and characterise their expressivity.
However, despite the prevalence of GNNs that use mean as an aggregation function, explainability and expressivity results are lacking for them.
We consider GNNs with mean aggregation and non-negative weights (MAGNNs), proving the precise class of monotonic rules that can be sound for them, as well as providing a restricted fragment of first-order logic to explain any MAGNN prediction.
Our experiments show that restricting mean-aggregation GNNs to have non-negative weights yields comparable or improved performance on standard inductive benchmarks, that sound rules are obtained in practice, that insightful explanations can be generated in practice, and that the sound rules can expose issues in the trained models.

Sound Logical Explanations for Mean A Aggregation Graph Neural Networks
Matthew Morris
Ian Horrocks
Department of Computer Science
Department of Computer Science
University of Oxford
University of Oxford ian horrokococssss. .ucuk
matthew.morrisee ac.uk
Abstract
Graph neural networks (GNNs) are frequently used for knowledge graph com- pletion. Their black-box box nature has motivated work that uses sound logical rules explain predictions and characterise their expressivity. However, despite the prevalence of GNNs that use mean as aggregation function, explainability and expressivity results are lacking for them. We consider GNNs with mean aggrega- tion and non-negative weights (MAGNNs), proving the precise class of monotonic rules that can sound for them, as well as providing a restricted fragment first-order logic to explain any MAGNN prediction. Our experiments show that re- stricting mean-aggregation GNNs to have non-negative weights yields comparable improved performance standard inductive benchmarks, that sound rules are obtained in practice, that insightful explanations can be generated in practice, and that the sound rules can expose issues in the trained models.
1 Introduction
Knowledge graphs (KGs) [17] find use in number of applications [16, 41, 45]. However, KGs are often incomplete, creating the need for models to predict their missing facts. Neural models such as graph neural networks (GNNs) [13] are frequently used for this task [18, 22, 25], as well variety of others, including predicting properties of drug combinations [9] and recommender systems [11].
However, the predictions of neural models cannot easily be explained and verified [12]. In contrast, logic-based and neuro-symbolic methods for KG completion often yield logical rules which can be used to explain predictions [24, 29, 31, 46]. To ensure that the rules truly express the reasons why the model makes particular prediction, it is important to ensure that they are sound, in the sense that applying the rules an arbitrary dataset produces only facts that are predicted by the model. Thus, there is growing interest in models whose predictions can be characterized by sound rules [36, 42].
When it comes GNNs, Tena Cucala et al. [35, 37] provide sound Datalog rules and equivalent programs for GNNs with non-negative weights and max or sum aggregation, respectively. Morris al. [25] consider GNNs with sum aggregation and show that, in practice, they often provably have no sound Datalog rules. There is also a plethora of related work considering the logical expressivity of general aggregate-combine GNNs. Barceló al. [7] show that if a GNN captures rule, then it can be expressed in the logic ALCQ, Other works provide GNN expressivity results for various extensions of first-order logic, including linear programming [26], Presburger quantifiers [8], and counting terms [14]. Ahvonen et al. [3], Pilueger et al. [27] characterise recurrent GNNs using fixpoint operators. Cuenca Grau al. [10] consider GNNs with bounded aggregation functions and show their equivalence to fragments of first-order logic.
Although any function mapping multisets of real numbers real numbers be used for the aggregation function in a GNN, standard options include mean, sum, max, and attention [40]. In practice, mean aggregation often emerges as the default choice [16, 19, 30, 32, 44] due to its
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

simplicity, stability during training, and good empirical performance. With regard to the expressivity of mean-GNNS: Rosenbluth et al. [30] study mean, sum, and max aggregation terms of their ability to approximate one another. However, to our knowledge, there are no prior works analysing the logical expressivity of or attempting to extract sound rules from GNNs that use mean aggregation (mean-GNNss.
To obtain explanatory sound rules for mean-GNNs, we consider mean-GNNs with non-negative weights (MAGNNs). This isolates the source of the non-monotonicity to the aggregation function (since negative weights can also be a source of non-monotonicitt) enabling simpler analysis. This extends the work of Tena Cucala et al. [37], who proved that GNNs with non-negative weights and max or sum aggregation are monotonic under injective homomorphisms, enabling the verification of sound rules, and of Tena Cucala et al. [35] and Morris et al. [25], who found that restricting GNNs to non-negative weights did not greatly impact performance when using max or sum aggregation, respectively.
Our Contribution
We provide two main theoretical results. First, we prove the exact class of "monotonic rules" that can be sound for MAGNNs, which turns out to be very limited. We also provide means for checking if such rules are sound. Second, in light of the fact that some MAGNNs do not have equivalent first-order logic (FOL) programs, we instead provide a restricted fragment of FOL that contains sound rules that can be used to explain any prediction of MAGNN. In our experiments, we show that mean-GNNs still perform well on benchmark datasets when restricted to having non-negative weights. We also demonstrate that they recover a variety of sound monotonic rules, as well as providing examples of the generated rules that explain predicted facts of the GNN. Despite good model performance on the test set, we find that MAGNNs still learn some nonsensical sound rules, showing the importance of explainability.
2 Background
Datasets and Graphs We fix signature of countably infinite, disjoint sets of unary/binary predi- cates and constants. We also consider countably infinite set of variables disjoint with the sets of predicates and constants. term a variable or a constant, An atom is an expression of the form R(t2, 12) or (f2), where each iù is term and R, U are binary and unary predicates, respectively. An atom is ground if it contains no variables. A fact is a ground atom and a dataset D is a finite set of facts. We denote the set of all constants in D with cDn
For vector and i 0, v[i] denotes the i-th element of (likewise for matrices). For finite set Col of colours and ó E N, (Col, 0)-graph G is tuple (V. (E"EE" A} where V is finite vertex set, each E C V x V a set of directed edges with colour c, and assigns to each v E V a vector of dimension 8. Each vertex en E V is defined to correspond uniquely to constant a from the signature. When is clear from the context, we abbreviate the labelling A(v) as v. We uniquely associate each v(i] with unary predicate U, and each colour in c E Col with binary predicate R There thus a one-to-one correspondence between graphs and datasets [37]. We use Ne(v) to denote the c-coloured neighbours of a vertex Graph G is undirected if E is symmetric for each E Col and is Boolean vii E {0, for each v E V and i E (1,...,)).
We use standard first-order logic (FOL) syntax. including equality. A variable in a FOL formula free if it is not quantified. Barceló et al. [7] define first-order logic (FOL) classifiers over coloured graphs, where for graph G. node v, and FOL. formula 40 with a free variable, (G, v) } yp denotes o being satisfied by node v of G. Similarly, given the correspondence between graphs and datasets, for a dataset D, constant E D, and FOL formula &p with free variable x, we let (D, = ip denote yp being satisfied by constant a of D. More precisely, (D, a) }= yp if for variable substitution mapping + we have D F spu. As usual in this setting, D is treated as an interpretation and D == op iff tp evaluates to true in D.
FOL Rules
We define FOL rule to be of the form B + A(z), where B is FOL formula with free variable and A a unary predicate. A program is a set of rules. Given a dataset and FOL rule r : B - A(x), we define the immediate consequence operator T,(D) (A(a) a E con(D) D), (D, a) }= B). For program a, we likewise define Ta Ureo TD(D). This approach similar to that of Barceló et al. [7], except that instead of binary classification, we essentially doing multi-class classification.

---

It is the same approach of Tena Cucala et al. [37], where they find equivalent programs and sound rules for different GNNs, but use Datalog semanties.
We also consider fragments of FOL. defined by description logics such as ALCQ [6], the concepts of which are defined by:
C:: -ITILIIICCCCNDCLL | 3.. S. P.C 2n P.C.
for any relation (binary predicate) P. ALCQ concepts C, D. and atomic concept (unary predicate) A. We define an ALCQ rule to be subsumption of the form = Immediate consequences are defined in the same way as for FOL, since every ALCQ concept corresponds to FOL formula with one free variable.
Graph Neural Networks A function R - R is monotonically increasing if x < implies (a) S ay). We apply functions to vectors element-wise. (Col.5)- graph neural network M with 2 1 layers is tuple
(Achsses (Boeccolusss {behises, {othiees, faggehsess. cls; )
(I)
where, for each E (l,..., LJ.....] L} and e Col, matrices A; and B are of dimension & x ōx-1 with 5u 82 6, by is vector of dimension 8,, de R R+ U (0) is monotonically increasing continuous activation function with non-negative range, agg is an aggregation function from finite real multisets real values, and cls, R - {0, 13 for threshold i. E R is step classification function such that c1s,(r) = 1 if x 2 I and c = otherwise."
Applying M to a (Col, -ggrrphh induces sequence of labels vo, Vi,..., Vy for each vertex in the graph as follows. First, vo is the initial labelling of the input graph; then, for each < S L, Vy is defined by the following expression:
or + A
Σ
agg.(g(uuu (v, u) E E"))
(2)
cECul
The output of M is (graph with the same vertices and edges as the input graph, but where each vertex is labelled by cls,(Vz).
When each agg; is mean, we call it a mean-GNN (likewise for max and sum). When all values in each Ae and B; are non-negative, we say that the GNN is monotonic. In this paper, we consider in particular the class of monotonic mean GNNs (MAGNNs). Besides the restriction of non-negant negaaive weights, this is the same model used in R-GCN [32] (where the normalisation constant is set as described in their paper, to be the number of e-coloured neighbours of the node).
Dataset Transformations Through GNNs A GNN M induces a transformation TM from datasets to datasets over given finite signature [37]. To this end, the input dataset must be first encoded into a graph that can be directly processed by the GNN, and the graph resulting from the GNN application must be subsequently decoded back into an output dataset. We adopt the so-called canonical scheme, where enc(D) of a dataset and a c-coloured edge (u", nh for each fact (a, b) D. Furthermore, given a vertex v", vector component va [p) is set to if and only if (a( E D, for (I,..., .8). The decoder dec is the inverse of the encoder. The canonical dataset transformation induced by GNN M then defined as: (D) dec(MM(en((D))). We abbreviate M(enc(D)) (D) by M(D).
the Boolean (Col, 5ggrpph with a vertex o for each constant a in D
In this paper, we will only consider (Col, 8)- graphs, datasets, and GNNs, unless specified otherwise. When performing the task of link prediction, we use the additional dataset transformations of Tena Cucala al. [37], which enable GNNs to predict binary facts.
Soundness and Subsumption A FOL (or ALCQ) logic program or rule a is sound for a MAGNN M if T. (D) C (D) for each dataset D. Conversely, a is complete for M (D) C (D) for each dataset D. We say that a is equivalent to M if it is both sound and complete for M. Finally, we say that rule or program R subsumes a rule if for any dataset D, (D) S (D)..
Note that if > is used for the classifier instead of 2, one obtains an entirely different set of theoretical results from the ones in this paper.
3

---

3 Sound Rules and Explanations
We prove a series of theoretical results for MAGNNs, to identify which monotonic rules can be sound for them and obtain sound explanatory rules. The restriction non-negative weights isolates the source of the non non-monotonicity to the aggregation function, making analysis easier; however, MAGNNs still possess the defining feature of mean- mean-GNNs in their choice of aggregation function. This restriction is the same approach that was used effectively for GNNs with sum or max aggregation [25, 35, 37J. First, show that there exist MAGNNs with no equivalent FOL programs. Intuitively, this follows from FOL's inability to express numerical comparisons.
Proposition 1. There exists a MAGNN M such that for any dataset D and constant a E con D), (a) E (D) if and only at least half of the neighbours b of a in D are such that (b) D, where U is a unary predicate. This logical function cannot be defined in FOL [21].
full proof given in Appendix A. This means that the task of trying to find equivalent programs for them, such the approach of Tena Cucala et al. [37], is impossible. Instead, we aim extract sound rules from MAGNNs, to explain their predictions. Thus, we consider in particular a class of "monotonic" rules encompassing many common inference patterns, and identify the restricted fragment that can be sound for MAGNNs. Finally, we define a rule language using a fragment of FOL that, for any mean- BeeanGGNN prediction, contains sound rule that entails the prediction.
3.1 Which Monotonic Rules can be Sound for MAGNNS
Since equivalent programs cannot be found in some cases, we instead first show which simple monotonic rules can be sound for MAGNNs. Monotonic rules appear commonly practice [1, 23, 34], are often easily human-readable, and are easier to use for extracting sound rules.
Definition 2. A rule is monotonic (under datasel extension) if for all datasets D, D' such that D D' (D) C (DD)
Description logics, such ALCC [6], are natural choice for providing language for sound rules due to their widespread use in data modelling and their theoretical relationship to GNNs [7]. However, some ALCQ concepts are inherently non-monotonic: for example, if (D,c) } VP.A for some atomic concept A, binary predicate P. dataset D, and constant c E con D), then for D' = D u (P(c, d)} with fresh constant d, (D', c) + VP.A(c).
EL [6] is a more restricted description logic than ALCQ, where concepts use only intersection and existential quantification any EL rule is thus monotonic. We define ELUQ, language in be-between EL. and ALCQ, as the language containing concepts defined by
C := T T|ATCIIICCDII 3P.C| 2, P.C.
where C, D are ELUQ concepts. P is binary predicate, AA is atomic concept, and n positive integer. Note that any concept 3..CC can be written equivalently as 21 P.C. An ELUQ rule has the form C E A. This language is similar (but not equivalent) to that of Datalog with inequalities considered by Tena Cucala et al. [37] for GNNs with sum aggregation and non-negative weights, given constraints the inequalities and the addition of disjunction. All ELUQ rules monotonie; however, it remains an open question as to whether this is a maximal monotonic fragment of ALCQ.
We find that for any ELUQ rule r that is sound for MAGNN M, there exists set of rules of very simple form that (1) are each sound for M and (2) collectively subsume r. This is formalised the following theorem.
Theorem 3. Let M be a MAGNN and an ELUQ rule that is sound for M. Then there exists finite set of rules R such that:
1. Each r' R has the form 3P.T n... T. ... n As n T As+1, where each Pş is binary predicate, A, a umary predicate, and j, k E No-
2. Each r' E R is sound for M.
3. R. subsumes

---

The proof provides a construction of R. For example, given an ELUQ rule :: L. n 3/2 (EP .3) L A = As be sound for M, we can construct rules r1 T.. As and 22 A4 E As such that both r1 and 122 are sound for M and (ri,r2) subsumes r.
As consequence of this, when checking for sound ELUQ rules it suffices check for rules of the above restricted form. In addition, whilst the space of all ELUQ rules is infinite, the restricted fragment we provide is finite, meaning that all sound ELUQ rules can be covered by instead iterating over a finite number of restricted rules. Finally, this raises concerns for the logical expressivity of MAGNNs, since any sound ELUQ rule is ultimately subsumed by a set of much simpler sound rules.
Proof sketch. The full proof of Theorem is given in Appendix A.2. A different r' is defined for each concept in the outer disjunction of the body of r. To see the crucial step of the proof, consider some rule without disjunction in the outer concept, and let 71 == r. Then 71 is of the form Zn P.C. 7 C2 E A, where P is a binary predicate, C1 an ELUQ concept, C2 an ELUQ concept without disjunction, and n positive integer. We inductively define sequence r2 .... of ELUQ rules that such for all i E f1...., k 1}. F:41 is sound for M and ri+1 subsumes r,. Given r; of the form 2n P.C. n C2 E A, we define r as the rule 3P.T C2 E A. Trivially, T:+1 subsumes r;.
Now consider the following datasets Dj and Dm (parametrised by N). In D1, a concept C2 annotating a constant a denotes that there exists other facts in the dataset such that (D1,a) = C2 (similarly for D..)
b1
a
C1
C1
P
Dataset Dj:
C2
P
Dataset Dm
P
C
P
P
P
Ci
bm
Cn
Ci
Note that D1 is instantiation of the body of T++1- The soundness of T,+1 depends on the fact that as m + co, the computation of M on Dm at constant a tends to that of M on D₃ (and that A(a) E (P..))
Since T1 contains a finite number of or 2n operators and each T++1 has one fewer 3 or 2n operator than ri, this inductive construction is guaranteed to terminate for some k. We include ти in R. Once this has been done for every r E R', we have A subsumes r.
Checking for Monotonic Rule Soundness remains to be shown how one can verify the soundness of ELUQ rules. Since we only need to consider rules of the form given in Theorem 3, there are exactly 8 261||ool possible rules to check. For rules 1 72, when considering the sets of body concepts B,, and Br,, if B,, S Br, and F1 is sound, then is sound: we use this to optimise the procedure. The following proposition allows one to check the soundness of ELUQ rules.
Proposition 4. Let M be MAGNN and r: EP,T n ... n 3P T n A n ... 7 Ag 5 ARt1 be a rule of the form given in Theorem Define Drase == (Ai (a), (a(a), ()., b)3 for constants + b. Then is sound for M if and only (s) TM((Daa)
For example, to check if rule r 3... r 2P M A₁ 7 A2 = Ag is sound, suffices compute the output of M on the following dataset Druse = (A)(a), A2(a), Pi (a b), Pz b)), which can be represented as follows:
P2
b
A1
P
Then r is sound for M if and only if As(a) E (M(sees)), Note that this method also works the body of the rule is empty, by simply checking if (s+1(a) E (D)) where Dg [P(b, a)}.
Proof sketch. The full proof of Proposition is given in Appendix A.3. relies on the fact that (Donse, a) }= B. where B is the body of Furthermore, no extension to Doase will decrease the output
5

---

at em and any dataset satisfying B is an extension of Drsse (up to constant relabelling, un un-merging the neighbours of v", and letting a). Note that none of these merges un-merges will decrease the output at o and that MAGNNs are agnostic to the particular constants used in the input dataset. IT
Consequences for Link Prediction To perform link prediction, we combine the canonical transfor- mation with the dataset encoding-decoding scheme defined by Tena Cucala et al. [37], which has found wide use [22, 25, 35, 37, 43]; it introduces additional nodes in the graph to represent pairs of constants. Node labels then encode binary facts, instead of unary. Graph edges are used only to connect nodes that have constants in common; and so the presence of an edge is independent of whether any specific fact holds in the dataset.
The encoding and decoding can be described by a set of rules [37, Section 3.2], each expressed in a simple extension of Datalog. Given a sound rule for the canonical transformation, we can combine (via unfolding) with the rules representing the encoder and decoder to obtain a Datalog rule that is sound for the entire link prediction transformation. This observation, combined with Theorem 3, ensures that each monotonic rule sound for the entire link prediction transformation is subsumed by rules of the form Rí (2., y) A... Rm- (2;, y) - Rm v), where R1, ..., Rm,. are binary predicates from the signature. This is obtained by unfolding a rule of the form given in Theorem 3, since the unary predicates A, are unfolded into the binary predicates they represent, and the existentials 3PJ.T T can safely be removed since the edge presence is independent of any specific fact.
3.2 Explaining MAGNN Predictions
In this section, we provide a family of rules Q (a fragment of FOL) to explain any prediction of a MAGNN. More precisely, for any MAGNN M, dataset D, and predicted fact A(a) E (D). there exists rule E Ω such that A(a) (T(D) and is sound for M. To achieve this, we define a procedure to derive the rule E S2 given M, D, and A(a).
Logic Language Needed We first define the family of rules using ALCQ syntax, with the addition of a new operator, rather than defining it directly in FOL. The operator is 3n ("exists n unique"): for example: 3, (A,, A2, T). Its semantics are defined as follows. For concepts Ci...., Cn. binary predicate P. dataset D, and constant e E D, we define (D,c) F P.(I,, ........ if and only there exist distinct constants CI,,,,, Cn E con(D) such that (D,c) - C (D,ca) F C. and P(c, P(c, G.) E D. Written in first-order logic, it is defined as (D,e) = 3, P.(C. .n. =
(D,c) Fan,.. + 2, for all i,j e f1,..., n) such that < f) A A A A (x,) A P(z,z1) A ... A P(x,,x))
for free variable x. We then define the family of rules Ω as follows. An Ω-concept C' is defined by C : T | A C n C2 P,,., C,) Im P.T, where is any atomic concept, n any positive integer, m an integer, CI,..., On any ft-concepts, and P any binary predicate. A rule in Ω has the form C E A, where C' is any ft-concept and A any atomic concept.
Let M be MAGNN, D dataset, and A(a) (D) a prediction of the MAGNN. We define rule r E S by C2, E A, where the only part of M that the rule depends on is L, which is what guarantees that the rule will be finite. The body concept C2 is defined as follows:
Explanatory Rule
Definition 5. For dataset D, e E con(D), E. E No. we inductively define a concept Cj by C7 := T r A n ... 7 Ag, where AI,...,y are all atomic concepts A₁ such that A²(c) E D. Then, if O, we are done: C2 has been defined.
Otherwise, for each binary predicate P, let Ci, Cn be all the constants &; E con(D) such that P(c, c.) E D. Then, i > 0, extend Cū as follows: Cj := C2 n 3 P.P. C32,) Sn P.T. C is extended for each binary predicate P. Note that each Cop is defined inductively.
The following theorem then shows that the rule both explains the prediction (by producing the same fact on the dataset as the MAGNN) and is sound for the MAGNN.
Theorem 6. For any MAGNN M, dataset Das and fact A(a) E (Da)),, the rule r CC 5 (dependent on D.)) is sound for M, and A(a) E (D.).

---

Consider a dataset Du - (A, 2-1ayer GNN M. for example, such that Ag(a) (D). Then, using Theorem we construct the rule:: C2 [ A3. where 02 is T n A 1....TT.Te A2 ())()))))) S Pz. T) Sa P..T.
P2 c), Ps(c, d)} and b2). P2 a), A2
Notice that (Da: a) F= C2. so we have Az(a) E (D). Furthermore, As(a) E (D) is sufficient witness for the soundness of r, as we will prove below.
Proof sketch. The full proof of Theorem 6 is given in Appendix A.5.
(Da: a) += C?2 follows from the inductive construction of Ci, from which we obtain A(a) E (D.). It remains to be shown that is sound for M. Let Dj be dataset: to show soundness, we prove that T,(D,) C (D)) so let A(b) E (D()))
First, we define dataset D2 to be the L-hop neighbourhood of the constant a in D. (analogously to how L-hop neighbourhoods are defined for nodes graphs). Then we show that A(a) E TM (DE). since A(a) E TM Da) this follows from the definition of DL as the I.-hop neighbourhood. Finally, we prove A(b) E (Ds)),, since A(a) E (D)) - this follows from the fact that any differences between D2 and Dj, cannot yield a lower MAGNN output for dd in comparison to un plus mapping between constants of Dj and D2.
4 Experiments
We train GNNs across several benchmark link prediction datasets and node classification dataset, showing that sound rules and explanations can be found for MAGNNS in practice, and that the restriction to monotonicity does not significantly decrease performance. For the model architecture, we fix hidden dimension of twice the input dimension, GNN layers, ReL.U after the first layer, and sigmoid after the second layer. The GNN definition given in Section 2, which was chosen for ease of presentation, describes GNNs aggregating in the reverse direction of the edges. For our experiments, we follow the standard approach and aggregate in the direction of the edges. Thus, when presenting rule, we write each binary predicate as its inverse. For example, "advisor" is written as "advisorOf".
We use GNNs with max, sum, and mean aggregation. We train each model for 8000 epochs, stopping training early if loss does not improve for 50 epochs. For all trained models, we compute standard classification metrics, such precision, recall, accuracy, and F1 score. For each model, we choose the classification threshold by computing the accuracy on the validation set across a range of 108 thresholds between 0 and 1, selecting the one which maximises accuracy. We train all our models using binary cross entropy loss and the Adam optimiser with a learning rate of 0.001. We train models without restrictions as baselines (denoted by "Standard"), as well as restricting the models to having non-negative weights (denoted by "Non-Neg") by clamping negative weights to 0 after each optimiser step, as in the approaches of Morris et al. [25], Tena Cucala et al. [35]. We each experiment across 5 different random seeds and present the aggregated metrics. To compute 95% confidence intervals, we assume a normal distribution and compute the interval as 1.97 x SEM (standard error of the mean). Experiments were run using PyTorch Geometric, with 2 CPUs and 16GB of memory on a Linux server, using 34 days of compute time.
Datasets We use 3 standard benchmarks: WN18RRv1, FB237v1, and NELLv1 [38), each of which provides datasets for training, validation, and testing, as well as negative examples and positive targets. Importantly, these benchmarks are also inductive, meaning that the validation and testing sets contain constants not seen during training. We also use the LUBM dataset [15, LUBM(1 (1,0)), with the train/test split from Liu et al. [23]: this is node classification dataset, all others are link prediction.
Finally, we utilise LogInfer [23], a framework which augments a dataset by considering Datalog rules conforming to a particular pattern and adding the consequences of the rules to the dataset. We use the datasets Doglnfe--NN-hie (WN-hier) and LogInfer-WN:
(WN-sym) [23], which are enriched with the hierarchy and symmetry patterns, respectively. We also use LogInfer-WNe WN-hier WN-hier_nmhier [25]. which was created using a mixture of monotonic and non- monotonic rules: rules from the "hierarchy" and "non- monotonic hierarchy" (R(x, y) A AS(y, 2) + T(x, v)) patterns, in this case. We use the dataset to test whether monotonic rules can recovered from the dataset, despite the presence of non-monotonic rules. For the LogInfer datasets, during each training epoch, 10% of the input facts are randomly set aside and used as ground truth positive targets, whilst the rest of the facts are used as input to the model.
7

---

Dataset
Agg
Weights
%Acc
%Prec
%Rec
F1
LUBM
Mean
Standard Non-Neg
97.1 = 0.0
96.9 +.0 0.0
97.2 07.2.0.00
0.0
91.5 = 0.0
87.8
96.4
9.0
WN-hier
Mean
Standard
99.5 = 0.0
9.0
9.0
9.0
Non-Neg
99.8 + 0.0
99.7
9.0
99.8 0.0
WN-sym
Mean
Standard
99.4 = 0.0
99.5
99.3
99.4 0.0
Non-Neg
100 + 0.0
100 +.0
100 1 0.0
100 0.0
WN-hier_amhicr
Mean
Standard
86.2 + 0.0
84.7 0.0
88.4 0.0
86.5 0.0
Non-Neg
71.6 + 0.0
80.1
58.8 1 0.1
67.2 + 0.0
FB237v1
Mean
Standard
68.7 + 0.0
95.4 0.0
39.3
55.7 + 0.0
Non-Neg
71.8 + 0.0
+
(4.8
69.7 + 0.0
WN18RRv1
Mean
Standard
93.7 + 0.0
98.5 9
88.
93.4 0.0
Non-Neg
95.5 + 0.0
98.1
92.7
95.3 + 0.0
NELLv1
Mean
Standard
75.2 + 0.1
93.8 0.0
0.2
65.7 + 0.2 93.8 + 0.0
Non-Neg
93.4 = 0.0
88.8
99.4 = 0.0
Table 1: Results for mean- mean-GNNs with standard / non-negative weights, across all datasets. Metrics are computed on the test set and shown with a 95% CI.
Datasct
Tot
Un
Bin
Mix
3
4
7
8
LUBM
11.6
1.4
9.8
0.4
9.6
1.4
0.6
0
WN-hier
22.6
15.6
7
2.6
5.4
6.6
1.4
3.8
2.2
0.4
0.2
WN-sym
0.4
0.4
0
0.4
0
0
WN-hier WN-hier_nmhier nmhiir
53.6
4.6
49
1.8
16.2
17.8
12.6
4.8
0
0.4
FB237v1
136
136
0
29
136
WNISRRv1
0
0
0
0
0
0
NELLvI
Table 2: Counts of monotonic rules of the form given in Theorem 3. Tot, Un, Bin, Mix are the counts of the total number of rules, rules with only umary atoms, rules with only binary atoms, and rules with a mix of atom aritics. Each remaining column counts the number of rules with body concepts.
Rule Extraction and Explanations On all datasets, we use Proposition 4 to check for monotonic rules of the form given in Theorem 3. This procedure described in Algorithm 1 of Appendix B. Given the differing number of unary and binary predicates in each dataset and the exponential growth of the rule space, we check all rules up to differing number a body concepts: for LUBM, all 15 for WN-based-datasets, 1 for FB237v1. 1, and for NELLv1. This yields total possible number of sound rules: 383670 for LUBM, all 360448 for WN18RRv1 and the LogInfer datasets, 56169 for FB237v1, and 216600 for NELLv1. When rule is subsumed by another with fewer body atoms, is not counted.
We also compute sound explanatory rules of the form given in Theorem for all true positive predictions made on the test set of LUBM. Given that explanatory rules are often large, we improve the process by first checking if sound rule of the form given in Theorem 3 derives the fact on the input dataset, and return the rule as an explanation it does. no such rule exists, we use rules from Theorem 6. Other strategies for improving the rule quality are discussed in Appendix B.2.
is shown in Table For completeness, results across all aggregation functions are given in Tables 5 to 7 of Appendix C. We see similar behaviour for mean- Gaaas as for sum and max-GNNe when they are restricted to non-negan non-negative weights, which matches the behaviour seen by Morris et al. [25] for sum-GNNs and Tena Cucala et al. [35] for max- GNNs. On LUBM, the restriction yields small decrease in performance. For monotonic LogInfer datasets, there is slight increase in performance, and for the non-monotonic one, substantial decrease, since the dataset explicitly penalises monotonic model behaviour. Finally, on the benchmark datasets, the restriction improves performance, sometimes substantially. This demonstrates that the
Results Mean-GNN performance on the

---

Dataset
Examples of Sound Rules
LUBM
_ Publication
JadvisorOf.T AssociateePoffesoor
Department Uuw.degrruuuteSuuuuuuattnaaaasaa
FullProfessor
WN-hier
_eember_o__doomminn_aaaee +__member__erroomm(XX
WN-sym
hass_ _hs__par(XX, Y) deerivationallyyreaatedddoooo _iimilrr_toXX,7
A
WN-hier_anhier
hyperrpwml...y/A.Syysssss..oooor Y) - _also__seee_ Y)
FB237v1
T + /
hhaerbbbiiieees/hhhsssooottaannn /imm//i/////// Y)
NELLv1
organizationeemminacddpessolll X, http://eennnoooooooooooomeeeerre totopmmmemerooofogaaiiiiiiioiii Xx Y)
ogganizationhhirddprrooo//
Table 3: Randomly sampled sound monotonic rules of the form given in Theorem
Fact Rule
T C Publication
Fact Rule
GraduateStudent ResearchAssistant
Fact Rule R Grranattteett
Fact Rule ResearchAsssitann 77 IaathoooPPuuiioiiiiinnonnn L C GraduateeStudent
Fact Rule Tacurse/TakenBy... JhasTeacher. C Course
Fact Rule
FadvisorOf. Assissannsssssstttrrrrssssoor
Fact Rule
AgrnatedUnddggradatttDDooorr T E University
Table
Randomly sampled explanatory rules that have successfully been reduced in size, shown
with the corresponding facts produced by the MAGNN on LUBM.
restriction mean-Grn GNNs to MAGNNs can be done in practice without sacrificing significant model performance, while enabling the extraction of sound rules. We hypothesize that the occasional performance increase seen when restricting the models to non-negative weights is due to (1) regularizing the model and (2) the dataset patterns not requiring negative weights to be captured.
In Table 2. we present counts of the number of sound monotonic rules that were obtained on each dataset. On LUBM, WN-hier, WN-hier_nmhin with a varying number of body concepts. On average, we found 2 sound rules on LUBM that have empty bodies, and 29 on FB237v1; these rules are clearly absurd, but are what the GNN has learned, highlighting the need for sound rules so that such issues in the models can be exposed. Further to this, note that almost sound monotonic rules were obtained on WN-sym, WN18RRy1, or NELLvI. This is especially concerning for WN-sym, which was populated with the consequences of monotonic rules. This behaviour is due to the very restricted form that sound monotonic rules can have when used with the link prediction encoding of Tena Cucala et al. [37], as discussed in Section 3.1. Morris et al. [25], the other hand, found that all of the rules used to create WN-sym were sound when using -Nus with non neg-negative weights. We show some sample sound monotonic rules in Table 3, with more given in Table 8 of Appendix C.
and FB237v1, we find a number of sound rules
In Table 9 of Appendix C, we give samples of explanatory rules of the form given Theorem On LUBM, these explanatory rules had 25 body concepts average. When using the improved

---

procedure of first checking for explanatory rules of the form given in Theorem 3, the rules averaged only 11 body concepts. On average, out of 1990 true positive predictions, the process only failed 22 times to explain the predicted fact using a rule from Theorem 3. In Table 4, we give samples of such explanatory rules, which are useful for providing insights into the data, as well as exposing issues with the trained MAGNN. For example, the explanatory rule E Publication exposes a nonsensical rule learned by the MAGNN, which arises as a consequence of publications in LUBM having no incoming edges. Likewise, it is sensible that the MAGNN has learned that research assistants are graduate students, but it has also erroneously learned that all graduate students are research assistants. Finally, note that the fourth rule in the table is subsumed by the third rule this is because they come from two different MAGNNs, which have learned different sound rules. Table 10 of Appendix C provides a longer list of explanatory rules that have been reduced in size.
5 Discussion
Our Contribution We considered mean-GNNs with non-negative weights (MAGNNs), showing first that they can express logical functions that go beyond FOL. We proved which ELUQ rules (a class of monotonic ALCQ rules) can be sound for MAGNNs, which turned out to be very limited. The resulting rule space is finite, which enabled us to define a procedure to check for all sound ELUQ rules, We also provided a restricted fragment of FOL, from which sound rules can be constructed to explain any prediction of MAGNN. In our experiments, we found that mean- GNass still perform well on benchmark datasets when restricted to having non-negative weights. We also found a variety of sound monotonic rules on half the datasets, with provably almost no sound monotonic rules on the other half. This, alongside several nonsensical sound rules, raise questions about how mean- GNNs can be encouraged to recover the underlying rules the datasets, and suggests that max- or sum-GNNs may be preferable when provable soundness is required. It also shows the importance of rule extraction techniques, given the good empirical performance of MAGNNs on the test datasets but nonsensical rules they have learned (for example, that everything is publication). Finally, we computed explanatory rules for predictions made by MAGNNs on the LUBM dataset.
Logical Explanations for GNNs Other works also extract logical explanations for GNN predictions [4, 5, 20, 28]. However, none of these provide theoretical guarantees that the explanations are sound for the model, only empirical evidence that they approximately faithful. Pluska al. [28], for example, learn decision trees from GNNs and then extract logical rules from the decision trees they are not equivalent to the GNNs they are derived from, the extracted logical rules are not provably sound. Furthermore, Köhler and Heindorf [20] only consider explanations in EL., which is a fragment of ELUQ.
Mean-GNN Theory Further works also provide theoretical analyses of GNNs with mean aggre- gation. Vasileiou et al. [39] provide generalisation bound for mean-GNNs. Adam-Day al. [2] show that mean-GNNs used for graph classification tend to a constant function as the sizes of the input graphs tend infinity (under certain random graph models). Their approach of tending the size to infinity is similar to our technique used in the proof of Theorem 3. In contemporancous work, Schönherr and Lutz [33] identify the FOL expressivity of GNNNs in the uniform (standard) and non-uniform (only on graphs up to a bounded number of nodes) settings. In the uniform setting, they prove that any continuous mean- GNN (that equivalent to FOL classifier) has an equivalent logical classifier expressible in alternation- -ffeee modal logic (AFML). However, they do not provide a construction of the AFML classifier, a demonstration that such construction would be obtainable in practice, or means to recover sound rules if the mean- mean-GNN is not equivalent to FOL classifier.
Limitations Our work is limited in several ways. First, despite being able to check the infinite space of ELUQ rules for soundness by instead checking finitely many rules of the form given in Theorem 3, the size of this finite space grows exponentially in the number of predicates, making the search intractable as the number of predicates increases (as seen on FB237v1, for example). Also, it is an open question as to whether ELUQ is a maximal monotonic fragment of ALCQ, so there may be other monotonic rules that can be sound for mean-GNNs. Finally, we only consider the S operator for the mean-GNN step classification function cls, due its standard use in prior work [25, 35, 37] and the fact that using < yields entirely diffeerntt set of thcoretical results (for example, rules with a body of 3.AA could be sound for such a mean- GNN, without 3P.T being sound).
10

---

Acknowledgments and Disclosure of Funding
Matthew Morris funded by an EPSRC scholarship (CS2122 EPSRC_ 1339049). This work was also supported by Samsung Research UK, the EPSRC projects UKFIRES (EP/S019111/1) and ConCur (EP/V050869/1) The authors would like to acknowledge the use of the University of Oxford Advanced Research Computing (ARC) facility in carrying out this work: http://ds doi org/10. 5281/zenodo. 22558.
For the purpose of Open Access, the authors have applied CC BY public copyright licence to any Author Accepted Manuscript (AAM) version arising from this submission.
References
[1] Ralph Abboud, Ismail Ceylan, Thomas Lukasiewicz, and Tommaso Salvatori. Boxe: box embedding model for knowledge base completion. Advances in Neural Information Processing Systems, 33:9649-9661, 2020.
[2] Sam Adam-Day, Michael Benedikt, Ismail Ceylan, and Ben Finkelshtein. Almost surely asymptotically constant graph neural networks. Advances Neural Information Processing Systems, 37:1 37:124843--1 144488668486,, 2024.
[3] Veeti Ahvonen, Damian Heiman, Antti Kuusisto, and Carsten Lutz. Logical characterizations of recurrent graph neural networks with reals and floats. arXiv preprint urXiv:2405, /4606, 2024.
[4] Burouj Armgaan, Manthan Dalmia, Sourav Medya, and Sayan Ranu. Graphtrail: Translating gnn predictions into human- bumaan-nterppettable logical rules. Advances in Neural Information Processing Systems, 37:123443-123470 2024.
[5] Steve Azzolin, Antonio Longa, Pietro Barbiero, Pietro Liò, and Andrea Passerini. Global explainability of gnns via logic combination of learned concepts. In The First Learning Graphs Conference-LoG 2022, 2022.
[6] Franz Baader. The description logic handbook: Theory, implementation and applications. Cambridge university press, 2003.
[7] Pablo Barceló, Egor V Kostylev, Mikael Monet, Jorge Pérez, Juan Reutter, and Hab-- Silva. The logical expressiveness of graph neural networks. 8th International Conference on Learning Representations (ICLR 2020), 2020.
[8] Michael Benedikt, Chia-Hsuan Lu, and Tony Tan. Decidability of graph neural networks via logical characterizations, arXiv preprint arXiv:2404. 18151, 2024.
[9] Milad Besharatifard and Fatemeh Vafaee. review on graph neural networks for predicting synergistic drug combinations. Artificial Intelligence Review, 57(3):49, 2024.
[10] Bernardo Cuenca Grau, Eva Feng, and Przemystaw A Walega. The correspondence be- tween bounded graph neural networks and fragments of first-order logic. arXiv preprint arXiv:2505.0802.. 2025.
[11] Chen Gao, Xiang Wang, Xiangnan He, and Yong Li. Graph neural networks for recommender system. In Proceedings of the fifteenth ACM international conference web search and data mining, pages 1623-1625, 2022.
[12] Marta Garnelo and Murray Shanahan. Reconciling deep learning with symbolic artificial intelligence: representing objects and relations. Current Opinion in Behavioral Sciences, 29: 17-23, 2019.
[13] Justin Gilmer, Samuel S Schoenholz, Patrick Riley, Oriol Vinyals, and George E Dahl. Neural message passing for quantum chemistry. In International conference machine learning. pages 1263-1272 PMLR, 2017.
[14] Martin Grohe. The descriptive complexity of graph neural networks. TheoretiCS, 3, 2024.

---

[15] Yuanbo Guo, Zhengxiang Pan, and Jeff Heflin. Lubm: A benchmark for owl knowledge base systems. Journal of Web Semantics, 3(2-3):158-182 2005.
[16] Will Hamilton, Zhitao Ying, and Jure Leskovec. Inductive representation learning on large graphs. Advances in neural information processing systems, 30, 2017.
[17] Aidan Hogan, Eva Blomqvist, Michael Cochez, Claudia d' Amato, Gerard de Melo, Claudio Gutierrez, Sabrina Kirrane, José Emilio Labra Gayo, Roberto Navigli, Sebastian Neumaier, Axel-Cyrille Ngonga Ngomo, Axel Polleres, Sabbir M. Rashid, Anisa Rula, Lukas Schmelzeisen, Juan F. Sequeda, Steffen Staab, and Antoine Zimmermann. Knowledge graphs. ACM Comput. Surv. 54(4):71:1 2022. doi: 10. 10.1145/344777..
[18] Vassilis N loannidis, Antonio G Marques, and Georgios Giannakis. A recurrent graph neural network for multi-relational data. In ICASSP 2019-2019 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pages 8157-8161. IEEE, 2019.
[19] Thomas N Kipf and Max Welling. Semi-supervised classification with graph convolutional networks. International Conference on Learning Representations, 2017.
[20] Dominik Köhler and Stefan Heindorf. Utilizing description logics for global explanations of heterogeneous graph neural networks. arXiv preprint arXiv:2405. 12..:24455.26.4., 2024.
[21] Leonid Libkin. Elements of finite model theory, volume 41. Springer, 2004.
[22] Shuwen Liu, Bernardo Grau, Ian Horrocks, and Egor Kostylev. Indigo: Gnn-based inductive knowledge graph complction using pair-wise encoding. Advances in Neural Information Processing Systems, 34:2034-2044 2045, 2021.
[23] Shuwen Liu, Bernardo Cuenca Grau, Ian Horrocks, and Egor V Kostylev. Revisiting inferential benchmarks for knowledge graph completion. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, pages 461 461-471, 2023.
[24] Christian Meilicke, Manuel Fink, Yanjie Wang. Daniel Ruffinelli, Rainer Gemulla, and Heiner Stuckenschmidt. Fine-grained evaluation of rule-and embedding- based systems for knowledge graph completion. In The Semantic Web-ISWC 2018: 17th International Semantic Web Conference, Monterey, CA, USA, October 8-12, 2018, Proceedings. Part 17, pages 3-20. Springer, 2018
[25] Matthew Morris, David Tena Cucala, Bernardo Cuenca Grau, and Ian Horrocks. Relational graph convolutional networks do not learn sound rules. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 21, pages 897-908, 2024.
[26] Pierre Nunn, Marco Sälzer, François Schwarzentruber, and Nicolas Troquard. A logic for reasoning about aggregate-combine graph neural networks. Proceedings of the Thirly-Third International Join! Conference Artificial Intelligence, pages 3532-3540, 2024.
[27] Maximilian Pflueger, David Tena Cucala, and Egor V Kostylev. Recurrent graph neural networks and their connections to bisimulation and logic. In Proceedings of the AAAI Conference Artificial Intelligence, volume 38, pages 14608-14616. 2024.
[28] Alexander Pluska, Pascal Welke, Thomas Gärtner, and Sagar Malhotra. Logical distillation of graph neural networks. In Proceedings of the 2/ International Conference on Principles of Knowledge Representation and Reasoning, pages 920-930, 2024.
[29] Meng Qu, Junkun Chen, Louis-Pascal Xhonneux, Yoshua Bengio, and Jian Tang. Ranlogic: Learning logic rules for reasoning on knowledge graphs. In International Conference Learning Representations, 2020.
[30] Eran Rosenbluth, Jan Toenshoff, and Martin Grohe Some might say all you need is sum. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intellignnce pages 4172-4179, 2023.
12

---

[31] Ali Sadeghian, Mohammadreza Armandpour, Patrick Ding, and Daisy Zhe Wang. Drum: End-to-end differentiable rule mining on knowledge graphs. Advances in Neural Information Processing Systems, 32, 2019.
[32] Michael Schlichtkrull, Thomas N Kipf, Peter Bloem, Rianne Van Den Berg, Ivan Titov, and Max Welling. Modeling relational data with graph convolutional networks. In The semantic web: 15th international conference, ESWC 2018, Heraklion, Crete, Greece, June 3-7, 2018, proceedings 15, pages 593-607. Springer, 2018.
[33] Moritz Schönherr and Carsten Lutz. Logical characterizations of gnns with mean aggregation. arXiv preprini 1rXiv:2507.18145, 2025.
[34] Zhiqing Sun, Zhi-Hong Deng, Jia Nie, and Jian Tang. Rotate: Knowledge graph em- bedding by relational rotation in complex space. In International Conference on Learning Representations, 2018.
[35] David Tena Cucala, Bernardo Cuenca Grau, Egor V Kostylev, and Boris Motik, Explainable gnn- based models over knowledge graphs. In International Conference on Learning Representations, 2021.
[36] David Tena Cucala, Bernardo Cuenca Grau, and Boris Motik. Faithful approaches to rule learn- ing. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, pages 484-493 2022.
[37] David Tena Cucala, Bernardo Cuenca Grau, Boris Motik, and Egor V Kostylev. On the corre- spondence between monotonic max-sum gnns and datalog. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, pages 658-667, 2023.
[38] Komal Teru, Etienne Denis, and Will Hamilton. Inductive relation prediction by subgraph reasoning. In International Conference on Machine Learning, pages 9448-9457, PMLR, 2020.
[39] Antonis Vasileiou, Ben Finkelshtein, Floris Geerts, Ron Levie, and Christopher Morris. Cov- ered forest: Fine-grained generalization analysis of graph neural networks. In Forty-second International Conference on Machine Learning. 2025.
[40] Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Lio, and Yoshua Bengio. Graph attention networks. nternational Conference on Learning Representations, 2017.
[41] Hongwei Wang, Fuzheng Zhang, Jialin Wang, Miao Zhao, Wenjie Li, Xing Xie, and Minyi Guo. Ripplenet: Propagating user preferences on the knowledge graph for recommender systems. In Proceedings of the 27th ACM international conference on information and knowledge management, pages
2018
[42] Xiaxia Wang, David Tena Cucala, Bernardo Cuenca Grau, and Ian Horrocks. Faithful rule extraction for differentiable rule learning models. In The Twelfth International Conference Learning Representations, 2023.
[43] Zhe Wang, Suxue Ma, Kewen Wang. and Zhiqiang Zhuang. Rule-guided graph neural networks for explainable knowledge graph reasoning. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 39, pages 12784-1279 2025.
[44] Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S Yu. A comprehensive survey on graph neural networks. IEEE transactions on neural networks and learning systems, 32(1) :-424, 2020.
[45] Bishan Yang and Tom Mitchell. Leveraging knowledge bases in lstms for improving machine reading. In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pupers), pages 1436-1446, 2017.
[46] Fan Yang, Zhilin Yang, and William W Cohen. Differentiable learning of logical rules for knowledge base reasoning. Advances in neural information processing systems, 30, 2017.
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The claims made in the abstract and introduction match the theoretical results given in Section and experimental results Section 4.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
Limitations are given in Section
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
14

---

Assumptions are given in the definitions in Section and within each theoretical results presented in Section Full proofs are given in Appendix A, with proof sketches in Section 3.
Justification:
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proof's provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless whether the code and data are provided or not)?
Answer: [Yes]
Justification: All implementation details necessary for reproducing results are given in Section 4, and the rule-checking definitions / constructions given in Section 3 describe our methods for obtaining sound rules.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, a No answer this question will not perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data often one good way to accomplish this, but reproducibilityy can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
specific model and empirical evaluation, may
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way access this model for reproducing the results or way to reproduce the model (e.g., with an open- open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. the case of closed-source models, may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
15

---

5. Open access to data and code
Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Question:
Answer: [Yes]
Justification: Code and data have been submitted with the supplementary material. The README in the code and hyperparameters in Section provide the details necessary for reproducing the experimental results.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nipp cc/
wowooicolllllloooloooooomooiilll for more details.
While we encourage the release of code and data, we understand that this might be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to rum to reproduce the results. See the NeurIPS code and data submission guidelines (https: //n //iips.coo wwtpcc/pppllc.. wttgguudes//CC hete//oooSSubiissee wwssssnolliiooo for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: All important details given in Section 4, with full details in the code.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: We compute and present 95% confidence intervals for of our model performance metrics, described in Section 4.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
16

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful to show in tables or figures symmetric error bars that would yield results that are out of range (c.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of exccution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: As stated in Section 4, we used CPUs and 16GB of memory Linux server, for 34 days of compute time. Each individual run was a maximum of 12 hours. Preliminary and failed experiments used total additional compute time of 28 days.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics https http///eeiippp.eeeee wttp:.cc/pputee hccppublic/ttiicaaaaiiiiei
Answer: [Yes]
Justification: Our work does not have human participants and uses publicly available benchmark datasets for evaluation. We foresee no negative societal impact, our methods only allow for explaining and verifying model predictions, which can only expose bias, not create it. Our work is fully legally compliant.
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- cration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative socictal impacts of the work performed?
Answer: [Yes]
17

---

Justification: In Section 1, we point out the importance of explaining and justifying the predictions of neural models, which the problem that our work aims solve. We foresee no potential negative societal impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to partieular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out, For example, it is legitimate to point that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data or models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: As stated in Section we use only publicly available datasets in our experi- ments.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
The creators of the codebases and datasets we make use of the in the paper are all cited in Section 4. The licenses are as follows: (1) LogInfer [23] source MIT License, (2) non-monotonic LogInfer [25]- - source MIT License, (3) Benchmark Datasets [38]- -
Justification:
source CC BY 4.0, and (4) LUBM [15] source GPL-2.0.
18

---

Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
If assets released, the license, copyright information, and terms of in the package should be provided. For popular datasets, paperswi thcode. com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if has changed) should be provided. If this information is not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
No new assets are given in the paper.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: No crowdsoureing nor human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurIPS Code Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
19

---

Justification:
No crowdsourcing nor human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with
human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality the research, declaration is required.
Answer: [NA]
Justification: LLMs were not used in the paper.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to our LLM policy (https: Sbeerrpp..cc/onteeeeneee////3330 for what should or should not be described.
20

---

A Proofs
A.1 Proposition 1
Proposition. There exists a MAGNN M such that for any dataset D and constant con D), (a) E (D) if and only at least half of the neighbours of a in D are such that U(b) E D. This logical function cannot be defined in FOL [21].
Proof. Consider MAGNN M over signature with only one unary predicate (U) and only one binary predicate (P), corresponding to colour c in the canonical encoding. Let M have L (one layer), with A (0), b (0), and Bi- (1). Finally, let 01 be the identity function and tM = 0.5.
Consider dataset D and constant a in D. Then vi. the labelling of er after M is applied to (Dc, depends only on the number and type of the direct neighbours of v". Each neighbour v² either has U(b) E (b) & D. We end up with
v = Hu (v0, v8) E and v² [1] 1}
[NN(
[(b] P(a, b) E D and U()) D)
H{b P(a, E
Now vg [1] 2 0.5 = LM if and only if [[b P(a, b) E D and (b) E DJI 2 { P(a. E D and (bb) & D).. T.e. ((a) E (D) if and only least half of the neighbours b of in D are such that Ubb E D.
However, this logical function cannot be expressed in FOL. To prove this, consider Libkin [21], who defines the majority predicate MA v) which tests if constants satisfying contains at least half of the constants satisfying th. We find that, for every dataset D and constant E con(D), we have (D, a) -= MAJ(R(aa a, x) A (z). R(a, x)) if and only if "tt least half of the neighbours of in D are such that (b) D if and only if (a) (D).
However, Libkin [21, Corollary 13.17] proves that MAJ queries cannot be defined in an extension of FOL. from which it trivially follows that they cannot be defined in FOL. Thus, M is equivalent to logical function that cannot be defined in FOL.
A.2 Theorem
Theorem. Let M be a MAGNN and an ELUQ rule that is sound for M. Then there exists a finite set of rules R such that:
1. Each r' E R has the form 3P.T ..... each P; is binary predicate, Ai a unary predicate, and j, k E No-
E...TTTTT n. n A₃ n T Ast1, where
2. Each r' R is sound for M.
3. subsumes r.
Proof. First, notice that of the form C² ... C C A for ELUQ concepts C² ...., C containing no disjunction in the outer scope (i.e. disjunction is only nested within existential quantification),
N, and atomic concept A. Note that not containing any disjunctions in the outer scope is covered by m 1.
Now, let R! = {C' C A, C. E A}. By the operation of rule application, Tu (D(D) for all datasets D. Also, each rule in R' sound for M, as a consequence of r being sound for M. We will construct R by including in it rule for each rule in R'.
Base Case
21

---

Consider each E R'. If contains no 3 or 2n operators, then it is already trivially of the form specified in the theorem, so r. r1 and include in R. Also, stated above, ri sound for M. Otherwise, we have that is of the form 2n P.C. n C E A, where P is binary predicate, C1 an EL.UQ concept, C2 an ELUQ concept without disjunction, and n positive integer.
We now inductively define a sequence T of ELUQ rules that such for all i E {I,..., k 1}.
Ti+1 sound for M
2. M++1 subsumes r;
Inductive Step
For this purpose, consider the last defined rule rı: we define r1+1 and prove the above properties.
If T3 contains no 3 or 2n operators, then let k := i and cease the inductive construction. As assumed in the inductive hypothesis, r; is sound for M. Otherwise, we have that r; of the form 2n P.C. 7 C2 Cc A, where P is a binary predicate, C₁ an ELUQ concept, C2 an ELUQ concept without disjunction, and a positive integer.
Now let ri+1 be the rule 3P. E A. Trivially, T++1 subsumes rs. since they have the same head and whenever the body of ri+11 satisfied, sound for M. For this purpose, assume to the contrary that ri+1 is not sound for M.
the body of rs. remains to prove that 71+-1 is
If for all datasets D1 such that P(a, b) E D1 and (D1,a) a) }= C2 for some constant b, we have A(a) E (D1).,. then T:41 would be sound for M. This follows from these conditions covering all datasets that satisfy the body of ri+1-
Likewise, for all datasets D1 such that P(a, b) E D1, (D), F C2, C2. a, and b not mentioned in any other fact of D2, we have A(a) (D1).) then li+1 would be sound for M. This is because neither mentioning in another fact of D₃ nor having a b will decrease the output of M(D1) for node n
So instead there exists some dataset Dj such that P(a, b) E Dr, (D1,a) C22 and A(a) & TM (1)) for some constants a * b, where b not mentioned any fact Dj besides P(a, b). Here follows representation of D1:
a
C2
Now consider vū, the output for node when M is applied to enc(Di), and let S S in the index of the unary predicate A in the canonical encoding. Since A(a) & (Mi,)), we must have vil < t. Let := tM-viípp
We now define a dataset Dm, parameterized by non-negative integer m. We define D = D1 (P b)} U (P(a, P(a, cx)) }} (P(a, (1),,,)),.., P(a, 6m)3 for distinct constants Cl,.... Cn. bi.bb,..bb.. bm (all also distinct from a) and further require that (Dm, C1) F Ci.... (Dm Cx) C1. by including other facts necessary for the satisfaction hold. We also require that b .... bm are not mentioned in any other facts of Dm These further requirements may be satisfied in several different ways, but any them will suffice for the definition of Dmn. Here follows representation of Dm
b
④
Ci
P
P
C1
P
P
bm
Cn
Ci
P
P
C2
22

---

Notice that (Dm: a) F C2 and (Dm.a) P.C A(a) E Tr, (D.). But from the soundness of ri. we also have A(a) E (D,) However, as m - oc, the computation node v" when M is applied to enc Dm) tends to that of M being applied to enc
this is consequence of the definition of MAGNNs. Thus, there exists some m. such that when considering vř. the output of M applied to enc (m.), we have v2 [p] < (note that this requires the use of continuous activation functions, otherwise it is possible that [i 2 t for every m).
But since / < tM, we have vi.pp] < M. And since A(a) E TM(Dm), we have vi.pp] 2 L.. This a contradiction, so r++1 sound for M..
End of Inductive Construction
Since ri contains finite number of 2n operators and each 7++1 has one fewer 3 or 2n operator than 7v, this inductive construction is guaranteed to terminate for some k.
We thus have sequence Tı, "...... of ELUQ rules such that for all i E {1..... k - 1),
subsumes rt. Since r subsumes rı. for all datasets 1) we have (D) C Tr. (D). So T, (D) g
Tr, (D) ... S Tr (D), and thus Tr, (D) C Tr, (D). Also, notice that contains no existential
quantifiers or disjunction, so it is of the form specified in the theorem. Furthermore, F%k is sound for
M, as was shown above. We include ty in R.
Conclusion
We now have a set Rt of rules of the form specified in the theorem, such that each is sound for M. It remains be shown that R subsumes r.
Let D be a dataset. Recall that T,(D) = Ty. (D). But for each 71 E It' there exists Tkk E such that Tr, (D) S Tr, (D). Thus UnER T,, (D) S U Tra (D), and so Tn (D) S (D) Hence,
have (D) (n()), so subsumes r, required.
A.3 Proposition 4
Proposition. Let M be MAGNN and r D.P. A1 m.. 1 Ax C Ast1 1 be rule of the form given in Theorem 3. Define Drare := (A)(a).... As(a), (a, Py(a, b)} for constants & Then is sound for M and only (a) (Drre)))).
Proof. We prove both direction of the and only if. First, assume r is sound for M. Notice that (Douse: a) F B, where B denotes the body concepts of r, we have Ak+1(a) T, (Dpsee) But since r is sound for M, T, (Dasee S. TM and thus (a+1(a) E TMu(Dase as required.
Now assume that Ac+1 (a) E (Drase) We prove that r is sound for M. For this purpose, let D be an arbitrary dataset: we prove that (D) C (D). So let As+1(e) E T,(D).
Extending The Base Dataset
Consider the set Deplits. consisting of every dataset (A1 (a), -.. As(a), Pi (a, Pa (a,,bb)) bj)} for (not necessarily mutually distinct) constants b,,...,u, by that are distinct to a. Then for each such D1 D splits the computation of M(D1) is identical to that of M(Dresc). So A++1(a) E (D1).
Now consider the set D Dmerges consisting of every dataset (a), (u, Pi b.., (a, for (not necessarily mutually distinct) constants b bi.... bj that are not necessarily distinct to Each D2 E Dmerges either has a distinct to all by..... by. or it does not. does, then D2 E D in which (a)1(a) TM Otherwise, D2 has corresponding D1 E Dspliss where each b, such that b; = a is swapped out for another constant by * a.
Consider vî and v the outputs for node d when M is applied to D, and Da respectively. Notice is because merging each of the neighbours 6, of into b, will never decrease the output of the MAGNN.
that, by the operations MAGNNs, for all p E [1,..., 8) we have ví [p] S v4. v4][p). This
23

---

Now let p be the index of Ag+1 in the canonical encoding. Then since vi S v and A (1) have tM I vi S vž [p]. and thus 1 E TM So for every D2 D mergess we have (a+1(a) E (
Conclusion
We now prove that (c)1(c) E (D) Since Ak+1(c) E T,(D), there exists (not necessarily distinct) constants d1,..., dj in such that D' := (A1(c), As(c). dc)..)...... ((c, d,) C D. There are potentially multiple such constants d; that could be used for D' S D. For each E {I. j}, if there exists constant d; & such that (c, d,) D, then choose this de be in D'.
But then, up to the relabelling of the constant c - O, we have D' E Dmerges, so A E (M()"). since MAGNNS are agnostic the specific constants used.
is a superset of D'. Consider of E enc(D') and the application of M to D' and D, resulting in vi and vi. respectively. Any unary facts in 1 that are not in D' will preserve v S Vvi. from the definition MAGNNs and the canonical encoding. The only binary facts D that are not in D' that could decrease the computation of vg. (leading v?. vil[p] vi.[g for some index q) are of the form Pi(c, d,) for c + d,, where D' contains some fact (c c). However, as was stated in the definition of D', if D contains fact (c d,) with + d, then D' will not contain Pa c). So, facts added when extending D' to D will decrease the computation of vi and we obtain vi S vL.
Now let p be the index of Ak+1 in the canonical encoding. Then since A (c) E TM(D"), we have IM S vi [p] S vilp), and thus AR+1(c) E (D), , as required.
A.4 Lemma
We provide lemma that is used in the proof of Theorem 6.
Lemma 7. Let M be MAGNN, Da dataset, and con Da) constant. For any E No and E Da), we have (Da, c) F Cū, where Cf is dependent on Da.
Proof. We prove this by induction on l.
Base Case
For and some E con(D.) Da), have Cj T A n 7. As. where Ai,... A all atomic concepts A, such that A,(c) E Da. But then (Da: c) - A₁ for every A; in the conjunction of Cg. (Da.c) Cg-
Inductive Step
Consider some & E N, and assume that the claim holds for f 1. Let E con(Da). We have C = A .... 77 Ag n C", where Ai, Ag are all atomic concepts A, such that A((c) E D2 and C" denotes the remainder of the concept. Similarly to the base case, obtain (Da, }= A n... n Ag-
C' is a conjunction of T with a concept Cp for each binary predicate P such that there exists P(c, E D.. So consider such a P: we prove that (Da, c) CCp.
Let Ci, Cn be all the constants 6; con(D.) (Da) such that Plc, D. Then we have Cp 3, P, 1.: ) Sn P.T. Since e has exactly n P-neighbours in D., we have (Da: c) - Sp P.T. By induction, (Da, c) += Cp= for every i E {1, [1,,.., n]. Also, all Ci,..., are distinct. So from the semantics of En, (Da, c) + P. ... Cfa Thus, we obtain (Da, c) - Cp.
Now since (Day c) }= Cp holds for every binary predicate P, we have (Daye) }= C", and thus (Day c) - C%2 as required.
D
24

---

A.5 Theorem
Theorem. For any MAGNN M, dataset Da, and fact A(a) (D), the rule r CL 5 A
(dependent on Da) is sound for M, and A(a) E (D.)..)
Proof. First, have A(a) (D,), since A is the head of r and (Da. a) -= Cý, follows directly from Lemma 7. remains to be shown that r is sound for M. Let D, be dataset: to show soundness, prove that (Db) _ (D,)... For this purpose, let A(b) E (Db) be an arbitrary fact; prove A()) E (D)))
Minimal Satisfaction Dataset
We define a dataset Dt. in an analogous fashion to the definition of C% to be the L-hop neighbourhood of the constant a in Da..
Given e E con (a)) E No. we inductively define a dataset DI by D3 == (A,(c) A,(c) E Da)- Then, if L 0, we are done: Dř has been defined. Otherwise, for each binary predicate P. let C1, On be all the constants & E con(D,) such that P(c,c)) E Da. Then, if > O, extend Dř as P(c,a) P(ecc) each binary predicate P. Note that each 1 defined inductively.
follows: D == Dÿ U DE DD
Di (PP(c
Da). Dद is extended for
At this point in the proof, we have three datasets to consider:
Da the original input dataset from which fact A(a) was produced by the MAGNN TM
D2 an arbitrary dataset instantiated for the proof of soundness
Di the L-hop neighbourhood of the constant a in D.
In the remainder of the proof, show the following in sequence:
(1) A(a) E (M(Dt), since A(a) E (M)(D) - follows from definition of Dj as the L-hop neighbourhood.
(2) A(b) E (D))),, since A(a) TM follows from the fact that any differences between Do and D1, cannot decrease the MAGNN output for t / plus a mapping between constants of Do and Di.
(1) Prove A(a) E (D)) Using A(a) E (M,(Da)
First note that DJ, C Da. since only facts from Da are included in its definition. Consider v2, vł the output M on Da. D2 respectively for the vertex corresponding to a, and let p be the index of A in the canonical encoding. Since A(a) (Ma))), [i tM. However, since M has only L layers, the computation of vî, affected only by vertices in the L-hop neighbourhood
o².
Since D2, contains exactly the L-hop neighbourhood of a, we thus have vř vz'. This implies vL. [p] tm and thus A(a) E TM(D?).
(2) Prove A(b) (Ds) Using Ala) E TM(
First, we inductively construct a mapping क (f) + con D2) from constants to constants. Intuitively, this will track "corresponding" constants from the two datasets in the computation of
M. We also assign a "level" to each constant of con(Dg) from the set {0, (O.... L}. We perform the
induction from L 0, simultaneously proving that for each constant E con(D))) of level E, we have:
(Di,c) C2 and (Do, (c)) - C²
(3)
Inductive Construction of Constant Mapping
25

---

For the base case, we define T(a) = b, and let the level of a be L. Since A(b) E (D)))). (D,, F Ci the body of So we have (D,. x (a)) = Cf and also trivially (D) Ct.
Now consider each constant c E con( D1) of level & 2 1; we define æ for constants of level l 1. For each binary predicate P, let c1y...y Cn. be all the constants e2 E con(D.) such that P(c, ci) E Da- Let the level of each C12 C.. be l 1.
Let d == [(c). By the inductive assumption, (Do, T(c)) } Cū P,P. 221 n Sn P.T. So there exist distinct constants di, dn E con(D,) such that (Do: d1) F CC1 1-1 d,) - - and P(d, d1) E Do, d(d,dn) E DD. We define (ct)) = di...., π (Ca) ) dn. Notice that we have that (Db, (())) } Chi (Do, ((a)) H + -F=1 and trivially from the construction of Dq, that (Df, c1) } CcL C2-1... (Do, Cn) F C as required for the induction proof.
have that (Do, d) }
Monotonicity
For each constant E con(D)) and d E con D,), let vi, vi be the outputs when M is applied to Dj, and D,, respectively. Likewise, let E E denote the edges and No. No the neighbours in enc(Df,) and enc(D;) for colour o, respectively. We prove the following claim by induction on & from to L.
Claim: For each l E {O...., L}, constant c E con(D9) of level e' E (e, L}, and i {1,...,ākk we have vi[l] S v. [ [1].
Base Case
For the base case (L 0), let E {1,... do), let l' (0...., L}, and consider each constant c E con( (D2) of level l'.
As proven in Equation (3), we have (Di, Cj and (D,, IC)) F Cÿ. Recall that Cū. includes Ag. where A.,... Ag are atomic concepts A' such that A'(c) E Da. From definition of Do, the unary facts in DJ that mention are precisely A (c(c).... ..., (x(c). Then since (Ds, x
T A
(c)) + Cs we have A₁ (T(()),,,.... As(x(c)) E Dg.
So if v 1, then A((c) E Di. where A, is the unary predicate with index i in the canonical encoding. This implies that (T))(c)) Ds. and thus vo ( [:] 1. This proves the base case, since vild =
vo [ [ 1 and the definition of the canonical encoding let us conclude that
vill S v [...
Inductive Step
For the inductive step, prove the claim for E > 1; to do so, assume the claim holds for f 1. Let E (e.... L.). let i E (1....,z) 5.), and consider each constant E con(D)) (Dt) of level f". We prove that vg[i] v
(() [i]. Consider the computation of v and v (e)))))
4
8e
vild oe beli] +
Σ
A
Σ
Σ Beli mean(fu:-1l))) (v u) ET))
oECal
(4)
6
(0) 1 σi
buli] + Σ
A
Σ
Σ
Beli mean ( (T) u) E E. B))
ccCal j=1
(5)
26

---

From the induction hypothesis, since e is of level l' 2 é 1, we have vi-ı S ve [b]. Since all else in the above equations is equal, it remains to be shown that, for all colours E Col and j E (1....06-11)
mean (f (0 u) E ETD) mean( (f (,*(9) u) E)D)
So let o E Col, j E (1,...,6--1)) and let P be the binary predict corresponding to colour o. Now if there exists Ck E con( such that P(c,cg) Da, then by the definition of E as the edges from enc(Di) we have E = 0 and thus mean( ( [ (v", u) E E = O. So the incquality trivially holds, since each iz- [j] is non-negative.
Thus, instead consider all Cl, Cp E con(Da) such that P(c, ck) E Da. Note that each such Ck has level L' - 1. Then since L - for each Ck-
1, from the inductive hypothesis, we have v 8--1 [
Furthermore, since E con D has level 6", we obtain T(c)) } Cg. from Equation (3). Thus, we have (D,, T())) F (C .-..... C+- Sn P.T. So there exist exactly n distinct constants di...., dn con (D)) such that P(T(c), E D ..., (()())) d.) E D3. However, recall from the definition of that these constants are precisely d1 = π (c)), dn <C..).
From the canonical encoding, {u** (v", e**) }*} and (1*((>) (u7(e), vt(a)) En} ( (u v E E"). Also, as stated above, from the inductive hypothesis, we have v-n [i] S v [i] for each ex. Combining these, we obtain the inequality mean( (f [--- (v u) E B s mean [ū (x*(e) u)
thus have one-to-one correspondence between the sets
B).) This allows us to conclude vi[i] S v. (0 [i] as required.
Conclusion
We have shown that for each E {O,...,L), constant c E con(Di) of level E fl...., L}. and i {1...., ) we have vild S [(() [t].
Now let p be the index of in the canonical encoding. We obtain vg,[p] I v.
v-(a) [p]. and thus
v [p] S v..[p), since (a) and a of level L. But since A(a) (D),),, vi(p) Lu thus
[p] f.s and finally A(b) E (D,)))
27

---

B Algorithms
B.1 Checking Soundness of ELUQ rules
Algorithm 1: Check the soundness of all rules of the form given Theorem for MAGNN M
Input :MAGNN M
Output:S: set of sound rules for M of the form given in Theorem that together subsume every ELUQ rule that is sound for M
5 foreach {1,... + ] do
// result set
// consider rules whose body contains exactly n concept atoms foreach candidate rule form
r: T.. n
n A C Ak+1
with exactly n body concepts do // check subsumption by sound (smaller) rule
3r' S with head A whose body concepts are contained those of r then SU (r)
continue
// construct dataset with fresh constants a a b
Druse + (Ai(a)..... As(a), Pi (a, b). (a, 1/ test the soundness of r, using Proposition
if A (Dmse)))) then + S U(r)
return S
B.2
Refining Explanations
There are two primary issues with the rules defined in Theorem 6.
First, the size of the rules can be large in practice, making them difficult to read, and also limiting their ability to generalise to other datasets. The size of the rule can iteratively refined by pruning facts from D2 and then recomputing Ci.-
More precisely, for D/= = Da \ {a} for some unary fact a E Da such that A(a) TM()),,, the rule r': C% [ A (dependent on D') is still sound for M, by the same argument made in Theorem 6. This can be done iteratively, until find that A(a) & TM (D.). This works similarly for DY == Da Da. where D. = {P(c, eI),... P(c, cx)) for some binary predicate P and constants C....,, such that there is no fact P(c, d) Da with P(c, d) Da. and A(a) (D,(',) Note that there are many different choices for a and D, in each iteration, so the space should be searched to find explanatory rules with minimal size. Only facts a and sets D. within the L-hop neighbourhood should be considered for pruning, this is what will decrease the number of concepts in the body Cy.
The second issue is that the inclusion of the S.. P.T term limits their ability to produce facts on other datasets with higher numbers of neighbours. As a possible solution, we can substitute n for some m > n. Consider a dataset D2 and fact A(a) E Tm((D.) Instead of defining C% := O S, P.T in Definition we can define C = such that extending D. with D = [P(c, d1). ..., P(c, dm-nn)} for fresh constants di,..., dm-n still leads to A(a) (D, Di). the above done for multiple constants CI, C₁ and E,, i..... Eg. must be ensured that A(a)- (D. U D2 U...U,,,
Sm P.T, for some m 2 n. Any m can be chosen
The simple approach we take in this paper is as follows. Given a predicted fact A(a) on a dataset D. we first identify all atoms A ..., An such that (a) E D, and check if the rule A₁ 1 17 A. C A is sound using Proposition 4. If it is not, we then identify all binary predicates Pl. P. such that (a b) D for any constant b, and check if the rule A n n A, 3P₁. n ... n 3Pm. C A is sound using Proposition 4. If either of these rules is sound, it explains the prediction A(a) on D.
28

---

Dataset
Agg
Weights
%Acc
%rrec
%Rec
F1
LUBM
Mean
Standard
97.1 = 0.0
9..
9.0
9..1
Non-Neg
91.5 = 0.0
8.8
96.4
91.9
Max
Standard
95.7 0.0
95.3
96.3
9..8
Non-Neg
91.6 = 0.0
88
9.0
92
Sum
Standard
96.1 0.0
9.0
9.0
96.1
Non-Neg
91 = 0.0
88.1
949
91.4
Table Results for GNNs across various aggregation functions and standard non-negative weights, for the LUBM dataset. Metries are computed on the test set and shown with 95% CI.
Dataset
Agg
Weights
%Acc
%Prec
%Rec
WN-hier
Mean
Standard
99.5 + 0.0
99.5 + 0.0
99.5 0.0
99.5 + 0.0
Non-Neg
99.8 - 0.0
9.0
9.0
9.0
Max
Standard
99.3 = 0.0
99.5
9.0
9.0
Non-Neg
99.9 0.0
0.0
100
0.0
Sum
Standard
98.9 - 0.0
0.0
9.0
0.0
Non-Neg
98.8 0.0
97.6 0.0
100 1
98.8 +.0
WN-sym
Mean
Standard
99.4 + 0.0
99.5
99.3
9.0
Non-Neg
100 = 0.0
1.0
100
1.0
Max
Standard
99.3 09.3000
99.1
9.0
9.0
Non-Neg
100 =
1.0
100
1.0
Sum
Standard
99.1 + 0.0
9..
9.0
99.1
Non-Neg
100 + 0.0
1.0
100
1.0
WN-hier -N-hiee_nmmhier
Mean
Standard
86.2 0.0
0.0
8.0
8.0
Non-Neg
71.6 0.0
0.1
58.8
6.0
Max
Standard
86.9
8.0
8.0
0.0
Non-Neg
0.0
7.0
6.04
0.0
Sum
Standard
89.5
88.1
9..4
0.0
Non-Neg
66.9 +: 0.0
7.1
59.3
62.7 0.1
Table Results for GNNs across various aggregation functions and standard non-negative weights, for the LogInfer datasets. Metrics are computed on the test set and shown with a 95% CI.
C Full Results
Full results for mean, sum, and max aggregation given in Tables 5 to 7. Randomly sampled sound monotonic rules of the form given in Theorem 3 are shown in Table Randomly sampled explanatory rules for predictions LUBM of the form given in Theorem 6 shown in Table 9.
Randomly sampled explanatory rules that have been reduced size are shown in Table 10. The final entry in the table is an example of predicted fact where the size reduction process failed and fell back using Theorem 6.
On average, out of 1990 true positive predictions, the model only failed 22 times to explain the predicted fact using rule from Theorem 3. For of 5 trained MAGNNs, it only failed 10 times each. For the other MAGNN, it failed 72 times. One factor that brought up the average number of body concepts is that some of the explanations were very large: for example, the rule that explained the prediction Department
UniversityO.edu) had 1914 4 body concepts.
29

---

Dataset
Agg
Weights
%ccc
% Prec
%Rec
F1
FB237v1
Mean
Standard
68.7 0.0
95.4 0.0
39.3
55.7
Non-Neg
71.8 = 0.0
64.8 0.0
0.0
Max
Standard
0.0
94.9
35.9
5.0
Non-Neg
75.8
0.1
6.0
0.0
Sum
Standard
68.4 0.0
9.0
0.0
5.0
Non-Neg
73.8 + 0.0
7.
64.5 0.0
7.0
WN18RRv1
Mean
Standard
93.7 + 0.0
98.5
88.8 0.0
93.4 0.0
Non-Neg
95.5+00
98.1
0.0
0.0
Max
Standard
9.0
9.0
9.01
9.0
Non-Neg
0.0
98.7
0.0
0.0
Sum
Standard
93.9
9..1
91.6 0.0
9.0
Non-Neg
94.9 0.0
97
92.7 0.0
94.8
NELLv1
Mean
Standard
75.2 0.1
03.8
53.4 0.2
0.2
Non-Neg
9.0
0.0
0.0
0.0
Max
Standard
1. 0.0
0.1
5.1
Non-Neg
9.0
9.0
9..1
9.0
Sum
Standard
$1.8000
18.3+
0.1
7.8
Non-Neg
92 + 0.0
86.3 + 0.0
100 + 0.0
9..
Table 7: Results for GNNs across various aggregation functions and standard non-negative weights, for the standard benchmark datasets. Metrics are computed on the test set and shown with a 95% CL.
Dataset
Sample Sound Rules
LUBM
T C Publication
T UndergraduatteStudent
BauthorOfPuulicationnn7 T ResearchAssistant
HadvisorOf. T AssocciateProfessorr
JcourseTakenBy. ThasTeacher. C Course
Department UnderggaaduateeSuudent 3advisorOf.T C FullProfessor
WN-hier
cirrnber_of_dmmiinn__o
Y) + >_member____ Saanbbrrmeronym(XX Y)
derivationally
laatooaallllyyeeeteeeeeeeee related_fonte form Y) A _iiiilrr_to{A) Y)
synset domain coanain_topii___1 sfoeo_ooxx"_ Y)
also ceoo_see(X., Y) A similar to (o(XYY)
_verb grob_group(AX) (X,
instance_hyyperyym(XX (
WN-sym
has has_part(X, Y)
A
similar to(X,
derivationally
catpiiinnnllyyellteeeeeeeee rewated_ relaatedfoom(XX)))
WN-hier amhier
has Stas_par([X,]
A
member Baciiier_rroommmX,.11 (X,Y)
member of domain domain_usagel X,
has baa_pprr(XX] (,,, Y)
^
verb Berb_group({ Y)
domainnusage((X hypernym(X, otaps//XoXaaoaooooooooooaoannnno Y) - _ _aeso__seeXX, Y)
member of domain uwwgeuX,aaea.. (X,
FB237v1
T + /muscc/isttuner/nntttuunnaasssss + pponpeeppesoosssiiiiinggeepeebpp hrtpriiinnnrrraaaioossspipiiiiii (X, Y)
hhssehiilliieesshiiis.Lootttttti /iln/iin//////////gnn//>/ Y)
NELLv1
oggnizaiiooeemmmaaccccessssy/yy, hatpa/amiiiniiioooooa/a//nanonnn X,
organizationhhircperson/.K worksfor(X. X, Y)
orgaiizaioneemminteeprrrso///X>>
organizationnhiedpersoo (X,Y)
Table 8: Randomly sampled sound monotonic rules of the form given in Theorem
30

---

Fact Rule
T C Publication
Fact Rule
University httpe//iyhhtt////www////////////
T n ( (GraduateStudent 3 JuauthorOOPPublication...
Publication) n S authorOfPublicatioo.. T)
Si graneeddUnnegggrdutteeeeeee....
University
Fact Rule
TrradaateStudennttttt////wwwwwww
T
FlauthorOfPubliiattonn,
Publication, Publication)
authorOfPublication. [ GraduuateStudentt
Fact Rule
VaachingAsistant(tttt/////w/.// htwp://wwwee.ttliieeoooeooooaaae GraduateStudent
10 7 EgauthorOOFPullicationnn Publication)
authorOfPublicatiion. T TeachingAAsistant
Fact Rule
ResearchAssistant n 2baauthorOrPuubication.. Publication, Publication, Publication,
pubiicatoon,,Pllicatiino
Publication) S5 authorOfPublicatioon. GraduateStudent
Fact Rule
T UndergradduateeSuudent
Fact Rule
T n #gauthorOfPPbliicttonn.. (Tublicciiio
Publication, T) n S3 authorOfPubllicttion.
C
TeashingAssistant
Fact Rule
T n 3iaattoorOPPublicctionn... I authorOrPuulliattonn.TT C GraduateStudent
Fact Rule
T http:h/ppp//wwwo.pppprtttttttted
TiacourseTakkenBy. UndergraduatteStudent. UndergraduaatStudenn,
UndergraduateSttuden,, UndergraduateSttueen, UndergraduuateStudent,
LindergraduattSStuden,,, UndergraduuateStuddnn. UndergraduutteStuddnn. T,T,
UndergraduateStudden,, UndergraduuateStudnn,, UndergraduatteSuudent course ToursBTakeBBy.TT r 3 hasTeacher, (wapacchee.AAsssssssaaPooooee (AssistantProofesoor r
Su4
3 aravisorOff UndergraduateSttudent, UndergraduatteStudnn,, T, T, SetachhinAsssiteee GraduateStudent, GraduateStudennt, T) 7 S, advisorOr. wtw..rnnnnanttttuuuubbbiiio (Publication, Publication, Publication, Publication, Publication) n has Teacher. T Course
Ss authorOfPublication.
Sı
Fact Rule
wttps//sttttttttp///////////ppea T 7 aaauthooO@Publiiatioonn (Publication, Publication, Publication, Publication) 7 authorOfPuulicattinn. T ResearchAssistant
adtu/GraduateSSuudnn[]]
S1
Fact Rule
T 7 TaccourseTakkenBy... U UndergradduateStuden,, T, UndergraduutteSuuenn.
UndergraduatteStudlen, T, UndergraauuatteSuuden)) course'Taken TourseTakenBB..T
Sg
has TeacheTerrr... (eaetuer
7
I GraduateStudent authorOfPublication..T (Publication, T, Publication, Publication, T)
has hasTeacher. T n 3 B hasseaahhnn/AAsssttaa (Teaching
JrauthorOPPublication..
S5
S hasTeachhnngAsssitan. T Course
Fact Rule
hniiversiiihttt////ww...niveeees 333.
T n Iagrantedddddeggraaattteeeege Seraaaeaeeeeeenaaaaaaaaeettee 3, OuthorOOfubliiattionn (GraduateStudent Publication) n S, authorOrPublication. GraduateStudent n auuthorOfPulliiatioon
T, Publicaat,,,, T, Publication, Publication) grantedtUndergraauateeeeee
Ss authorOfPublication.. r S2
University
Table 9: Randomly sampled explanatory rules of the form given in Theorem 6, shown with the corresponding facts produced by the MAGNN.
31

---

Fact Rule
Publication
T E Publication
Fact Rule
T C Undergraduaatetuudent
Fact Rule
GraduateStudent 7 IaathorOPPPubliattinnn. Teaching-Assistant
Fact Rule
GraduateStudent r1 EauthooOOOPuuliiititinn T ResearchAsssistant
Fact Rule [ _ Rescarch/sssssttnnaa Saverssssuueettteeeececccccaaaat
Fact Rule C ResearchhAsiisaat
Fact Rule TauthorOrPubllicationn. T GraduateStudent
Fact Rule [ GradutteSttetnnnnneeeenenttntttt
Fact Rule I 7 TaathooooooPioiiiiiiiiioooooo Cttpa/aiiatttttttattatotaotooaaa hararaeeeeeeaatotooooooeoannneee GraduateSSuudent
Fact Rule
TeastinggAssistantt BauthoofPPPuiiiiiiiiiiiion Sanpre/eeeencctttoooonnnnnnnnnnn
GraduateSStudent
Fact Rule
Ecourse TakenBy. 77 ThasTeacher.. C GraduateCourse
Fact
Rule
3course/TakenBy n 3hasTeacher. T [ Course
Fact Rule
C http:///wwww...p..//ooo////////s
Fact Rule
http:///wwssssoo/oo//ooo/oo/o/// C AssistannPooooossssooor
Fact Rule
C fwt.h//wwsscct///////popp/orrord
Fact Rule
BrrattdUnndeggrraaadttDerrrrrrrr Universiity
Fact Rule
University BgeamtddUnneegggdduteeeereee.. C University
Fact
University(httpp//www (http://www.. http://wwww.uiiiriiiyyyy//o...ll
Rule
GraduateStudent,, GraduateStudent r ResearchAssistarr GraduateStudent I7 TeachingAAsiitant)) IT S1 BirauthoOO/Pulicattoo PT,billiaaiiinnn, Publication,, pubiicaatonn,Piiicatioonn Publication, Publication, Publication, T, Publication, Publication, Pubiiiation,iiiiiiiiinnn. T, Publication, Publication, Publication, Publication, Publication) 77 SI7 authorOfPPullicatio... ar (ttrrisorOO.n.nnngggrrrrarree (UnderggraduaateSruuenn, htwp://rnduuuuuuuuueeeeutuerrrrr UndergraduateSStuden,, UndergraduatteStudent, UndergraduateStuuden,, T. T. GraduateStudent, GraduateStudent ResearchA GraduateStudent, T, TeachingAAssistan 7 GraduateStudentt GraduateStudent, GraduateStudent Teaching GraduateStudent TeashinggAsissann)) n S14 Pubblicatinn,.... Publication, Publication, Publication, Publication, Publication, T, Publication)
University n
advisorOf.T
advisorOf. n PpauthorOfPubiicationn. Publication,
S. authorOfPublication. T) n AggaateedMasttessggreeTToo (Lecturr)) n Si
n grantedDoctoralDeggrell University
grantedMassterDeegreeTTo
Table 10: Randomly sampled explanatory rules that have been reduced in size, shown with the corresponding facts produced by the MAGNN. The rules are grouped by similar bodies / heads. These rules come from 5 MAGNNS trained with different random seeds.
32


Reviews:
[{"review_id": "mHv1swRUqM", "reviewer": "Reviewer_bVNC", "summary": "The paper presents a theoretical analysis of the expressive capacity and explainability of monotonic mean-aggregating GNNs (MAGNNs). It shows that predictions made by MAGNNs can be explained by combinations of simpler logical rules, and provides a constructive approach to derive such rule sets. In addition, the authors propose a method for mining sound rules from model outputs, enabling post hoc explanation of predictions. These two directions together support the extraction of interpretable rules when applying GNNs to knowledge graphs, contributing to a better understanding of their behavior.", "questions": "-\tComparison with rule-mining algorithms: There exist a number of works focusing on rule mining from knowledge graphs, including both deep learning–based and symbolic rule-based approaches (e.g., [1], [2]). To what extent are the rules extracted by these existing methods sound? Do those algorithms—and the proposed method—tend to capture similar types of relational patterns?\n-\tNon-negative weights: The performance difference between GNNs with standard weights and those constrained to non-negative weights varies across datasets. As I understand it, the non-negative parameter space is a subset of the unconstrained one, yet the model with non-negative weights performs significantly better on the NELL dataset. Could the authors provide an analysis or explanation for this non-trivial behavior?\n-\tBroader GNN categories: While extending the theoretical framework to other categories of GNN may introduce additional complexity, it would be beneficial to include a discussion or empirical comparison with other GNN variants. Could similar experiments be conducted on more expressive architectures or more complex networks?\n\n\nReference:\n[1] Xu, Zezhong, et al. \"Ruleformer: Context-aware rule mining over knowledge graph.\" Proceedings of the 29th International Conference on Computational Linguistics. 2022.\n[2] Wang, Xiaxia, et al. \"Faithful rule extraction for differentiable rule learning models.\" (2024).", "limitations": "Yes", "rating": 3, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n-\tThe paper provides a formal and clear analysis of the expressivity of MAGNNs, offering theoretical insights into the reasoning strategies employed by GNNs in prediction tasks.\n-\tExperiments on representative datasets demonstrate the effectiveness of the rule mining algorithm. The extracted rules are interpretable in many cases, which aligns well with the goal of enhancing explainability in knowledge graphs and GNN-based models.\nWeaknesses:\n-\tBoth the theoretical analysis and experimental evaluation are limited to mean-GNNs with non-negative weights, which represent a relatively narrow and simplified subset within the broader family of GNN architectures.\n-\tThe experimental section lacks a comparison with existing rule-mining algorithms for knowledge graphs, which makes it difficult to assess the relative effectiveness of the proposed method.\nMinor weakness:\n-\tSome parts of the formalism, particularly those concerning the construction and subsumption of ELUQ rules, are dense and may be difficult to follow without substantial prior knowledge of symbolic reasoning.", "was_revised": false, "final_justification": "", "rebuttal": "We would like to thank the reviewer for their engagement with our paper and the time they took to review it.\nPlease see below for our responses to their comments and questions.\n\n## Weaknesses\n\n**Query:**\n\n*Both the theoretical analysis and experimental evaluation are limited to mean-GNNs with non-negative weights, which represent a relatively narrow and simplified subset within the broader family of GNN architectures.*\n\n**Response:**\n\nWhilst the GNN architecture is limited, this was necessary for the analysis and rule extraction we were able to perform, and the results in Table 1 show that this restriction results in models which are still viable in practice. The approach of restriction to non-negative weights has been followed in several past works, for max aggregation [4] and sum aggregation [3]. Our work extends these techniques and analysis to a common aggregation function not yet considered (mean aggregation).\n\n**Query:**\n\n*The experimental section lacks a comparison with existing rule-mining algorithms for knowledge graphs, which makes it difficult to assess the relative effectiveness of the proposed method*\n\n**Response:**\n\nThe goal of our paper is not to mine rules from knowledge graphs - this is an added benefit that our results allow for. As stated in our Abstract and Introduction, our motivation is as follows: given that GNNs with mean aggregation are commonly used on knowledge graphs, can we extract sound rules that explain their predictions and determine what kinds of rules can even be sound for such GNNs? With this goal in mind, we believe that comparing against knowledge graph rule-mining approaches would not support the arguments in the paper.\n\n## Questions\n\n**Query:**\n\n*Comparison with rule-mining algorithms: There exist a number of works focusing on rule mining from knowledge graphs, including both deep learning–based and symbolic rule-based approaches (e.g., [1], [2]). To what extent are the rules extracted by these existing methods sound? Do those algorithms—and the proposed method—tend to capture similar types of relational patterns?*\n\n**Response:**\n\nThe rules learned by Ruleformer [1] are given in their section 3, and have the form r (X, Y ) ← r1 (X, Z1) ∧ ... ∧ rT (ZT −1, Y ). This is Datalog (without disjunction, negation, or inequalities), which is equivalent to the rules learned by GNNs with max aggregation and non-negative weights, as proved in [4]. It is unclear whether the extracted Ruleformer rules are sound for the model, as it is not proved in the paper.\n\nBy contrast, [2] prove that the rules learned by DRUM (another method) can be unsound or incomplete, and adapt DRUM such that the rules are sound and complete. In the adapted version of DRUM, the sound rules recovered come from Datalog with inequalities. This is equivalent to the rules extracted from GNNs with sum aggregation and non-negative weights, as proved by [3].\n\nThe rules we consider are fundamentally different, since mean aggregation introduces non-monotonicity into the model. By contrast, both of the above rule fragments are monotonic under injective homomorphisms.\n\n**Query:**\n\n*Non-negative weights: The performance difference between GNNs with standard weights and those constrained to non-negative weights varies across datasets. As I understand it, the non-negative parameter space is a subset of the unconstrained one, yet the model with non-negative weights performs significantly better on the NELL dataset. Could the authors provide an analysis or explanation for this non-trivial behavior?*\n\n**Response:**\n\nThis matches the behaviour seen by [5] for sum-GNNs and [4] for max GNNs (as noted in L321 of our paper). Our hypothesis for this behaviour is that (1) the restriction to non-negative weights acts a regulariser for the model and (2) the patterns in the data do not require negative weights to be captured, so the restriction makes searching the weight space easier for the optimizer. We will add a brief explanation of this to the paper.\n\n**Query:**\n\n*Broader GNN categories: While extending the theoretical framework to other categories of GNN may introduce additional complexity, it would be beneficial to include a discussion or empirical comparison with other GNN variants. Could similar experiments be conducted on more expressive architectures or more complex networks?*\n\n**Response:**\n\nOther works have already performed empirical and theoretical comparisons between GNNs with different aggregation functions, such as [6]. Given that the contribution of our paper is primarily theoretical, we believe that empirical comparisons between the GNNs with mean aggregation used in our paper and other GNN architectures is outside of our scope, and that the wide-spread use of mean-GNNs (see L34 of our paper) is sufficient motivation for the problem.\n\n## Citations\n\n[1] Xu, Zezhong, et al. \"Ruleformer: Context-aware rule mining over knowledge graph.\" Proceedings of the 29th International Conference on Computational Linguistics. 2022.\n\n[2] Wang, Xiaxia, et al. \"Faithful rule extraction for differentiable rule learning models.\" (2024).\n\n[3] David Tena Cucala, Bernardo Cuenca Grau, Boris Motik, and Egor V Kostylev. On the correspondence between monotonic max-sum gnns and datalog. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, pages 459 658–667, 2023\n\n[4] David Tena Cucala, Bernardo Cuenca Grau, Egor V Kostylev, and Boris Motik. Explainable gnn based models over knowledge graphs. In International Conference on Learning Representations, 452 2021.\n\n[5] Matthew Morris, David Tena Cucala, Bernardo Cuenca Grau, and Ian Horrocks. Relational graph convolutional networks do not learn sound rules. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 21, pages 897–908, 2024.\n\n[6] Eran Rosenbluth, Jan Toenshoff, and Martin Grohe. Some might say all you need is sum. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, pages 4172–4179, 2023."}, {"review_id": "Joa5JtCUHx", "reviewer": "Reviewer_Tx4b", "summary": "This paper investigates the expressivity and explainability of Graph Neural Networks (GNNs) using mean aggregation (mean-GNNs), which are popular but lack theoretical analysis. The authors focus on mean-GNNs with non-negative weights (MAGNNs) to isolate non-monotonicity sources. \n\nTheoretical: (a) Characterizes the limited class of monotonic rules (ELUQ) sound for MAGNNs (Theorem 3). (b) Proves MAGNNs can express non-FOL functions (Proposition 1). (c) Defines a restricted FOL fragment to generate sound explanatory rules for any MAGNN prediction (Theorem 6).\n\nEmpirical: Shows restricting to non-negative weights preserves performance on benchmarks (Table 1), extracts meaningful/sometimes nonsensical rules (Tables 2–3), and generates instance-specific explanations (Table 8).", "questions": "1、\tTheorem 3 suggests MAGNNs are limited to trivial monotonic rules. Is this a feature of mean aggregation itself, or an artifact of the non-negative weight constraint?  \n2、\tWhy do MAGNNs extract zero sound rules on WN18RRv1 (Table 2) despite decent accuracy (95.5%)? Is this due to theoretical limitations or optimization challenges?  \n3、\tHow do you reconcile the 15% F1-score drop for MAGNNs on WN-hier_nmhier (Table 5) with the claim that non-negative weights \"do not significantly impact performance\"?", "limitations": "Yes", "rating": 4, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 3, "originality": 4, "strengths_and_weaknesses": "Strengths：  \n1、\tThe paper establishes a robust theoretical foundation through meticulous proofs (Theorems 3 & 6, Propositions 1 & 4) while complementing them with well-designed experiments.  \n2、\tThis work delivers significant originality as the first formal characterization of the expressivity and explainability of mean-aggregation GNNs.   \n3、\tThe paper achieves exemplary clarity through precise definitions and logical theory-experiment separation.  \n\nWeaknesses：  \n1、\tRestricting weights to non-negative values simplifies theoretical analysis but severely limits practical applicability. Negative weights are essential for modeling inhibitory relationships.  \n2、\tRules are trivialized; unclear if results hold for general mean-GNNs. Theorem 3 reduces rules to simplistic forms.", "was_revised": true, "final_justification": "The authors have partially addressed my concerns. However, certain statements remain potentially misleading in light of the reported results, and important clarifications are still needed for precision and completeness.", "rebuttal": "We would like to thank the reviewer for their engagement with our paper and the time they took to review it.\nPlease see below for our responses to their comments and questions.\n\n## Weaknesses\n\n**Query:**\n\n*Restricting weights to non-negative values simplifies theoretical analysis but severely limits practical applicability. Negative weights are essential for modeling inhibitory relationships.*\n\n**Response:**\n\nWhilst negative weights are essential for modelling certain types of relationships, past works have found that restricting GNNs to non-negative weights leads to models that are still viable in practice, such as [2] for sum-GNNs and [1] for max GNNs. Our experimental findings also validate that, in practice, mean-GNNs with non-negative weights can still be viable and achieve performance equivalent to (and sometimes even better than) ones with negative weights (see Table 1).\n\n**Query:**\n\n*Rules are trivialized; unclear if results hold for general mean-GNNs. Theorem 3 reduces rules to simplistic forms.*\n\n**Response:**\n\nWe consider the fact that Theorem 3 reduces rules to simplistic forms to be a strength of our paper, rather than a weakness. Starting from the general fragment of ELUQ, we can prove that any sound ELUQ rule $r$ is in fact subsumed by much simpler rules. The simpler the rules that subsume $r$, the more powerful the result and the more useful they are for providing explanations.\n\n## Questions\n\n**Query:**\n\n*Theorem 3 suggests MAGNNs are limited to trivial monotonic rules. Is this a feature of mean aggregation itself, or an artifact of the non-negative weight constraint?*\n\n**Response:**\n\nThis is primarily a feature of mean aggregation. The sketch of the proof given in L182 onwards relies on the fact that, as neighbours of the same type are continuously added to a node, the computation at that node will become arbitrarily close to the computation on the graph including only a single neighbour of that type, and no other neighbours. This is similar to the technique used in the proof of Property D.7, of [3], albeit to prove different results, and using weighted mean aggregation.\n\n**Query:**\n\n*Why do MAGNNs extract zero sound rules on WN18RRv1 (Table 2) despite decent accuracy (95.5\\%)? Is this due to theoretical limitations or optimization challenges?*\n\n**Response:**\n\nThese results show, as stated in the table caption, only the sound rules of the form given in Theorem 3 (which subsume all sound ELUQ rules). We can still use Theorem 6 to derive sound rules that explain predictions, and there may be further sound rules beyond ELUQ, which while sound are difficult (or possibly impossible) to prove to be sound. Ultimately, this is a theoretical limitation of the paper, as we can only check the soundness of certain kinds of rules - the ones given in Proposition 4 and Theorem 6.\n\n**Query:**\n\n*How do you reconcile the 15\\% F1-score drop for MAGNNs on WN-hier\\_nmhier (Table 5) with the claim that non-negative weights ``do not significantly impact performance''?*\n\n**Response:**\n\nFirstly, this is not a common benchmark, and our claim is that “restricting mean-aggregation GNNs to have non-negative weights does not significantly impact performance on common benchmarks” (L9-10). On the three benchmark datasets (FB237v1, WN18RRv1, NELLv1), performance of non-negative mean-GNNs is comparable or better to those with negative weights. Furthermore, this is one of only a few isolated examples of where performance drops in our experiments, meaning the claim is still broadly true in all our results. Finally, this dataset was proposed by [2] to specifically penalise models that are only able to learn monotonic rules, so it is not surprising that performance decreases when the weights are restricted to only being positive.\n\n## Citations\n\n[1] David Tena Cucala, Bernardo Cuenca Grau, Egor V Kostylev, and Boris Motik. Explainable gnn based models over knowledge graphs. In International Conference on Learning Representations, 452 2021.\n\n[2] Matthew Morris, David Tena Cucala, Bernardo Cuenca Grau, and Ian Horrocks. Relational graph convolutional networks do not learn sound rules. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 21, pages 897–908, 2024.\n\n[3] Adam-Day, Sam, et al. \"Almost surely asymptotically constant graph neural networks.\" Advances in Neural Information Processing Systems 37 (2024): 124843-124886."}, {"review_id": "7z9UymJJ5O", "reviewer": "Reviewer_UPm7", "summary": "The paper studies the class of logical rules that can be encoded as graph neural networks (GNNs) with mean aggregation and positive weights (MAGNNs). Previous work has focused on sum and max aggregation. The authors propose a class of monotonic rules, expressible in description logic ALCQ, that can be embedded as MAGNNs, and thus can be used as explanations for their behavior. They also show, experimentally, that the restriction to positive weights is not too stringent in practice, and that meaningful explanations can be obtained from practical MAGNNs by using their language.", "questions": "- Is there any difference in expressive power between MAPNNs and GNNs with sum aggregation and positive weights?", "limitations": "Yes, they have", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths\n\n- The paper is well-written and deals with the interesting and relevant topic of providing explanations to GNNs in the form of logical rules. \n\nWeaknesses: \n\n- The paper feels a bit unambitious, in my view, as theoretical results are a bit shallow and do not establish a clear-cut difference with previous work. For instance, is there any difference between the rules that can be expressed by MAPNNs and GNNs with sum-aggregation and positive weights? The latter can also express properties that lie beyond FO, but I see no reason why the two might not be equivalent in expressive power. \n\n- The fact that ELUQ is the strongest fragment of ALCQ that can be expressed with MAPNNs was a bit disappointing for me. I understand that this class of results is difficult, but certainly not impossible, and I would have appreciated to see at least some effort in this direction.", "was_revised": true, "final_justification": "This is a reasonable paper, but not at the level of NeurIPS. LoG seems like a more suitable venue for these results.", "rebuttal": "We would like to thank the reviewer for their engagement with our paper and the time they took to review it.\nPlease see below for our responses to their comments and questions.\n\n## Weaknesses\n\n**Query:**\n\n*The paper feels a bit unambitious, in my view, as theoretical results are a bit shallow and do not establish a clear-cut difference with previous work. For instance, is there any difference between the rules that can be expressed by MAPNNs and GNNs with sum-aggregation and positive weights? The latter can also express properties that lie beyond FO, but I see no reason why the two might not be equivalent in expressive power.*\n\n**Response:**\n\nWe assume the reviewer to mean “MAGNNs”, instead of “MAPNNs”. GNNs with sum aggregation and positive weights are characterised exactly by sound rules from the language of Datalog with inequalities, as proved by [1]. This means that they cannot express properties that lie beyond FO, since Datalog with inequalities is a fragment of FO (when not computing to a fixpoint). As such, they are strictly not equivalent to MAGNNs when it comes to expressive power, as we show in Proposition 1 (L136) that MAGNNs go beyond FO.\n\n**Query:**\n\n*The fact that ELUQ is the strongest fragment of ALCQ that can be expressed with MAPNNs was a bit disappointing for me. I understand that this class of results is difficult, but certainly not impossible, and I would have appreciated to see at least some effort in this direction.*\n\n**Response:**\n\nWe appreciate that it is disappointing that we could not extend our analysis to fragments of ALCQ beyond ELUQ, or ideally to ALCQ itself. The reason for this is that the monotonicity (under injective homomorphisms) of ELUQ is essential for our proofs. Both negation and universal quantification are non-monotonic, so we had to exclude them from our fragment to be able to prove the claims in the paper.\n\n## Questions\n\n**Query:**\n\n*Is there any difference in expressive power between MAPNNs and GNNs with sum aggregation and positive weights?*\n\n**Response:**\n\nWe assume the reviewer to mean “MAGNNs”, instead of “MAPNNs”. GNNs with sum aggregation and positive weights are characterised exactly by sound rules from the language of Datalog with inequalities, as proved by [1]. This means that they cannot express logical functions beyond FO, since Datalog with inequalities is a fragment of FO (when not computing to a fixpoint). As such, they are strictly not equivalent to MAGNNs when it comes to expressive power, as we show in Proposition 1 (L136) that MAGNNs go beyond FO. Furthermore, the class of ELUQ rules that MAGNNs can capture is very limited (given in Theorem 3), whereas sum-GNNs with non-negative weights can capture Datalog rules with inequalities, which is a much richer fragment of FO.\n\n## Citations\n\n[1] David Tena Cucala, Bernardo Cuenca Grau, Boris Motik, and Egor V Kostylev. On the correspondence between monotonic max-sum gnns and datalog. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, pages 459 658–667, 2023"}, {"review_id": "CxPCwSUFxk", "reviewer": "Reviewer_1gqb", "summary": "The paper analyzes from a theoretical point of view the problem of providing sound explanations for the restricted class of GNN with non-negative weights and mean aggregation. They prove that it is possible to extract logic formulas to approximate the behavior of the GNN, and carry out experiments to show the interpretability of the resulting formulas.", "questions": "Q1: How is your method different from [2,3]?\n\nQ2: How are the predicates reported in Table 3 defined?", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 1, "clarity": 1, "significance": 2, "originality": 2, "strengths_and_weaknesses": "**Strengths**\n\n- The problem addressed is highly significant, and providing formal logic-based explanations is a promising research direction\n\n**Weaknesses**\n\n- **W1**: The main weakness is regarding the writing style and clarity of the paper. It is very hard to follow the logical flow, and the fact that the paper introduces an abundant and non-intuitive notation does not make the job easier. Below are some examples that I find particularly representative of this weakeness:\n\n  - Authors refer to GNN with the letter $\\mathcal{N}$, which is instead frequently used in previous literature to denote the neighborhood of a node. \n\n  - I could not understand the difference between unary predicates $U$ and node colors $c \\in Col$. \n\n  - Line 269 says \"we define a dataset $D^a_L$ to be the $L$-hop neighbourhood of the constant a in $D^a$\". This is mixing concepts that are apparently distinct, like dataset, constant, and $L$-hop neighborhood.\n\nOverall, I found myself going back several times to the preliminaries to check what symbols mean, and the fact that notation is often introduced as free text in paragraphs makes it very hard to retrieve the desired meaning. A table of symbols might help in this sense, but in general, I recommend a substantial rewriting of the text to favor readability.\n\n\n- **W2**: The explanations provided in Table 3 are very promising and indicate a very interesting result. However, no details are provided about how those are extracted. Authors refer to Theorem 3, which however does not provide a constructive approach to extract those formulas. Also, it is not clear how predicates are defined, and whether they are user-defined or provided in the dataset. This is a crucial detail, as not every dataset may come with this kind of annotation. The authors should, at least, provide a concise and intuitive algorithm to compute those explanations.\n\n\n- **W3**: The paper does not compare nor discuss alternative solutions for extracting logic formulas from GNNs already available in the literature, like [1,2,3,4]\n\n[1] Global Explainability of GNNs via Logic Combination of Learned Concepts\n\n[2] Utilizing Description Logics for Global Explanations of Heterogeneous Graph Neural Networks\n\n[3] Logical Distillation of Graph Neural Networks\n\n[4] GraphTrail: Translating GNN Predictions into Human-Interpretable Logical Rules", "was_revised": true, "final_justification": "During the rebuttal, the authors clarified that some of the points I raised were due to a misunderstanding, which I believe was partially favored by a paper that was difficult to read for a general ML audience (some unintuitive notation, lack of real-world examples to clarify the statements). Presentation issues aside, I believe the results of the paper are interesting and worth publishing, but not enough for a flagship venue like NeurIPS. This is for two main points: the first, the considered GNN family is quite restricted, as also pointed out by other reviewers; The second, the family of formulas that this family can explain soundly is also quite restricted to only monotonic formulas. This restricts quite a bit the potential impact of the work, in my opinion.\n\n**I raised my score from 2 to 3** to reflect the fact that the authors were very proactive and polite in answering all my points.\n\n**EDIT**\n\nFollowing an additional discussion with authors, I further increased the score from 3 to 4. The authors highlighted some relevant insights in their answers, which I believe can reshape in the good the overall paper. In particular, they motivated well why it can be a sensible design choice to have less expressive models but at the advantage of better interpretability.", "rebuttal": "We would like to thank the reviewer for their engagement with our paper and the time they took to review it.\nPlease see below for our responses to their comments and questions.\n\n## Weaknesses\n\n**Query:**\n\n*The main weakness is regarding the writing style and clarity of the paper. It is very hard to follow the logical flow, and the fact that the paper introduces an abundant and non-intuitive notation does not make the job easier.\nOverall, I found myself going back several times to the preliminaries to check what symbols mean, and the fact that notation is often introduced as free text in paragraphs makes it very hard to retrieve the desired meaning. A table of symbols might help in this sense, but in general, I recommend a substantial rewriting of the text to favor readability.*\n\n**Response:**\n\nWe appreciate this feedback from the reviewer, and are committed to improving the readability of the paper. We are grateful for the concrete insights that were given on confusing sections of the paper, and would appreciate more of it: this will allow us to adapt the paper to be more readable by the machine learning community at large.\n\n**Query:**\n\n*Authors refer to GNN with the letter $\\mathcal{N}$, which is instead frequently used in previous literature to denote the neighborhood of a node.*\n\n**Response:**\n\nThis is standard notation in some of the literature, most particularly the works upon which this paper is based [1,2,3]. We typically reserve $G$ for graphs.\n\n**Query:**\n\n*I could not understand the difference between unary predicates $U$ and node colors $c \\in \\text{Col}$.*\n\n**Response:**\n\nAs stated in L68-69, unary predicates are associated with elements of the vector labels of nodes, and edge colours are associated with binary predicates. As shown in L65, the colours correspond to edges, not nodes. We will make this more explicit by editing our paper to state “is a set of directed edges with colour c” (L66).\n\n**Query:**\n\n*Line 269 says ``we define a dataset $D_L^a$ to be the $L$-hop neighbourhood of the constant $a$ in $D^a$''. This is mixing concepts that are apparently distinct, like dataset, constant, and $L$-hop neighborhood.*\n\n**Response:**\n\nAs defined in L60-63, a dataset is a set of facts, which contain constants. $L$-hop neighborhood is well-defined in graphs, which makes them well-defined in datasets given the equivalence defined in L112-120. However, we appreciate that the phrase “$L$-hop neighborhood” may be confusing; we will try to find a better term and would welcome any suggestions.\n\n**Query:**\n\n*The explanations provided in Table 3 are very promising and indicate a very interesting result. However, no details are provided about how those are extracted. Authors refer to Theorem 3, which however does not provide a constructive approach to extract those formulas. Also, it is not clear how predicates are defined, and whether they are user-defined or provided in the dataset. This is a crucial detail, as not every dataset may come with this kind of annotation. The authors should, at least, provide a concise and intuitive algorithm to compute those explanations.*\n\n**Response:**\n\nOn L310-L313 of our paper, we state how the rules are extracted: specifically, we enumerate all rules of the form given in Theorem 3 up to a number of body concepts, then use Proposition 4 to check for soundness. The latter step is not stated explicitly in this section, it is discussed on L199-L203; to improve readability, we will add a reference to Proposition 4 explicitly on L312. We will also add an algorithm in the appendices to show how the sound rules are computed.\n\nAs stated in L58-59, we assume a fixed signature of predicates, thus assuming that they are provided up-front (whether they originate from the dataset or from the user is independent of our claims). In our experiments, we use standard KG benchmarks, all of which come with pre-defined predicates.\n\n**Query:**\n\n*The paper does not compare nor discuss alternative solutions for extracting logic formulas from GNNs already available in the literature.*\n\n**Response:**\n\nWe will add comparisons to these papers in our introduction - we thank the reviewer for bringing them to our attention.\n\n## Questions\n\n**Query:**\n\n*Q1: How is your method different from [4,5]? (please note, we changed the citation numbering)*\n\n**Response:**\n\nWith respect to [4], they only consider explanations in EL, which is a fragment of ELUQ. Thus, our work considers more broad sound rules and explanations. Furthermore, the work provides no formal proofs that their rules are sound for the models - they rely only on empirical evidence.\n\nOn the other hand, [5] learn decision trees from GNNs, and then extract logical rules from the decision trees. These decision trees are not equivalent to the GNNs they are derived from (as can be seen in the fact that their performance differs from the GNNs they are learned from), so the extracted logical rules are also not strictly sound. Furthermore, it is not clear how understandable / human readable any of these extracted rules are.\n\nIn contrast, our work extracts rules directly from the GNN, with the guarantee that they will be sound for the model.\n\n**Query:**\n\n*Q2: How are the predicates reported in Table 3 defined?*\n\n**Response:**\n\nThey are defined in the datasets.\n\n## Citations\n\n[1] David Tena Cucala, Bernardo Cuenca Grau, Boris Motik, and Egor V Kostylev. On the correspondence between monotonic max-sum gnns and datalog. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, pages 459 658–667, 2023\n\n[2] David Tena Cucala, Bernardo Cuenca Grau, Egor V Kostylev, and Boris Motik. Explainable gnn based models over knowledge graphs. In International Conference on Learning Representations, 452 2021.\n\n[3] Matthew Morris, David Tena Cucala, Bernardo Cuenca Grau, and Ian Horrocks. Relational graph convolutional networks do not learn sound rules. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 21, pages 897–908, 2024.\n\n[4] Köhler, Dominik, and Stefan Heindorf. \"Utilizing Description Logics for Global Explanations of Heterogeneous Graph Neural Networks.\" CoRR (2024).\n\n[5] Pluska, Alexander, et al. \"Logical distillation of graph neural networks.\" Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning. 2024."}]

Author rebuttal:

Meta-review: Reviewers generally appreciated the solid formal analysis but lamented the limited potential impact of the results, which are restricted to a subclass of GNN architectures. The authors reply to reviewer 1gqb does address this specific point, however its effects did not propagate to the other reviewers. More generally, the author-reviewer discussion was useful in that it did have a moderate impact on the reviewer's opinion of the paper.

Keeping all of this into consideration, I am moderately positive about the contribution: notational issues aside, it is clean and also sufficiently interesting/impactful for GNN research.
Decision: Accept (poster)