Source-linked AI summary

Beyond Trained Models: Compiling GNNs for a Sound Explainer Benchmark

Steve Azzolin, Francesco Paolo Nerini, Stefano Teso, Francesco Bonchi, Bruno Lepri, André Panisson, Andrea Passerini

arXiv:2610.03526v1cs.LGcs.AI

TL;DR

Plausibility evaluation assumes that a trained GNN relies on the intended pattern, an assumption that can fail on popular benchmarks. The paper replaces training with compilation and uses prime implicants to define exact ground truth explanations. Across tasks, only a few explainers consistently avoid chance-level performance, while indirect influences expose trade-offs for others.

  • Problem

    Plausibility evaluation compares explanations with a predefined pattern, but it assumes the trained GNN actually relies on that pattern.

    Source: §1 · p. 1
  • Method

    The paper compiles graded modal logic formulas into behaviour-equivalent GNNs and defines ground truth as the union of all prime implicants, computed using the symbolic representation.

    Source: §1 · p. 2, §4.1 · p. 4, §4.3 · p. 5
  • Results

    FLOWX, GRAPHSVX, and IG are the only explainers that never fall to chance level across six tasks.

    Source: §5.2.2 · p. 8
  • Takeaways & Limitations

    GracrBench provides a rigorous testbed for evaluating explainers against compiled GNNs with known behaviour.

    Source: §6 · p. 9

    Compiled GNNs use binary embeddings and noiseless aggregations, so evaluations should be treated as a minimum bar rather than a proxy for in-production evaluation.

    Source: §6 · p. 9

Abstract

from arXiv · show

Explainers for Graph Neural Networks (GNNs) are commonly evaluated by their plausibility, i.e., how well their explanations recover a predefined ground truth, such as a motif planted in the data. This protocol implicitly assumes that a GNN trained on such data relies on the intended motif. Although prior work has questioned this assumption, plausibility remains widespread. First, we show that the assumption is violated on several widely used benchmarks, where, e.g., degree statistics alone suffice to solve the task. Then, we remove this confounder by replacing training with compilation. We achieve this by introducing $\mathsf{Gracr}$, the first compiler translating graded modal logic formulas into GNN weights, yielding models that replicate the behaviour of the corresponding formulas. Since the behaviour of the model is now known by construction, we can define its ground truth explanation formally and compute it exactly. Building on this, we introduce $\mathsf{Gracr}\mathsf{Bench}$, a benchmark of compiled GNNs for the evaluation of explainers against this exact ground truth. Experiments on eleven explainers across six tasks show its effectiveness for fine-grained diagnostic evaluation: notably, we discover that most explainers are not robust to indirect influences or alternative implementations of the same formula. These results position $\mathsf{Gracr}\mathsf{Bench}$ as a novel, rigorous evaluation setting for graph post-hoc explainability.

1 Introduction

Plausibility evaluates whether an explainer recovers a predefined ground-truth pattern, but this assumes the trained GNN actually uses that pattern. The paper replaces training with compilation to control model behaviour and support a more principled plausibility benchmark.

1 Introduction

  • Plausibility measures how well an explanation recovers a predefined discriminative pattern, such as a planted graph motif.The standard protocol trains a GNN on data with a known pattern, then checks whether its explanation recovers that pattern.Source: §1 · p. 1
  • Roughly 25% of the 155 surveyed papers use plausibility as their only explanation-evaluation criterion.Plausibility was used alone in at least 20% of papers in every surveyed year.Source: §1 · p. 1, Figure 1 · p. 2
  • A trained GNN may use spurious patterns instead of the intended discriminative pattern, making plausibility scores misleading.A well-behaved explainer that reports the model’s actual alternative rationale can be penalized in favour of one that reports the intended pattern.Source: §1 · pp. 1–2
  • Popular benchmarks may not reliably test plausibility because the evaluated GNN may not behave as expected.The proposed compiler translates logic formulas into GNN weights, yielding models with known, controllable behaviour.Source: §1 · p. 2
  • The paper adopts prime implicants as ground truth explanations and develops an efficient procedure to extract them.Its ground truth is the union of all prime implicants, accommodating multiple minimal subgraphs that suffice for a prediction.Source: §1 · p. 2
  • Experiments use the compiler to build a sound plausibility benchmark that exposes explainer limitations beyond motif-based tasks.The benchmark recovers previously known findings and uncovers new ones in understudied scenarios.Source: §1 · p. 2

2 Background

The paper frames plausibility as comparing an explainer’s edge-importance scores with a binary ground-truth mask. Its example shows why that score can mislead when a trained model relies on a different pattern than the intended one.

2 Background

  • A graph explainer maps a classifier and graph to edge-importance scores, while the ground truth is a binary edge mask.For node classification, the explainer also receives the node being explained.Source: §2 · p. 2
  • A plausibility score compares the predicted explanation with the selected ground-truth mask, so the choice of mask matters.Accuracy and its variants are examples of such scoring functions.Source: §2 · p. 2
  • In the Mutagenicity example, removing the intended NO2 pattern leaves the prediction unchanged, suggesting the model uses an alternative pattern.An explainer that reports that alternative can be penalized in favour of one that reports the intended pattern.Source: Figure 2 · p. 3

3 Issues with previous evaluations of plausibility

The usual plausibility protocol treats a dataset’s discriminative pattern as the trained GNN’s explanation ground truth. The paper argues this assumption can fail on popular benchmarks and motivates evaluating models whose behaviour is controlled by construction.

3 Issues with previous evaluations of plausibility

  • The standard protocol treats a known dataset pattern as ground truth, then scores explanations against it.For Mutagenicity, the NO2 group is commonly used as the ground-truth explanation for the class distinction.Source: §3 · p. 3
  • The protocol assumes that a high-accuracy GNN learns only the known discriminative pattern.Machine-learning models can instead learn shortcuts, making plausibility misleading when the assumption fails.Source: §3 · p. 3
  • Removing the intended NO2 pattern often leaves a trained model’s prediction unchanged, suggesting it learned an alternative pattern.A well-behaved explainer that reports the alternative can then be penalized in favour of one reporting the intended pattern.Source: §3 · p. 3
  • BaShapes and BaMultiShapes can be solved using average node degrees rather than their intended motifs.On Benzene, AlkaneCarbonyl, and FluorideCarbonyl, GNNs consistently fail to learn the specified patterns exactly and resort to spurious correlations.Source: §3 · p. 3
  • Dataset design alone cannot guarantee that a trained GNN implements a uniquely identified behaviour, and verifying its behaviour afterward may be as hard as explaining it.The authors therefore provide guarantees on the model itself rather than relying on better-designed datasets.Source: §3 · pp. 3–4
  • Faithfulness metrics also have limitations: definitions vary, metrics can conflict, and some are validated against human-defined explanations.The authors leave testing faithfulness metrics in their proposed setting to future work.Source: §3 · p. 4
  • The paper addresses the plausibility confound by replacing GNN training with compilation, producing models whose behaviour is known by construction.This makes it possible to study effects that are confounded in trained models in controlled experiments.Source: §3 · pp. 3–4

4 From logic formulas to ground truth explanations

The paper compiles graded modal logic classifiers into GNNs with known behaviour, then defines ground truth explanations as the union of all prime implicants. It uses ROBDD-based computation to extract that ground truth for compiled models.

4.1 Gracr: Compiling a logic formula into a GNN

  • Gracr compiles a target logic classifier into a message-passing GNN that agrees with the formula on every graph.The construction extends prior constructive expressiveness results to graph-level tasks.Source: §4.1 · p. 4
  • The compiled classifier fragment uses node colours as atomic predicates and graded modalities to test how many neighbours satisfy a formula.Node classifiers evaluate a formula at each node, while graph classifiers count nodes satisfying a predicate.Source: §4.1 · p. 4
  • The compiler uses an aggregate-combine GNN with sum aggregation and truncated ReLU activations.Every graded modal logic classifier is captured by this architecture.Source: §4.1 · p. 4
  • The compiler encodes each formula subexpression in a hidden coordinate, maintaining its truth value across successive layers.After the final layer, a node classifier reads the formula coordinate; graph classifiers sum-pool node values and threshold the count.Source: §4.1 · p. 4

4.2 Defining ground truth explanations formally

  • A prime implicant is a minimal subgraph sufficient to preserve the classifier’s prediction across all its extensions within the input graph.Prime implicants need not be unique, so the ground-truth explanation is their union.Source: §4.2 · p. 5
  • The union of prime implicants accommodates alternative explanations and recovers implanted motifs in motif-based graph tasks.The paper motivates prime implicants as a rigorous target that applies beyond task-specific motif heuristics.Source: §4.2 · p. 5

4.3 Computing UPI for a compiled GNN

  • The UPI algorithm uses ROBDDs to compute prime-implicant ground truth from the symbolic formula, avoiding black-box model queries.Computing prime implicants is generally hard because candidate explanations must be checked against every extension; the compiled representation supplies the symbolic function.Source: §4.3 · pp. 5–6
  • UPI extraction encodes each graph edge as a Boolean variable, extends the classifier to identify sufficient subgraphs, then marks edges belonging to at least one prime implicant.An edge is included when a sufficient set containing it ceases to be sufficient upon its removal; the authors report negligible runtime for their algorithm relative to evaluated explainers.Source: §4.3 · p. 6

5 GracrBench: Benchmarking explainers on compiled GNNs

GracrBench evaluates explainers on GNNs compiled from formulas, whose behavior and exact ground-truth explanations are known. Across six tasks, only FLOWX, GRAPHSVX, and IG avoid chance-level performance; results also expose sensitivity to formula implementations and indirect influences.

5 GracrBench: Benchmarking explainers on compiled GNNs

  • The benchmark compiles formulas into GNNs without training, computes UPI ground truth, and scores eleven explainers using precision and recall.It covers three graph-classification tasks and three node-classification tasks, including one-hop and recursive two-hop majority rules.Source: §5 · p. 7, §5.1 · p. 7

5.2.1 Recovering existing insights

  • On Redundancy, GNNEXPLAINER achieves perfect recall across a wide range of L1 strengths, highlighting all alternative explanations rather than a sparse subset.This contradicts the expected sparsification and matches findings previously observed empirically [Funke et al., 2022] and explained theoretically [He et al., 2025].Source: §5.2.1 · p. 7
  • On RedBlueLeaf, DECONV can assign spurious relevance to irrelevant-by-design edges, and recolouring background nodes can vary its precision.This recovers the finding that DECONV can be insensitive to what the model actually computes [Nie et al., 2018].Source: §5.2.1 · p. 8

5.2.2 Uncovering new limitations of explainers

  • Only FLOWX, GRAPHSVX, and IG never fall to chance across tasks; FLOWX maintains F1 ≥0.92 on all six tasks, while IG never falls below 0.96 precision.On motif-based tasks alone, SALIENCY, LRP, and GNNEXPLAINER perform on par with FLOWX and IG; differences emerge in settings beyond familiar motifs.Source: §5.2 · p. 7, §5.2.2 · p. 8, Table 2 · p. 8
  • Only IG, FLOWX, and GRAPHSVX maintain consistent performance across equivalent task formulations; several other explainers fall to chance on CompetingRedundancy.The discrepancy is associated with the original implementation of the “∨” operator, which introduces double negations through De Morgan’s laws; similar effects occur with other formula rewritings.Source: §5.2.2 · p. 8
  • On Majority2Hop, GNNEXPLAINER, DECONV, and FLOWX reach recall ≥0.95 at the expense of precision, while most gradient methods miss indirect multi-hop effects.Except for DECONV and IG, gradient-based explainers maintain precision >0.9 at the expense of recall; missing edges can alter an intermediate grey node and thereby affect the target prediction.Source: §5.2.2 · pp. 8–9

6 Conclusion

The paper introduces Gracr and GracrBench to address plausibility evaluations where trained GNNs may not behave as expected, using compiled models and exact prime-implicant explanations. The approach supports fine-grained analysis, but compiled models use binary embeddings and noiseless aggregations and should not be treated as proxies for in-production evaluations.

6 Conclusion

  • GracrBench evaluates explainers on compiled GNNs against exact ground truth defined as the union of all prime implicants, enabling sound, fine-grained analysis.The paper describes Gracr as the first compiler translating graded modal logic sentences into GNN weights and reports an exact, efficient prime-implicant extraction algorithm.Source: §6 · p. 9
  • Compiled GNNs use binary embeddings and noiseless aggregations, so evaluations should be treated as a minimum bar rather than a proxy for in-production performance.The current implementation is also restricted to binary classification and categorical node features.Source: §6 · p. 9
  • The benchmark currently tests popular instance-level explainers; extending it to counterfactual and model-level explainers remains future work.Making compiled models more realistic through fine-tuning is challenging because fine-tuning may invalidate guarantees, and preserving expected behavior remains future work.Source: §6 · p. 9

A Extended related work

  • Unlike related white-box GNN approaches, Gracr compiles general graded modal logic formulas and automatically extracts exact, complete UPI explanations for node and graph tasks.The paper contrasts this with approaches targeting only node features or using manual ground-truth edge derivations that miss indirect influences.Source: A Extended related work · p. 17

B Analyses of popular datasets for evaluating plausibility

  • The dataset analysis examines alternative solutions and whether trained GNNs may fail to implement intended ground truth, covering 74 of 94 plausibility-related papers considered.For motif datasets, alignment between model behavior and intended ground truth is possible only when models achieve nearly perfect accuracy.Source: B Analyses of popular datasets for… · p. 17

B.1 Synthetic datasets

The synthetic-dataset analysis tests whether alternative shortcuts can solve tasks intended to depend on motifs. It finds degree-based shortcuts in BaShapes and BaMultiShapes, and evidence of unexpected model behavior in Tree-Cycles and Tree-Grid.

B.1 Synthetic datasets

  • The analysis explicitly checks synthetic motif datasets for valid alternative explanations that could invalidate the intended ground-truth assumption.It uses GIN, described as a provably powerful GNN, and focuses on novel shortcuts after noting previously reported alternatives in Ba2Motif, Grid, and GridHouse [Fontanesi et al., 2024].Source: §B.1 · p. 17
  • BaShapes classes are separable by node degrees: classes 0 and 1 by degree, and classes 2 and 3 by average neighbour degree.A 2-layer GIN reaches 100% accuracy even though the implanted house-like motif requires three hops to cover all its edges.Source: §B.1 · pp. 17–18, Figure 6 · p. 18
  • BaMultiShapes classes can be perfectly separated using average graph node degree; a 1-layer GIN reaches 100% test accuracy.This provides an alternative solution to the intended motif task and a counterexample to Assumption 1.Source: §B.1 · p. 18, Figure 7 · p. 18
  • On Tree-Cycles, no tested GIN configuration robustly reaches 100% test accuracy across seeds, and background-tree perturbations can change predictions for cycle nodes.The only 4-layer GIN reaching 100% test accuracy did so on only a few seeds, and still attended to information outside the intended motif.Source: §B.1 · p. 18, Figure 8 · p. 19, Table 4 · p. 19
  • On Tree-Grid, 3-layer GINs perform best despite a receptive field too small to cover the full motif, and removing outside edges flips some target predictions.These observations suggest the model may be using a shortcut rather than the intended 3 × 3 grid.Source: §B.1 · p. 19, Table 5 · p. 19

B.2 Molecular datasets

Tests on four molecular datasets find that trained GNNs often fail to reach near-perfect accuracy on intended motifs, while compilation examples illustrate how formulas and derived connectives are represented in GNNs.

B.2 Molecular datasets

  • Almost no model–dataset pairs reached near-perfect accuracy; no GNN reached perfect performance on FluorideCarbonyl or AlkaneCarbonyl despite fully discriminative motifs and no label noise.The four datasets are Mutagenicity, Benzene, AlkaneCarbonyl, and FluorideCarbonyl, with motifs including NO2 or NH2 groups and dataset-specific chemical substructures.Source: §B.2 · pp. 19–21
  • After NO2 or NH2 removal, more than half of perturbed mutagenic graphs retained their prediction, indicating these groups are not the exclusive prediction factors.The analysis suggests NH2 is a spurious signal, whereas NO2 is one of multiple possible drivers of mutagenicity.Source: §B.2 · p. 21
  • PNA achieved perfect Benzene classification using edge features; without them, GNNs rely on signals outside the aromatic-ring motif, so even ≥0.90 accuracy does not establish alignment.Aromaticity is encoded via edge features because hydrogen atoms are not explicitly represented.Source: §B.2 · p. 21

C.1 Practical example of a compiled GNN

  • The example formula for a red node with at least two blue neighbours compiles to a width-4, two-layer GNN that returns true exactly for that condition.The formula is Φ(u) = red(u) ∧ ♢≥2 blue.Source: §C.1 · p. 21

C.2 Desugaring the derived connectives

  • Derived connectives are rewritten using the core operators, including upper-bound and exact-count modalities expressed with graded-diamond negations.The passage gives separate rewrites for ≤n, =n, and interval counts.Source: §C.2 · p. 22
  • The comparative neighbour-count operator uses a bound n; flat gates compile it to depth 4 regardless of n, rather than the 3n depth of binary disjunctions.In the datasets, n is the maximum degree, and the thresholds are absorbed into layer width.Source: §C.2 · p. 22

C.3 Ablation on comparative operator implementation

The ablations show that explainer outcomes can vary across compiled implementations even when the task is logically equivalent. The appendix details how ROBDDs encode these functions and how the BUILD procedures construct them.

C.3 Ablation on comparative operator implementation

  • Most explainers are unaffected by the comparative-operator change, but SALIENCY and LRP are noticeably affected by its negative gradients.SALIENCY’s absolute gradients can assign high importance to edges with large negative gradients; LRP can produce false positives through compounded relevance.Source: §C.3 · p. 22, Table 8 · p. 23

C.4 Keeping the backward pass of a compiled model informative

  • IG’s two backward passes yield identical scores on five of six tasks; on Majority2Hop, F1 is 0.92 with the surrogate gradient versus 0.97 with the original.IG retains the exact gradient to avoid potentially violating its Completeness axiom; the forward pass remains untouched for the other explainers.Source: §C.4 · p. 23, Table 9 · p. 24

C.5 Ablating how the formula is written

  • Five explainers (SALIENCY, DECONV, GUIDEDBP, GNNEXPLAINER, and LRP) move from random-level to perfect performance under flat-disjunction compilation.The De Morgan implementation places negations on paths to branches, blocking gradient flow under the surrogate backward pass; the flat gate contains no negation.Source: §C.5 · p. 24, Table 10 · p. 25
  • On RedBlueLeaf, SALIENCY, GUIDEDBP, and LRP fall to chance under the deeper equivalent formula; IG, GRAPHSVX, and GNNEXPLAINER remain unaffected, while FLOWX times out.The graphs, labels, and UPI are identical across the two formulas; only the compiled GNN changes.Source: Table 11 · p. 25, §C.5 · p. 25

D.1 Definition of ROBDDs and a practical example

  • ROBDDs encode formula truth over graph substructures for efficient UPI extraction; in the path example, the minimal edge cover is {e1, e3}.Figure 10 shows the path graph and the ROBDD for its edge-cover function.Source: §D.1 · p. 26, Figure 10 · p. 26

D.2 The BUILD algorithm for ROBDDs

  • BUILDNODE recursively combines subformula ROBDDs; for counting modalities it tracks whether each incident edge exists and its neighbour satisfies the subformula.The returned counting function is true exactly when at least N neighbours satisfy that subformula.Source: §D.2 · p. 27

D.3 Unrolling the recursive rule in Algorithm 2

  • Unrolling Algorithm 2’s edge-wise updates yields a conjunction over every edge subset, making the accumulated function true exactly when R is sufficient.Each update conjoins the accumulated function with a shifted copy, doubling the terms at each edge step.Source: §D.3 · pp. 27–28

D.4 Computational complexity of Algorithm 1

Algorithm 1 uses ROBDD symbolic operations to extract ground-truth explanations, with a derived operation-count bound and a separate worst-case dependence on ROBDD size. On the tested edge-cover instances, extraction substantially outpaces brute-force enumeration.

Complexity

  • Building a node-level formula's ROBDD costs O(|E| · |Φ| · Nmax) symbolic operations, with an additional O(|V|^2) term for graph-level formulas.Nmax is the largest counting threshold in Φ; |Φ| is its number of subformulas.Source: §D.4 · p. 29
  • Sufficiency extension and final edge extraction each use O(|E|) symbolic operations, giving O(|E| · |Φ| · Nmax + |V|^2) operations for one target.The bound counts symbolic operations, not their cost as a function of ROBDD size.Source: §D.4 · p. 29
  • The practical bottleneck is ROBDD size: a symbolic operation can be exponential in the number of input edges in the worst case.The tested tasks and datasets rarely reach that worst case.Source: §D.4 · p. 29

Setup

  • The timing experiment uses complete directed graphs with self-loops and an edge-cover classifier, comparing three dd ROBDD engines against exhaustive subgraph enumeration.Each engine is asserted to return the same edge mask; runs exceeding one second are not continued to larger sizes.Source: §D.4 · p. 29

Results

  • 48 seconds at N = 5 nodes makes brute force out of reach immediately after, while Algorithm 1 stays in the millisecond range through |E| = 144 edges.The ROBDD has a few tens of thousands of nodes at the largest tested size; dynamic variable reordering costs up to two orders of magnitude more than static ordering there.Source: Table 12 · p. 29, §D.4 · p. 29

D.5 Cost of the ground truth against the cost of the explainers

The authors compare ground-truth extraction time with explainer runtime across benchmark datasets. Extraction is bounded in practice, while the overall experiment runtime is largely driven by explainers.

Setup

  • The authors report extraction time for ROBDD construction, sufficiency extension, and final extraction, averaged over the first 200 instances per dataset.The measurements use one CPU core; explainer timings are averages for one explanation and include only the most expensive explainers.Source: §D.5 · p. 30

Results

  • The overall runtime of the experiments is largely dominated by the explainers.Table 14 reports per-instance explanation times by explainer and dataset; † marks explainers that did not finish every instance within the timeout.Source: §D.5 · p. 30, Table 14 · p. 30
  • 0.15 seconds is the maximum reported time for one ground-truth extraction across the benchmark datasets.This cost is paid once, after which ground-truth explanations are stored with the dataset.Source: Table 13 · p. 30, §D.5 · p. 30

E Choosing the right evaluation metric

The section argues for reporting precision and recall separately against the union of prime implicants. This preserves distinctions between recovering relevant edges and covering alternative valid explanations that scalar metrics can obscure.

Why not accuracy

  • Accuracy can reward an all-negative explanation because UPI covers only a small minority of graph edges.The constant prediction that every edge is irrelevant can score highly while conveying no information.Source: E Choosing the right evaluation metric · p. 30

Why not AUROC and PRAUC

  • An explainer returning one complete prime implicant may have arbitrarily low recall against the UPI, so PRAUC and AUROC can understate that valid explanation.The section notes that the explainer need not rank edges from alternative prime implicants above irrelevant edges.Source: E Choosing the right evaluation metric · p. 31

Why not WIoU

  • WIoU can score the same perfect edge ranking very differently as graph size grows: 0.991 at |E| = 10 versus 0.167 at |E| = 5000.The example assigns importance 1.0 to the single relevant edge and 0.001 to each other edge.Source: E Choosing the right evaluation metric · p. 31

Why the union of PIs

  • Scoring against each prime implicant separately can require storing and matching exponentially many masks, and a best-match score can reward reporting just one implicant.The authors therefore use the union of the PIs as the reference.Source: E Choosing the right evaluation metric · p. 31

Metric choice

  • Separate precision and recall measure, respectively, whether selected edges are relevant and whether the explainer covers alternative valid explanations.The union of prime implicants (UPI) is the reference mask for this evaluation.Source: E Choosing the right evaluation metric · pp. 30–31

Caveats

  • Reported F1 values may not match the displayed precision and recall because F1 is averaged sample-wise; threshold sweeping also gives optimistic metric estimates.The average of sample-wise F1 scores need not equal the F1 of averaged precision and recall.Source: E Choosing the right evaluation metric · p. 31

F Dataset details

The appendix specifies the formulas, graph constructions, and implementation protocols used to build the benchmark datasets and survey. Across these materials, tasks are defined through graded-modal predicates and controlled graph-generation choices.

F Dataset details

  • Graph-classification tasks close a node predicate with a counting quantifier, and the ordered colour palette supplies both predicate vocabulary and one-hot node features.The common graph protocol uses 1,000 graphs with class ratio 0.5 and rejection sampling to ensure annotations are unambiguous.Source: F Dataset details · p. 31
  • RedBlueLeaf uses a chain of four red nodes with two blue leaves each; its 11 motif edges form the ground-truth explanation, while green anchor edges are excluded.The formula avoids satisfying a four-core condition by backtracking between two adjacent red cores.Source: F Dataset details · pp. 31–32
  • Redundancy plants one black node with six red neighbours, making each black-red edge a valid prime implicant and their six-edge union the UPI.Five edges connect the anchor to background nodes and are irrelevant to the explanation.Source: F Dataset details · p. 32
  • CompetingRedundancy plants three complete candidate neighbour groups of sizes one, two, and three, yielding three alternative explanations and a six-edge UPI.Negative graphs fall short of each group's threshold by one member.Source: F Dataset details · p. 32
  • Node-classification tasks use Barabási–Albert graphs and collect at least 500 targets; Majority2Hop applies neighbourhood comparisons twice, expanding the receptive field to two hops.The nested predicates assign derived labels before the outer comparison, corresponding to two rounds of label propagation.Source: F Dataset details · p. 32
  • The RedBlueLeaf node-classification variant uses a three-hop predicate on a planted path of three red cores, with targets inside one unit receiving structurally different explanations.The construction plants 50 units in a 300-node background, for 750 nodes total.Source: F Dataset details · pp. 32–33

G Additional Details on the Survey

  • The literature survey is restricted to selected peer-reviewed venues and excludes non-standard explanation modalities where plausibility and faithfulness metrics do not apply meaningfully.Entries are categorized by evaluation type, paper type, model-ground-truth verification, explanation type, task, and dataset.Source: G Additional Details on the Survey · p. 33

H Implementation details

  • Explainer hyperparameters are tuned per task on held-out-seed data, with a 180-second per-instance time budget during evaluation.The tuning protocol uses 50 trials per explainer and task, each scored on 50 instances; timed-out explainers are marked OOT when no seeds finish.Source: H Implementation details · pp. 33–34, Table 16 · p. 34

H.1 Implementation details of explainers

The explainer implementations were adapted for a common edge-level evaluation setting, with changes intended not to alter their original scope or functionality.

Implementation overview

  • The implementation adjustments were made to fit the evaluation setting while preserving each explainer’s original scope and functionality.Implementations were taken from PyG except where otherwise specified.Source: §H.1 · p. 34

SubgraphX

  • SubgraphX explanations are evaluated on the full graph; edges outside its computation graph are zero-padded, and its depth is inferred from the model’s message-passing layers.The removed filter had returned only attributions within the node’s computation graph; this change does not affect execution time.Source: §H.1 · p. 34

GNNExplainer

  • GNNExplainer logits are initialized near unit message weights using a bias only at initialization, reducing count changes that can destabilize training on some datasets.A sweep over bias values on Redundancy left precision, recall, and F1 at 1.00 ± 0.00 across five seeds.Source: §H.1 · p. 34

FLOWX

  • FLOWX’s baseline implementation was modified to remove non-training operations that caused out-of-memory errors on models with more than three message-passing layers.A single-seed comparison on Majority2Hop and RedBlueLeaf-NC found no distinguishable behavior beyond a small recall rounding error on Majority2Hop; Table 17 reports mean ± standard deviation across sample nodes.Source: §H.1 · p. 35, Table 17 · p. 35

PGMExplainer

  • PGMExplainer’s node p-values are converted to edge scores as 1 − max(pu, pv), so an edge is scored only as highly as its less important endpoint.Source: §H.1 · p. 35

GRAPHSVX

  • GRAPHSVX scores each edge using the smaller absolute endpoint Shapley value and spends its coalition budget on graph structure, but equal directional scores cap precision near 50% on three tasks.The stated cap applies to Majority1Hop, Redundancy, and CompetingRedundancy; observed precision is about 56% on Majority2Hop.Source: §H.1 · p. 35
  • GRAPHSVX was adapted to sparse adjacency matrices, retaining its original coalition sampling and regression; its design cannot distinguish the two directions of an edge.The text also notes that PGMExplainer and SubgraphX share the theoretical precision cap, though both score substantially lower than GRAPHSVX in practice.Source: §H.1 · p. 35

LRP

  • LRP uses Captum’s baseline epsilon rule for every layer of the compiled models.Source: §H.1 · p. 35

I Proof of Theorem 1

The theorem characterizes an edge as belonging to the union of prime implicants exactly when a sufficient subgraph containing it becomes insufficient upon its removal. Its proof establishes both directions of this equivalence.

Theorem 1

  • An edge belongs to UPI(f, G) exactly when there is a sufficient subgraph containing that edge that becomes insufficient when the edge is removed.Source: I Proof of Theorem 1 · p. 35

Proof

  • If an edge belongs to a prime implicant, that implicant witnesses that the subgraph remains sufficient with the edge but not after its removal.Source: I Proof of Theorem 1 · pp. 35–36
  • Conversely, a witness subgraph containing the edge and becoming insufficient without it contains a smallest sufficient subgraph, which is a prime implicant that must include the edge.Source: I Proof of Theorem 1 · p. 36

Corollary 1

  • The equivalence also covers cases where UPI is empty: this occurs when removing any subset of edges leaves the prediction invariant, and the algorithm returns an empty mask.Source: I Proof of Theorem 1 · p. 36
Loading 2610.03526v1…