Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sound Logical Explanations for Mean Aggregation Graph Neural Networks

Matthew Morris, Ian Horrocks

TL;DR

This work addresses the explainability of mean-aggregation GNNs (MAGNNs) for knowledge-graph completion by restricting to MAGNNs with non-negative weights to isolate monotonic behavior. It formalizes soundness notions, proves that only a very limited class of monotonic rules can be sound for MAGNNs, and provides a finite, testable ELUQ rule set that captures these rules; it also introduces a restricted fragment of first-order logic (Omega) to generate sound explanations for any MAGNN prediction. Empirically, non-negative MAGNNs maintain competitive performance across standard benchmarks, while enabling the extraction of sound, human-interpretable rules and explanations, and revealing issues in learned models via nonsensical rules. The results underscore both the value of explainability in neuro-symbolic KG methods and the need for careful rule extraction, suggesting that max/sum variants may offer different explainability guarantees and that MAGNNs can be a practical component when interpretability is prioritized.

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 Aggregation Graph Neural Networks

TL;DR

This work addresses the explainability of mean-aggregation GNNs (MAGNNs) for knowledge-graph completion by restricting to MAGNNs with non-negative weights to isolate monotonic behavior. It formalizes soundness notions, proves that only a very limited class of monotonic rules can be sound for MAGNNs, and provides a finite, testable ELUQ rule set that captures these rules; it also introduces a restricted fragment of first-order logic (Omega) to generate sound explanations for any MAGNN prediction. Empirically, non-negative MAGNNs maintain competitive performance across standard benchmarks, while enabling the extraction of sound, human-interpretable rules and explanations, and revealing issues in learned models via nonsensical rules. The results underscore both the value of explainability in neuro-symbolic KG methods and the need for careful rule extraction, suggesting that max/sum variants may offer different explainability guarantees and that MAGNNs can be a practical component when interpretability is prioritized.

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.

Paper Structure

This paper contains 35 sections, 9 theorems, 11 equations, 10 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Our Contribution
  3. Background
  4. Datasets and Graphs
  5. FOL Rules
  6. Graph Neural Networks
  7. Dataset Transformations Through GNNs
  8. Soundness and Subsumption
  9. Sound Rules and Explanations
  10. Which Monotonic Rules can be Sound for MAGNNs
  11. Checking for Monotonic Rule Soundness
  12. Consequences for Link Prediction
  13. Explaining MAGNN Predictions
  14. Logic Language Needed
  15. Explanatory Rule
  16. ...and 20 more sections

Key Result

Proposition 1

There exists a MAGNN $\mathcal{M}$ such that for any dataset $D$ and constant $a \in \texttt{con}(D)$, $U(a) \in T_\mathcal{M}(D)$ if and only at least half of the neighbours $b$ of $a$ in $D$ are such that $U(b) \in D$, where $U$ is a unary predicate. This logical function cannot be defined in FOL

Theorems & Definitions (19)

  • Proposition 1
  • Definition 2
  • Theorem 3
  • proof : Proof sketch
  • Proposition 4
  • proof : Proof sketch
  • Definition 5
  • Theorem 6
  • proof : Proof sketch
  • Proposition
  • ...and 9 more