Automorphism-Induced Non-Canonicity in Top-k Explanations of Graph Neural Networks

# Automorphism-Induced Non-Canonicity in Top-𝑘 Explanations of Graph Neural Networks
Source: [https://arxiv.org/html/2607.26344](https://arxiv.org/html/2607.26344)
###### Abstract

A gradient\-based GNN explainer given a molecule with two chemically equivalent nitro groups assigns them attribution scores that are equal to the last bit\. It cannot do otherwise: message passing is exactly permutation equivariant, so any automorphism of the input leaves every attribution invariant\. Yet the standard report, the top\-kkedges, names one of the two, and which one is settled by the order of an array\.

We show this is a structural obstruction rather than an implementation slip\. When no minimal valid explanation is fixed by the input’s automorphism group, no rule can be single\-valued, minimal and symmetry\-respecting at once\. For the exact\-kkreports used in practice we give a parameter\-free criterion, mechanised in Lean 4 with no axiom dependencies, that decides from the graph alone whether*every*score\-optimal report of that size must split an orbit\. Across 21298 instance–budget decisions the criterion agrees with a mechanical model\-equivalence check without exception, and no severing case we found admitted a neutral alternative\.

The obstruction is common\. Nontrivial automorphisms occur in 93\.4% of Mutagenicity, the dataset the seminal explainability papers use, so the measure\-zero dismissal of symmetric inputs, sound on the continuous domains it was made for, collapses here\. At the sparsity budget those papers report, 24\.0% of molecules with two interchangeable nitro groups \(6 of 25\) surface exactly one of them, every one arbitrary under mechanical verification\. A model’s blindness also manufactures symmetry: every MUTAG molecule contains atoms chemistry separates and the network provably cannot, and a matched control shows the resolution is set by what the model reads rather than how it is parameterised\. Reporting orbits removes the arbitrariness at 0\.11 ms and 0\.43 extra edges per graph\.

## Introduction

Consider a molecule with two nitro groups in symmetric positions, and a graph neural network that predicts mutagenicity\. The two groups are interchangeable: there is an automorphism of the molecular graph carrying one onto the other\. Because message passing is permutation equivariant, the network’s output is invariant under that automorphism, and so is any attribution score computed from its outputs\. A gradient\-based explainer therefore scores the two groups*identically*, and we measure this identity to be exact rather than approximate: on the 25 molecules of this kind in MUTAG, Integrated Gradients assigns the two groups a total attribution ratio of 1\.00×\\times\.

The explanation the chemist sees is not the attribution vector\. It is a subgraph, conventionally the top\-kkedges\. And a top\-kkselection over values that are equal cannot be neutral: it must order the tied edges somehow, and common implementations inherit the order of an edge array\. Atk=10k=10, the budget bothYing et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib30)\)andLuo et al\. \([2020](https://arxiv.org/html/2607.26344#bib.bib20)\)report for molecular data, 24\.0% of these molecules have exactly one of the two equivalent groups surfaced in the reported explanation\. In 100\.0% of those cases we verify mechanically that the alternative—the same explanation carried across by the automorphism—is accepted by the model to within floating\-point tolerance\.[Figure˜1](https://arxiv.org/html/2607.26344#Sx1.F1)shows the three stages on 1,4\-dinitrobenzene, a molecule of exactly this kind\. The chemist is shown one of two answers the model cannot tell apart, and is not told there was a choice\.

#### What is and is not new here\.

The group theory is not\. That an equivariant map cannot break a symmetry of its input is Curie’s principle, stated for machine learning bySmidt, Geiger, and Miller \([2021](https://arxiv.org/html/2607.26344#bib.bib25)\)and in stabiliser form byKaba and Ravanbakhsh \([2023](https://arxiv.org/html/2607.26344#bib.bib14)\)\. The same monotonicity underlies the impossibility of continuous canonicalisation\(Dym, Lawrence, and Siegel[2024](https://arxiv.org/html/2607.26344#bib.bib10)\)and the inability of structural representations to separate automorphic nodes\(Srinivasan and Ribeiro[2020](https://arxiv.org/html/2607.26344#bib.bib26)\)\. Symmetry preservation is an axiom inSundararajan, Taly, and Yan \([2017](https://arxiv.org/html/2607.26344#bib.bib27)\), whose Theorem 1 makes Integrated Gradients the unique path method satisfying it, and equivariance of saliency and Integrated Gradients on graphs is proved byCrabbé and van der Schaar \([2023](https://arxiv.org/html/2607.26344#bib.bib7)\)\. Both halves of our starting observation are in print\. What is missing is their composition and its cost\. This literature treats equivariance as a property to achieve and sets symmetric inputs aside as negligible:Kaba and Ravanbakhsh \([2023](https://arxiv.org/html/2607.26344#bib.bib14)\)observe that inputs with a nontrivial stabiliser form a measure\-zero set, true for the continuous domains they consider\. On graphs that argument fails by a wide margin\.

#### Contributions\.

- •The obstruction\.Single\-valuedness, minimality and symmetry\-respect are jointly unachievable exactly when no minimal explanation is fixed by the input’s automorphism group\. For the exact\-kkreports used in practice we give a parameter\-free criterion, mechanised in Lean 4 with no axiom dependencies, deciding whether every score\-optimal report of that size must sever an orbit\.
- •The hierarchy, and a prediction it makes\.What the domain separates, what the model’s input separates and what its algorithm separates are nested\. The first gap puts 16\.2% of MUTAG’s edges beyond the model’s resolution, and a bond\-reading network with a matched control shows that reading an annotation is necessary for an explanation to resolve at the domain’s resolution but not sufficient\. The second gap stops at the representation: refinement classes tie what the forward pass cannot separate, yet attributions separate most of those pairs, which bounds what an expressiveness result can say about an explanation\.
- •The measurement\.Nontrivial automorphisms occur in 93\.4% of Mutagenicity \(n=4337n\{=\}4337\), the dataset the seminal explainability papers actually use, so the measure\-zero dismissal does not transfer from continuous domains to graphs\. The criterion agrees with a mechanical model\-equivalence check on all 21298 decisions we tested\. Equivariant explainers split attribution between two interchangeable functional groups in a ratio of1\.00×1\.00\\timesand still surface only one of them 24\.0% of the time\.
- •The consequences\.A stability of11is not evidence of canonicity, since resolving ties by array index attains it while orbit sampling scores 0\.8005 on outputs of identical fidelity\. Reporting orbits removes the arbitrariness at 0\.11 ms and 0\.43 extra edges\. Separately, the standard synthetic benchmarks understate the phenomenon because their generator attaches each motif through a vertex its own automorphism moves\.

![Refer to caption](https://arxiv.org/html/2607.26344v1/x1.png)Figure 1:1,4\-dinitrobenzene, a MUTAG molecule whose two nitro groups are exchanged by an automorphismσ\\sigma\. Because message passing is exactly equivariant, an equivariant explainer must score the two groups equally, and does: we measure a ratio of1\.00×1\.00\\times\(centre\)\. A top\-kkreport must nonetheless name one of them \(right\), and which one is settled by array index\. At the budget the seminal papers use this happens for 24\.0% of such molecules, and in 100\.0% of those the alternative is accepted by the model to within tolerance\.
#### Roadmap\.

[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)records that equivariance makes the relevant equalities exact\.[Proposition˜2](https://arxiv.org/html/2607.26344#Thmproposition2)places that fact in the hierarchy,[Theorem˜1](https://arxiv.org/html/2607.26344#Thmtheorem1)turns it into the impossibility, and[Proposition˜4](https://arxiv.org/html/2607.26344#Thmproposition4)decides for a given instance and budget whether the impossibility is triggered\. The results then measure the incidence, the two gaps, the stage of the pipeline at which the disparity appears, and the behaviour of the stability metric, before a final section gives the remedy and its cost\. Every number in this paper is produced by a script from the logged runs, and none is transcribed by hand\.

## Related Work

#### Symmetry of explanations\.

Crabbé and van der Schaar \([2023](https://arxiv.org/html/2607.26344#bib.bib7)\)formalise invariance and equivariance of interpretability methods, prove saliency and Integrated Gradients equivariant, and estimate violation by Monte Carlo over the full symmetric group\. We computeAut​\(G\)\\mathrm\{Aut\}\(G\)exactly withnautyand read the argument in the opposite direction: equivariance is not a goal to reach but a constraint that forces a tie\.Luong et al\. \([2024](https://arxiv.org/html/2607.26344#bib.bib21)\)observe that PGExplainer’s index\-order concatenation makes it not permutation invariant, a different defect from the degeneracy studied here, andLing et al\. \([2025](https://arxiv.org/html/2607.26344#bib.bib19)\)build an explainer for equivariant networks without establishing equivariance of the explanation itself\. Axiomatic treatments of graph attribution\(Duval and Malliaros[2021](https://arxiv.org/html/2607.26344#bib.bib9); Bui et al\.[2024](https://arxiv.org/html/2607.26344#bib.bib6)\)carry a symmetry axiom that permutes the value function or asserts equal treatment of equals, but none requiresΦ​\(π⋅G\)=π⋅Φ​\(G\)\\Phi\(\\pi\\cdot G\)=\\pi\\cdot\\Phi\(G\)\. Outside explainability the same structure is exploited rather than diagnosed:Bleukx et al\. \([2025](https://arxiv.org/html/2607.26344#bib.bib4)\)show that the image of a minimal unsatisfiable subset under a symmetry of the instance is again one, and prune enumeration with it\. Their symmetry is our obstruction, put to work\. Note that “invariant explanation” in this literature usually means domain invariance for out\-of\-distribution generalisation; we use the permutation sense throughout\.

#### Multiplicity, observed but attributed elsewhere\.

Kosan et al\. \([2024](https://arxiv.org/html/2607.26344#bib.bib17)\)report cross\-run Jaccard near0\.50\.5and note that explanations change while their quality does not, which they attribute to non\-convexity\.Agarwal et al\. \([2023](https://arxiv.org/html/2607.26344#bib.bib1)\)take the maximum over a hand\-annotated set of equally valid ground truths, motivated by semantic redundancy rather than symmetry, where our criterion generates that set fromAut​\(G\)\\mathrm\{Aut\}\(G\)instead of requiring curation\.Faber, Moghaddam, and Wattenhofer \([2021](https://arxiv.org/html/2607.26344#bib.bib11)\)identify redundant evidence as a pitfall using an example that is an automorphism\.Azzolin et al\. \([2025](https://arxiv.org/html/2607.26344#bib.bib3)\)record that a top\-kkoperator behaves unstably given equal scores and randomly permute nodes at load time, which under our account randomises which orbit representative the user sees\.

## Theory

### Preliminaries

LetG=\(V,E\)G=\(V,E\)be a finite undirected graph with a node colouringcc\(the node features\) and letffbe a message\-passing GNN with frozen weights\. We writeAut​\(G\)\\mathrm\{Aut\}\(G\)for the group of adjacency\- and colour\-preserving permutations\. An edge maskm∈ℝ\|E\|m\\in\\mathbb\{R\}^\{\|E\|\}is fed toffas edge weights, writtenf​\(G,m\)f\(G,m\)\. An automorphismσ∈Aut​\(G\)\\sigma\\in\\mathrm\{Aut\}\(G\)acts on masks by permuting coordinates along the induced edge permutationσ^\\hat\{\\sigma\}\.

###### Proposition 1\(Exact equivariance\)\.

For everyσ∈Aut​\(G\)\\sigma\\in\\mathrm\{Aut\}\(G\)and every maskmm,f​\(G,σ⋅m\)=f​\(G,m\)f\(G,\\sigma\\cdot m\)=f\(G,m\)for graph\-level readout, andf​\(G,σ⋅m\)σ​\(v\)=f​\(G,m\)vf\(G,\\sigma\\cdot m\)\_\{\\sigma\(v\)\}=f\(G,m\)\_\{v\}for node\-level readout\.

###### Proof\.

By induction on layers\. Each layer aggregates over the multiset of neighbour states, whichσ\\sigmapreserves because it preserves adjacency and colours\. Graph\-level readout is a permutation\-invariant pooling, and node\-level readout followsσ\\sigma\. ∎

The consequence we use throughout is that equality here is exact, not approximate\. Any validity criterion built fromff’s outputs—fidelity,ε\\varepsilon\-thresholded fidelity, mutual information, a Shapley value—is therefore*exactly*σ\\sigma\-invariant, since thresholding two identical numbers gives identical results\. This is stronger than the corresponding statement for tabular collinearity, where equally good alternatives must be assumed via a Rashomon set\. Here a single frozen model returns bit\-identical outputs, with no assumption beyond the architecture\. In practice on float32 we observe agreement to within one unit in the last place\. Of 884 decisions in our largest single sweep, 4 differ, all by exactly2−162^\{\-16\}\.

### A Resolution Hierarchy

Which group is the right one is not a bookkeeping choice\. Three equivalence relations on the nodes ofGGnest, and the gaps between them are the subject of this paper\. Writeu∼domvu\\sim\_\{\\mathrm\{dom\}\}vwhen some automorphism preserving*all*annotations of the domain carriesuutovv, writeu∼fvu\\sim\_\{f\}vwhen one preserving only whatffreads does, and writeu∼WLvu\\sim\_\{\\mathrm\{WL\}\}vwhenuuandvvreceive the same colour afterLLrounds of colour refinement, initialised with every input a layer consults beyond the multiset of neighbour states\.

###### Proposition 2\(Resolution hierarchy\)\.

For anLL\-layer message\-passing networkff,

∼dom⁣⊆⁣∼f⁣⊆⁣∼WL,\\sim\_\{\\mathrm\{dom\}\}\\ \\subseteq\\ \\sim\_\{f\}\\ \\subseteq\\ \\sim\_\{\\mathrm\{WL\}\},andffassigns identical representations to any pair related by∼WL\\sim\_\{\\mathrm\{WL\}\}\.

###### Proof\.

An annotation\-preserving permutation preserves in particular whatffreads, giving the first containment\. For the second, an automorphism preserves the initial colouring and, by induction on rounds, the refined one\. The final claim is the bound ofXu et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib29)\)andMorris et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib24)\)read at the node level: a layer is a function of the node’s own state and the multiset of its neighbours’, which is what one refinement round records\. ∎

The proposition stops at representations, and deliberately so\. For a pair related by an automorphism,[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)carries equality through to any attribution because a single permutation acts on the whole computation and on the perturbation coordinates at once\. Two nodes that share a colour without being automorphic admit no such permutation, and a coordinate\-level attribution can separate them even where the forward pass does not\. We measure this below rather than assume it either way\.

![Refer to caption](https://arxiv.org/html/2607.26344v1/x2.png)Figure 2:The three relations of[Proposition˜2](https://arxiv.org/html/2607.26344#Thmproposition2), coarsest outside, with a top\-kkreport sitting strictly inside all of them\. Gap 1 is resolution the model provably lacks: it is present in 100\.0% of MUTAG molecules and places 16\.2% of their edges in an orbit the domain splits\. Gap 2 is resolution the forward pass lacks but a coordinate\-level attribution can still supply, which is why only the first gap forces a tie\.Both containments are generally strict, and each strictness has a distinct meaning \([Figure˜2](https://arxiv.org/html/2607.26344#Sx3.F2)\)\. A pair tied under∼f\\sim\_\{f\}but separated under∼dom\\sim\_\{\\mathrm\{dom\}\}we call a*manufactured*tie: the model cannot tell the two apart, though the domain can\. Our GCN reads node features and adjacency but not bond types, so a permutation exchanging the two oxygens of a nitro group—distinguishable in Kekulé form—leaves its output untouched, verified mechanically on all 188 MUTAG molecules, where the output moves by 0 in every case\. A pair tied under∼WL\\sim\_\{\\mathrm\{WL\}\}but not under∼f\\sim\_\{f\}is an*algorithmic*tie: no automorphism relates the two, yet no network of this depth and class separates their representations\.

The consequence is the thesis of this paper\. A top\-kkreport distinguishes edges, and within a∼f\\sim\_\{f\}class the model does not: there[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)carries the equality all the way to the attribution, so a report that names one edge displays a distinction its own subject cannot make\. How far the same holds across the wider∼WL\\sim\_\{\\mathrm\{WL\}\}classes is an empirical question we answer below\.

LetValid​\(⋅\)\\mathrm\{Valid\}\(\\cdot\)be any such criterion and𝒮=\{E′⊆E:Valid​\(E′\)\}\\mathcal\{S\}=\\\{E^\{\\prime\}\\subseteq E:\\mathrm\{Valid\}\(E^\{\\prime\}\)\\\}\. By[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1),σ^​\(𝒮\)=𝒮\\hat\{\\sigma\}\(\\mathcal\{S\}\)=\\mathcal\{S\}, so the minimal elements of𝒮\\mathcal\{S\}form aσ^\\hat\{\\sigma\}\-invariant antichain\.

### The Trilemma

Call a selection ruleΦ\\Phi, mapping instances to explanation subgraphs,*neutral*ifΦ​\(σ⋅G\)=σ^​\(Φ​\(G\)\)\\Phi\(\\sigma\\cdot G\)=\\hat\{\\sigma\}\(\\Phi\(G\)\)for allσ\\sigma\.

###### Proposition 3\(No neutral selection\)\.

A neutralΦ\\Phisatisfiesσ^​\(Φ​\(G\)\)=Φ​\(G\)\\hat\{\\sigma\}\(\\Phi\(G\)\)=\\Phi\(G\)for everyσ∈Aut​\(G\)\\sigma\\in\\mathrm\{Aut\}\(G\)\(for node\-level tasks, everyσ∈Stab​\(v\)\\sigma\\in\\mathrm\{Stab\}\(v\)\)\. Hence a neutral rule exists atGGif and only if the minimal elements of𝒮\\mathcal\{S\}contain a point fixed by the whole group\.

The argument is the routine one for breaking a tie between alternatives a rule cannot distinguish, and we claim no novelty for it\. It is the graph instance ofKaba and Ravanbakhsh \([2023](https://arxiv.org/html/2607.26344#bib.bib14), Prop\. 2\.1\)\. Its content here is what it forbids\.

###### Theorem 1\(Conditional trilemma\)\.

WriteH=Aut​\(G\)H=\\mathrm\{Aut\}\(G\)and letMin\(𝒮\)H\\operatorname\{Min\}\(\\mathcal\{S\}\)^\{H\}be the set of minimal elements of𝒮\\mathcal\{S\}fixed by all ofHH\. A rule that is*\(i\)*single\-valued,*\(ii\)*minimal and*\(iii\)*neutral exists atGGif and only ifMin\(𝒮\)H≠∅\\operatorname\{Min\}\(\\mathcal\{S\}\)^\{H\}\\neq\\varnothing\. Hence when no minimal valid explanation isHH\-fixed, the three cannot hold together\.

###### Proof\.

IfΦ\\Phisatisfies all three thenΦ​\(G\)\\Phi\(G\)is minimal and, by[Proposition˜3](https://arxiv.org/html/2607.26344#Thmproposition3),HH\-fixed, soMin\(𝒮\)H\\operatorname\{Min\}\(\\mathcal\{S\}\)^\{H\}is nonempty\. Conversely, anyE∗∈Min\(𝒮\)HE^\{\\ast\}\\in\\operatorname\{Min\}\(\\mathcal\{S\}\)^\{H\}is itself such a rule’s output\. The two escapes are then as follows\. Relinquishing*\(ii\)*and reporting the orbit closureclH⁡\(E∗\)=⋃h∈Hh^​\(E∗\)\\operatorname\{cl\}\_\{H\}\(E^\{\\ast\}\)=\\bigcup\_\{h\\in H\}\\hat\{h\}\(E^\{\\ast\}\)gives anHH\-invariant set, and it lies in𝒮\\mathcal\{S\}whenever𝒮\\mathcal\{S\}is closed upwards, which is the case for sufficiency\-style criteria but not for everyValid\\mathrm\{Valid\}\. It contains disjoint sufficient subsets and so is not minimal\. Relinquishing*\(i\)*and reporting the orbit ofE∗E^\{\\ast\}satisfies*\(ii\)*and*\(iii\)*together\. ∎

TakingHHrather than a singleσ\\sigmamatters: for\|H\|\>2\|H\|\>2the setE∗∪σ^​\(E∗\)E^\{\\ast\}\\cup\\hat\{\\sigma\}\(E^\{\\ast\}\)need not be fixed by the rest of the group\.

###### Corollary 1\.

WhenMin\(𝒮\)H=∅\\operatorname\{Min\}\(\\mathcal\{S\}\)^\{H\}=\\varnothing, preserving both minimality and neutrality requires changing the*output type*of an explainer, from a subgraph to an orbit or to a distribution over minimal explanations that is equivariant underHH\.

[Corollary˜1](https://arxiv.org/html/2607.26344#Thmcorollary1)has teeth because every current fidelity, sparsity and ground\-truth metric is defined on a single mask\. Its hypothesis is not vacuous: the instances measured below are exactly those where it holds\.

### When a Report Severs an Orbit

In practice explanations are reported as top\-kkedges\. Suppose the mask isσ\\sigma\-invariant, as it must be for an equivariant explainer\. Then the edges of one*edge orbit*all carry the same value and a sort cannot tell them apart\. It can, however, interleave two distinct orbits that happen to share a value, which is why the two statements below differ\.

###### Proposition 4\(Combinatorial criterion\)\.

LetEkE\_\{k\}be the top\-kkedges under aσ\\sigma\-invariant mask\. Thenσ^​\(Ek\)=Ek\\hat\{\\sigma\}\(E\_\{k\}\)=E\_\{k\}for allσ\\sigmaif and only if the cut atkksevers no edge orbit\. Otherwise top\-kkmust choose among edges of exactly equal value, and the alternativeσ^​\(Ek\)\\hat\{\\sigma\}\(E\_\{k\}\)is, by[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1), equally valid\. We say the budget*severs*an orbit, reserving*forced*for the stronger property in[Corollary˜2](https://arxiv.org/html/2607.26344#Thmcorollary2)\.

###### Proof\.

If the cut severs no orbit thenEkE\_\{k\}is a union of complete orbits, and eachσ^\\hat\{\\sigma\}permutes every orbit onto itself, soσ^​\(Ek\)=Ek\\hat\{\\sigma\}\(E\_\{k\}\)=E\_\{k\}\. Conversely supposeσ^​\(Ek\)=Ek\\hat\{\\sigma\}\(E\_\{k\}\)=E\_\{k\}for allσ\\sigma, and letOObe an orbit with somee∈O∩Eke\\in O\\cap E\_\{k\}\. For anye′∈Oe^\{\\prime\}\\in Othere is, by definition of an orbit, aσ\\sigmawithσ^​\(e\)=e′\\hat\{\\sigma\}\(e\)=e^\{\\prime\}, and thene′∈σ^​\(Ek\)=Eke^\{\\prime\}\\in\\hat\{\\sigma\}\(E\_\{k\}\)=E\_\{k\}\. HenceO⊆EkO\\subseteq E\_\{k\}, so every orbit meetingEkE\_\{k\}lies inside it and none is severed\. ∎

[Proposition˜4](https://arxiv.org/html/2607.26344#Thmproposition4)characterises a*given*report\. Whether*every*report of that size must sever an orbit is a separate question, and the one faced when the budget is fixed\.

###### Corollary 2\(Exact\-kkreporting\)\.

Letttbe thekk\-th largest value of aσ\\sigma\-invariant mask, and split the edges intoE\>=\{e:me\>t\}E\_\{\>\}=\\\{e:m\_\{e\}\>t\\\}andE==\{e:me=t\}E\_\{=\}=\\\{e:m\_\{e\}=t\\\}, both unions of complete orbits\. A neutral, score\-optimal report of exactlykkedges exists if and only ifk−\|E\>\|k\-\|E\_\{\>\}\|is a sum of sizes of some sub\-collection of the orbits partitioningE=E\_\{=\}\. When it is not, every score\-optimal report of that size severs an orbit\.

###### Proof\.

Any score\-optimal report containsE\>E\_\{\>\}and takes the remainingk−\|E\>\|k\-\|E\_\{\>\}\|edges fromE=E\_\{=\}\. By[Proposition˜4](https://arxiv.org/html/2607.26344#Thmproposition4)it is neutral exactly when that remainder is a union of complete orbits, which is possible precisely for the stated subset sums\. ∎

The distinction is not idle: two orbits may carry the same value, in which case an index\-ordered sort can interleave and sever both where a different score\-optimal choice would have been neutral\. On MUTAG 25 molecules exhibit such cross\-orbit ties, yet of the 165 instance–budget pairs whose reported top\-kksevers an orbit, 0 admit a neutral alternative under[Corollary˜2](https://arxiv.org/html/2607.26344#Thmcorollary2)\. The severing we observe is therefore not an artefact of the implementation, a conclusion[Proposition˜4](https://arxiv.org/html/2607.26344#Thmproposition4)alone would not support\.

The criterion requires no model evaluation: orbits come from the graph, the ordering from the mask\. We mechanise exactly this argument in Lean 4, abstracted to a statement about a permutation acting on a finite set:σ^​\(S\)=S\\hat\{\\sigma\}\(S\)=Sif and only ifSSis a union of complete orbits\. The development is self\-contained, uses no library, and all three theorems discharge with*no axiom dependencies whatsoever*, not even propositional extensionality\. The criterion therefore holds unconditionally and by machine check, which is what lets us treat any disagreement with the model below as evidence about the model rather than about the criterion\.

#### Node\-level tasks\.

For a node\-level explanation ofvvthe relevant group isStab​\(v\)\\mathrm\{Stab\}\(v\), notAut​\(G\)\\mathrm\{Aut\}\(G\): aσ\\sigmamovingvvrelates*two*predictions rather than exhibiting two explanations of one, which is the equivariance studied byCrabbé and van der Schaar \([2023](https://arxiv.org/html/2607.26344#bib.bib7)\)and not the degeneracy studied here\. For anLL\-layer network only automorphisms acting inside theLL\-hop receptive field ofvvcan change the explanation\. Both restrictions are applied to the synthetic figures in[Table˜1](https://arxiv.org/html/2607.26344#Sx5.T1), and without the second the numbers would be far larger and largely vacuous: the tree underlying Tree\-Grid has an automorphism group of order exceeding105010^\{50\}, almost all of which permutes undecorated subtrees no explanation can reach\.

## Experimental Setup

We explain three\-layer GCNs\(Kipf and Welling[2017](https://arxiv.org/html/2607.26344#bib.bib16)\)on MUTAG\(Debnath et al\.[1991](https://arxiv.org/html/2607.26344#bib.bib8)\)and the datasets of[Table˜1](https://arxiv.org/html/2607.26344#Sx5.T1)with sum pooling, trained to convergence on each dataset\. Explanations of a model that has not learned the task are meaningless, so we report training accuracy alongside every measurement and discard any configuration below0\.70\.7\. Automorphism groups are computed exactly withnauty\(McKay and Piperno[2014](https://arxiv.org/html/2607.26344#bib.bib22)\)throughpynauty, with vertices coloured by their complete feature vector\. Explainers are taken from PyTorch Geometric\(Fey and Lenssen[2019](https://arxiv.org/html/2607.26344#bib.bib12)\): GNNExplainer, PGExplainer, and the Captum family \(Saliency, Integrated Gradients, Input×\\timesGradient, Guided Backpropagation, Deconvolution\), seven in all\. All experiments run on CPU in minutes: no GPU is required at any point, and the whole suite completes on one laptop core \(Apple M1 Pro, 16 GB, macOS 26\.5, PyTorch 2\.13, PyTorch Geometric 2\.8, Captum 0\.9,pynauty2\.8\.8; the code release pins every version\)\.

Hyperparameters were not tuned for performance, only until the model fit the task: hidden width6464, Adam at0\.010\.01, and the epoch count raised from6060to300300with dataset size until training accuracy cleared the floor\. The bond\-reading network is a three\-layer GINE of the same width, trained identically except on Mutagenicity, where0\.010\.01does not converge and we use0\.0030\.003\. Explainer hyperparameters are the library defaults throughout \(100100–150150optimisation epochs for GNNExplainer\), since the phenomenon is a property of the reporting step rather than of tuning\. Every measurement over seeds setstorchandnumpyseeds before each explainer call and reports the number of runs: eight per instance for the stability comparison, six for the cross\-seed decomposition, one for the deterministic sweeps\.

Two implementation details matter\. Each explainer gets a*fresh copy*of the model from a shared state dictionary, because GNNExplainer installs edge masks on the message\-passing modules and leaves them there, silently disabling the gradient path the Captum explainers differentiate through\. And colouring vertices byargmaxof the feature vector, adequate for the one\-hot encodings of MUTAG and PROTEINS, is wrong for BBBP whose features are mixed integer descriptors, where it yields spurious automorphisms that do not preserve the model’s input; we colour by the entire vector\. Directed edge masks are folded onto undirected edges by summing the two orientations before any top\-kk\.

## Results

### Incidence of Relevant Symmetry

Table 1:Instances admitting a nontrivial automorphism relevant to the explained prediction, withn=4337n\{=\}4337,188188,250250,250250for the real datasets\(Kazius, McGuire, and Bursi[2005](https://arxiv.org/html/2607.26344#bib.bib15); Debnath et al\.[1991](https://arxiv.org/html/2607.26344#bib.bib8); Borgwardt et al\.[2005](https://arxiv.org/html/2607.26344#bib.bib5); Wu et al\.[2018](https://arxiv.org/html/2607.26344#bib.bib28)\), the first three via TUDataset\(Morris et al\.[2020](https://arxiv.org/html/2607.26344#bib.bib23)\)and the synthetic generators fromYing et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib30)\)\. Synthetic figures are restricted to the33\-hop receptive field of the explained node\.[Table˜1](https://arxiv.org/html/2607.26344#Sx5.T1)reports incidence, and two points deserve emphasis\. First, Mutagenicity is the dataset the seminal explainability papers actually use:Ying et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib30)\)describe theirs as “a dataset of 4,337 molecule graphs”, and the average of 30\.32 nodes we measure matches the table inLuo et al\. \([2020](https://arxiv.org/html/2607.26344#bib.bib20)\)\. It is not the 188\-graph MUTAG of TUDataset, the two are frequently conflated, and we report both\. Second, the figures bear on the premise by which symmetric inputs are set aside:Kaba and Ravanbakhsh \([2023](https://arxiv.org/html/2607.26344#bib.bib14)\)dismiss them as measure zero, which holds on the continuous domains they consider and does not transfer to molecular graphs, where they are the overwhelming majority\.Lawrence et al\. \([2025](https://arxiv.org/html/2607.26344#bib.bib18)\)note in passing that small graphs are especially likely to carry nontrivial automorphisms, and[Table˜1](https://arxiv.org/html/2607.26344#Sx5.T1)quantifies it\.

#### Validation of the criterion\.

On Tree\-Grid the predicted rate alternates sharply withkk, falling to zero for Integrated Gradients at every budget whose cut consumes whole orbits and rising to the maximum in between, all from the graph alone\. We check this against a mechanical ground truth: form the top\-kkset, form its image under each automorphism, feed both to the frozen model as hard masks, and compare outputs\. Across 9312 decisions on MUTAG, PROTEINS and BBBP with four explainers, 3594 on Mutagenicity with three, and 1624 on synthetic benchmarks, the criterion agrees with the mechanical check on 14530 of 14530 decisions, with no false positives or negatives\. Under an absolute rather than relative tolerance the figure is 99\.83%, the discrepant cases differing by one float32 unit in the last place\.

#### An accident in the benchmarks\.

The generator ofYing et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib30)\)attaches each motif through the motif’s*first*node, which for the house motif is one of the two its only nontrivial automorphism moves, so attaching there destroys the symmetry: we measure zero symmetric instances in BA\-Shapes and in the house half of BA\-2Motifs, and re\-attaching through the roof apex restores\|Aut\|=2\|\\mathrm\{Aut\}\|=2\. The community’s most\-used synthetic benchmarks understate the phenomenon by construction, and did so by accident\.

### Two Gaps in Resolution

Table 2:MUTAG\. First column: percentage of pairs the GCN cannot separate\. Last two: percentage that network*can*\. GINE\-const is the same architecture with bond features replaced by a constant, so it differs from GINE in the information alone, not the parameterisation\. On this dataset GINE separates the manufactured pairs and ties the intrinsic ones, recovering∼GINE⁣=⁣∼dom\\sim\_\{\\text\{GINE\}\}=\\sim\_\{\\mathrm\{dom\}\}in both directions\. Mutagenicity, below, behaves differently\.#### The first gap is pervasive\.

Every MUTAG molecule contains at least one manufactured pair, and the index\[∼f:∼dom\]\[\\sim\_\{f\}:\\sim\_\{\\mathrm\{dom\}\}\]counting the symmetry the model’s blindness invents averages 3\.32 and reaches 16\. On average 16\.2% of a molecule’s edges lie in an orbit the domain splits, rising to 90\.9%\. Those edges are related by an automorphism of what the model reads, so[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)obliges any equivariant explainer to score them equally, and naming one of them displays a distinction the explainer’s own subject cannot make\.

Explaining a network that*does*read bond types tests this, and separates a necessary claim from a sufficient one\. The necessary half is provable and holds throughout: a bond\-blind network cannot separate a manufactured pair, and does not, on 100\.0% of MUTAG and 100\.0% of Mutagenicity pairs\. A matched control isolates the cause, since the same GINE\(Hu et al\.[2020](https://arxiv.org/html/2607.26344#bib.bib13)\)with bond features held constant separates 0\.0%, exactly like the GCN\. What sets the resolution is what the model reads, not how it is parameterised\.

The sufficient half is where the interesting variation lies\. On MUTAG a GINE trained to 0\.968 separates 99\.7% of manufactured pairs and 0\.0% of intrinsic ones \([Table˜2](https://arxiv.org/html/2607.26344#Sx5.T2)\), recovering∼GINE⁣=⁣∼dom\\sim\_\{\\text\{GINE\}\}=\\sim\_\{\\mathrm\{dom\}\}in both directions\. On Mutagenicity the same construction at 0\.831 separates 13\.9%, and the dataset accounts for the difference: it carries three bond types with 82\.8% of the mass on one against MUTAG’s four, and a correspondingly smaller gap, index 1\.74 against 3\.32\. Reading an annotation is therefore necessary for an explanation to resolve at the domain’s resolution but not sufficient, because the task must also reward using it\. This is the more useful conclusion of the two\. Over\-resolution cannot be repaired by enriching a model’s input, and the resolution at which a given trained model actually operates is an empirical quantity that the procedure above measures in one pass\.

#### The second gap stops at the representation\.

Automorphism orbits are contained in, and generally strictly smaller than, colour\-refinement classes: on MUTAG the classes are strictly coarser for 45\.2% of molecules, adding 325 node pairs that no automorphism relates to the 731 that one does, all of which receive GCN representations agreeing to within one unit in the last place\. It is tempting to read these as further forced ties\. They are not\. Saliency assigns equal scores to 57\.9% of them and Integrated Gradients to 20\.0%, against 100\.0% and 100\.0% on the automorphic pairs used as a positive control\. A coordinate\-level attribution separates what the forward pass cannot, because the gradient at an edge depends on every path through it and not only on the endpoint states\. Equal representations are therefore necessary for an attribution tie and not sufficient: an expressiveness bound alone licenses no claim about explanations, and the counts in[Table˜1](https://arxiv.org/html/2607.26344#Sx5.T1)should be read as automorphism\-induced ties only\.

Matching the refinement to the architecture still matters for the representation claim\. A GCN normalises by\(d~i​d~j\)−1/2\(\\tilde\{d\}\_\{i\}\\tilde\{d\}\_\{j\}\)^\{\-1/2\}, so a layer consults its neighbours’ degrees and is not a function of the neighbour multiset alone, and refinement initialised without degree is too coarse to bound it: under that mismatched calibration only 42\.5% of the supposedly tied pairs are tied, with discrepancies up to1\.1×10−21\.1\\times 10^\{\-2\}\. The signature of a correctly matched bound is agreement at the last bit\.

### Attribution versus Reporting

Table 3:The 25 MUTAG molecules whose two nitro groups are exchanged by an automorphism, atk=10k=10\. Equivariant explainers split attribution exactly evenly between the two groups and still surface only one of them a quarter of the time\. Every such case is verified arbitrary: the automorphic alternative is accepted by the model within tolerance in 100\.0% of them\.The sharpest form of the problem is visible on the 25 MUTAG molecules carrying two nitro groups exchanged by an automorphism \([Table˜3](https://arxiv.org/html/2607.26344#Sx5.T3)\)\. For the exactly equivariant explainers the total attribution assigned to the two groups has ratio 1\.00×\\times: the attribution stage is scrupulously even\-handed\. Yet atk=10k=10, 24\.0% of these molecules have exactly one group present in the reported subgraph, and in 100\.0% of those cases the automorphic alternative is accepted by the model within tolerance\. The disparity is manufactured wholly by the reporting step\.

GNNExplainer optimises a mask rather than differentiating one, so it is not exactly equivariant, and it assigns the two groups ratios up to 2\.93×\\times\. Its most extreme case is molecule 80\. There two chemically equivalent nitro groups receive 3\.515 and 1\.198, while the model’s outputs on the two corresponding subgraphs are identical to the last bit\. Across all 25 such molecules, 25 have the two groups verified model\-equivalent\.

#### How often does a practitioner’s budget land badly?

By[Corollary˜2](https://arxiv.org/html/2607.26344#Thmcorollary2)the admissible budgets are the prefix sums of the orbit sizes when the orbits carry distinct values, and the subset sums of the tied block otherwise\. Between 19\.5% and 39\.8% of budgets in\[1,20\]\[1,20\]are of neither form, depending on the dataset\. Budgets below the motif size are ordinary practice, not a corner case:Ying et al\. \([2019](https://arxiv.org/html/2607.26344#bib.bib30)\)useKM=10K\_\{M\}\{=\}10on real\-world data,Luo et al\. \([2020](https://arxiv.org/html/2607.26344#bib.bib20)\)use ten edges on molecules,Yuan et al\. \([2021](https://arxiv.org/html/2607.26344#bib.bib31)\)fix a five\-node budget for every dataset, and the sweeps inAmara et al\. \([2022](https://arxiv.org/html/2607.26344#bib.bib2)\)andKosan et al\. \([2024](https://arxiv.org/html/2607.26344#bib.bib17)\)reach down to five\.

#### Reproducibility\.

Because the tie is settled by array order, permuting the rows of an edge list, a semantic no\-op, can change what is reported\. For an equivariant explainer we observe the reported top\-kkto change on 0\.0–10\.6% of symmetric graphs and on 0\.0% of asymmetric graphs from the same datasets and model\. PyTorch documents thattopkdoes not guarantee stable indices among tied elements and may differ between CPU and CUDA, so the choice is delegated to behaviour the library declines to define, and two widely used implementations resolve it incompatibly: the original GNNExplainer code thresholds the mask and keeps both alternatives, while PyTorch Geometric takes a top\-kkand keeps one\.

### Stability Metrics under a Severed Orbit

Resolve a severed orbit three ways under oneσ\\sigma\-invariant attribution\. Using the cross\-run Jaccard ofKosan et al\. \([2024](https://arxiv.org/html/2607.26344#bib.bib17)\), breaking the tie by array index as current practice does scores 1\.0000, sampling the orbit 0\.8005, and reporting the orbit whole 1\.0000, while the first two outputs are automorphic images with identical fidelity in 93\.1% of cases\. The metric cannot separate an explainer that is canonical from one that is deterministic about being arbitrary, since both return the same set every run and so score11by construction\. A stability of11certifies a sorting routine rather than the data, and reporting the orbit structure beside the score costs one integer per instance\.

### Robustness across Architectures

The criterion reads onlyAut​\(G\)\\mathrm\{Aut\}\(G\)and the mask, which[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)makes orbit\-constant for any equivariant explainer and any network\. Repeating the core measurements on MUTAG with a graph isomorphism network and a graph attention network \(training accuracies 0\.867, 0\.851, 0\.840\), across 6768 further instance–budget decisions the criterion again agrees with the mechanical check on every one \(100\.00%\), and the equivariant explainers again surface only one of two interchangeable groups between 4\.8% and 36\.7% of the time\. Combined with the earlier sweeps this brings the validation to 21298 decisions without an exception\.

The separation between explainer families is the same on all three architectures\. For the gradient\-based explainers the asymmetry of the attribution underσ\\sigmasits at2​e−92e\-9, which is floating\-point noise, since[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)is exact in exact arithmetic and the residue depends only on the order in which a sum is accumulated\. For GNNExplainer it is0\.140\.14–0\.170\.17, eight orders of magnitude larger, because a sparsity\-regularised optimiser has no reason to settle on the symmetric point even when the objective is symmetric about it\. GAT is no exception, as[Proposition˜2](https://arxiv.org/html/2607.26344#Thmproposition2)anticipates: attention coefficients are normalised over a neighbourhood, so a layer remains a function of the neighbour multiset\.

## Orbit\-Aware Reporting

Algorithm 1Orbit\-aware reporting1:Input:graph

GG, attribution

mm, budget

kk, target

vv\(node\-level tasks only\)

2:

H←Aut​\(G\)H\\leftarrow\\mathrm\{Aut\}\(G\)if graph\-level, else

Stab​\(v\)\\mathrm\{Stab\}\(v\)//nauty, vertices coloured by feature vector

3:

𝒪←\\mathcal\{O\}\\leftarroworbits of

HHacting on

EE// union–find over generators

4:sort

𝒪\\mathcal\{O\}by decreasing mean of

mmover each orbit

5:

S←∅S\\leftarrow\\emptyset
6:for

O∈𝒪O\\in\\mathcal\{O\}in sorted order while

\|S\|<k\|S\|<kdo

7:

S←S∪OS\\leftarrow S\\cup O// a whole orbit, never a part of one

8:endfor

9:return

SS, together with

\|𝒪\|\|\\mathcal\{O\}\|and

maxO⁡\|O\|\\max\_\{O\}\|O\|// so the reader is told a class was reported

[Algorithm˜1](https://arxiv.org/html/2607.26344#alg1)selects whole orbits in decreasing order of mean attribution until the budget is met\. Its output isAut​\(G\)\\mathrm\{Aut\}\(G\)\-invariant by construction, satisfying*\(i\)*and*\(iii\)*of[Theorem˜1](https://arxiv.org/html/2607.26344#Thmtheorem1)and relaxing strict minimality\. On MUTAG it eliminates the arbitrariness entirely, from 83\.8% of budget–instance pairs to none, at a median 0\.11 ms per molecule \(0\.89 ms worst case\) and 0\.43 additional edges displayed\. Fidelity here is the drop in the predicted\-class logit when the reported subgraph is deleted,f​\(G\)c−f​\(G∖S\)cf\(G\)\_\{c\}\-f\(G\\setminus S\)\_\{c\}, averaged over instances and larger when the report carries more of the evidence\. It moves from 5\.1312 to 5\.1425\.

#### What a practitioner should do\.

Three findings translate directly into practice\. First, report\|Aut​\(G\)\|\|\\mathrm\{Aut\}\(G\)\|: it costs 0\.11 ms and tells a reader that symmetry\-induced non\-canonicity is possible, the check on whether it is realised being whether the reported set is a union of complete orbits\. Second, prefer a budget landing on an orbit boundary; between 19\.5% and 39\.8% of budgets in\[1,20\]\[1,20\]do not, and the check is combinatorial\. Third, if a single subgraph must be shown, show the orbit containing it and say so\. None of these needs a new explainer or retraining\. Benchmark designers should add a fourth: choose a motif’s attachment vertex deliberately, since attaching through one its automorphism group moves removes the symmetry silently\.

## Limitations

Our models have a few dozen nodes and at most three layers; transformer\-style models, whose relation is coarser still, are untested\. We claim no novelty for the group theory, credited in full above\. The validation of[Proposition˜4](https://arxiv.org/html/2607.26344#Thmproposition4)is a consistency check, so given[Proposition˜1](https://arxiv.org/html/2607.26344#Thmproposition1)its role is to establish that nothing outside the criterion is at work rather than to predict something new\. The test of[Proposition˜2](https://arxiv.org/html/2607.26344#Thmproposition2)against a bond\-reading network carries that burden instead\. The nitro\-pair case rests on 25 molecules, so its rates carry wide intervals \(11\.5–43\.4% atk=10k\{=\}10\), and at small budgets most of them have neither group reported at all\. Finally, we do not claim any published figure or qualitative claim is incorrect: our model, training and dataset version differ from the works we cite, and we measure only the rate at which the mechanism occurs\.

## Conclusion

For graphs, equivariance is not only a property an explanation should have but a constraint: naming one of two substructures the model cannot separate is a decision, not a summary\.

## References

- Agarwal et al\. \(2023\)Agarwal, C\.; Queen, O\.; Lakkaraju, H\.; and Zitnik, M\. 2023\.Evaluating Explainability for Graph Neural Networks\.*Scientific Data*, 10\(1\): 144\.
- Amara et al\. \(2022\)Amara, K\.; Ying, R\.; Zhang, Z\.; Han, Z\.; Shan, Y\.; Brandes, U\.; Schemm, S\.; and Zhang, C\. 2022\.GraphFramEx: Towards Systematic Evaluation of Explainability Methods for Graph Neural Networks\.In*Proceedings of the First Learning on Graphs Conference*\.
- Azzolin et al\. \(2025\)Azzolin, S\.; Longa, A\.; Barbiero, P\.; Liò, P\.; and Passerini, A\. 2025\.Reconsidering Faithfulness in Regular, Self\-Explainable and Domain Invariant GNNs\.In*International Conference on Learning Representations*\.
- Bleukx et al\. \(2025\)Bleukx, I\.; Verhaeghe, H\.; Bogaerts, B\.; and Guns, T\. 2025\.Exploiting Symmetries in MUS Computation\.In*Proceedings of the AAAI Conference on Artificial Intelligence*\.
- Borgwardt et al\. \(2005\)Borgwardt, K\. M\.; Ong, C\. S\.; Schönauer, S\.; Vishwanathan, S\. V\. N\.; Smola, A\. J\.; and Kriegel, H\.\-P\. 2005\.Protein Function Prediction via Graph Kernels\.*Bioinformatics*, 21\(suppl\_1\): i47–i56\.
- Bui et al\. \(2024\)Bui, N\.; Nguyen, H\. T\.; Nguyen, V\. A\.; and Ying, R\. 2024\.Explaining Graph Neural Networks via Structure\-aware Interaction Index\.In*Proceedings of the 41st International Conference on Machine Learning*\.
- Crabbé and van der Schaar \(2023\)Crabbé, J\.; and van der Schaar, M\. 2023\.Evaluating the Robustness of Interpretability Methods through Explanation Invariance and Equivariance\.In*Advances in Neural Information Processing Systems*, volume 36\.
- Debnath et al\. \(1991\)Debnath, A\. K\.; Lopez de Compadre, R\. L\.; Debnath, G\.; Shusterman, A\. J\.; and Hansch, C\. 1991\.Structure\-Activity Relationship of Mutagenic Aromatic and Heteroaromatic Nitro Compounds\.*Journal of Medicinal Chemistry*, 34\(2\): 786–797\.
- Duval and Malliaros \(2021\)Duval, A\.; and Malliaros, F\. D\. 2021\.GraphSVX: Shapley Value Explanations for Graph Neural Networks\.In*Machine Learning and Knowledge Discovery in Databases \(ECML PKDD\)*\.
- Dym, Lawrence, and Siegel \(2024\)Dym, N\.; Lawrence, H\.; and Siegel, J\. W\. 2024\.Equivariant Frames and the Impossibility of Continuous Canonicalization\.In*Proceedings of the 41st International Conference on Machine Learning*\.
- Faber, Moghaddam, and Wattenhofer \(2021\)Faber, L\.; Moghaddam, A\. K\.; and Wattenhofer, R\. 2021\.When Comparing to Ground Truth is Wrong: On Evaluating GNN Explanation Methods\.In*Proceedings of the 27th ACM SIGKDD Conference on Knowledge Discovery and Data Mining*\.
- Fey and Lenssen \(2019\)Fey, M\.; and Lenssen, J\. E\. 2019\.Fast Graph Representation Learning with PyTorch Geometric\.In*ICLR Workshop on Representation Learning on Graphs and Manifolds*\.
- Hu et al\. \(2020\)Hu, W\.; Liu, B\.; Gomes, J\.; Zitnik, M\.; Liang, P\.; Pande, V\.; and Leskovec, J\. 2020\.Strategies for Pre\-training Graph Neural Networks\.In*International Conference on Learning Representations*\.
- Kaba and Ravanbakhsh \(2023\)Kaba, S\.\-O\.; and Ravanbakhsh, S\. 2023\.Symmetry Breaking and Equivariant Neural Networks\.In*NeurIPS Workshop on Symmetry and Geometry in Neural Representations*\.ArXiv:2312\.09016\.
- Kazius, McGuire, and Bursi \(2005\)Kazius, J\.; McGuire, R\.; and Bursi, R\. 2005\.Derivation and Validation of Toxicophores for Mutagenicity Prediction\.*Journal of Medicinal Chemistry*, 48\(1\): 312–320\.
- Kipf and Welling \(2017\)Kipf, T\. N\.; and Welling, M\. 2017\.Semi\-Supervised Classification with Graph Convolutional Networks\.In*International Conference on Learning Representations*\.
- Kosan et al\. \(2024\)Kosan, M\.; Verma, S\.; Armgaan, B\.; Pahwa, K\.; Singh, A\.; Medya, S\.; and Ranu, S\. 2024\.GNNX\-Bench: Unravelling the Utility of Perturbation\-based GNN Explainers through In\-depth Benchmarking\.In*International Conference on Learning Representations*\.
- Lawrence et al\. \(2025\)Lawrence, H\.; et al\. 2025\.Equivariance Everywhere All At Once: A Recipe for Graph Foundation Models\.*arXiv preprint arXiv:2503\.21985*\.
- Ling et al\. \(2025\)Ling, H\.; Yu, H\.; Jiang, Z\.; Zou, N\.; and Ji, S\. 2025\.On Explaining Equivariant Graph Networks via Improved Relevance Propagation\.In*Proceedings of the 42nd International Conference on Machine Learning*\.
- Luo et al\. \(2020\)Luo, D\.; Cheng, W\.; Xu, D\.; Yu, W\.; Zong, B\.; Chen, H\.; and Zhang, X\. 2020\.Parameterized Explainer for Graph Neural Network\.In*Advances in Neural Information Processing Systems*, volume 33\.
- Luong et al\. \(2024\)Luong, K\.\-D\.; Kosan, M\.; Silva, A\. L\. d\.; and Singh, A\. 2024\.Robust Ante\-hoc Graph Explainer using Bilevel Optimization\.*arXiv preprint arXiv:2305\.15745*\.
- McKay and Piperno \(2014\)McKay, B\. D\.; and Piperno, A\. 2014\.Practical Graph Isomorphism, II\.*Journal of Symbolic Computation*, 60: 94–112\.
- Morris et al\. \(2020\)Morris, C\.; Kriege, N\. M\.; Bause, F\.; Kersting, K\.; Mutzel, P\.; and Neumann, M\. 2020\.TUDataset: A Collection of Benchmark Datasets for Learning with Graphs\.In*ICML Workshop on Graph Representation Learning and Beyond*\.
- Morris et al\. \(2019\)Morris, C\.; Ritzert, M\.; Fey, M\.; Hamilton, W\. L\.; Lenssen, J\. E\.; Rattan, G\.; and Grohe, M\. 2019\.Weisfeiler and Leman Go Neural: Higher\-Order Graph Neural Networks\.In*Proceedings of the AAAI Conference on Artificial Intelligence*\.
- Smidt, Geiger, and Miller \(2021\)Smidt, T\. E\.; Geiger, M\.; and Miller, B\. K\. 2021\.Finding Symmetry Breaking Order Parameters with Euclidean Neural Networks\.*Physical Review Research*, 3\(1\): L012002\.
- Srinivasan and Ribeiro \(2020\)Srinivasan, B\.; and Ribeiro, B\. 2020\.On the Equivalence between Positional Node Embeddings and Structural Graph Representations\.In*International Conference on Learning Representations*\.
- Sundararajan, Taly, and Yan \(2017\)Sundararajan, M\.; Taly, A\.; and Yan, Q\. 2017\.Axiomatic Attribution for Deep Networks\.In*Proceedings of the 34th International Conference on Machine Learning*\.
- Wu et al\. \(2018\)Wu, Z\.; Ramsundar, B\.; Feinberg, E\. N\.; Gomes, J\.; Geniesse, C\.; Pappu, A\. S\.; Leswing, K\.; and Pande, V\. 2018\.MoleculeNet: A Benchmark for Molecular Machine Learning\.In*Chemical Science*, volume 9, 513–530\.
- Xu et al\. \(2019\)Xu, K\.; Hu, W\.; Leskovec, J\.; and Jegelka, S\. 2019\.How Powerful are Graph Neural Networks?In*International Conference on Learning Representations*\.
- Ying et al\. \(2019\)Ying, Z\.; Bourgeois, D\.; You, J\.; Zitnik, M\.; and Leskovec, J\. 2019\.GNNExplainer: Generating Explanations for Graph Neural Networks\.In*Advances in Neural Information Processing Systems*, volume 32\.
- Yuan et al\. \(2021\)Yuan, H\.; Yu, H\.; Wang, J\.; Li, K\.; and Ji, S\. 2021\.On Explainability of Graph Neural Networks via Subgraph Explorations\.In*Proceedings of the 38th International Conference on Machine Learning*\.

The appendix records material that does not fit the main text: the machine\-checked development behind the combinatorial criterion, the per\-explainer and per\-budget breakdowns behind figures quoted in aggregate, and the experimental detail needed to reproduce them\. The body of the paper is self\-contained and nothing here is load\-bearing for any claim it makes\. Every number below is generated from the same archived run outputs as the paper’s, byscripts/make\_supplement\.py\.

## Appendix AThe Lean development

The combinatorial core of the criterion is that a permutation fixes a set setwise exactly when that set is a union of complete orbits\. We mechanise it in Lean 4 over a finite index type, with no dependency onMathlibor on any other library\. The development islean/OrbitSplit\.leanin the code archive, is 96 lines long, and elaborates in under three seconds\.

The claim in the paper that the three theorems carry*no axiom dependencies whatsoever*is checked by the file itself, which ends with three`\#print axioms`commands\. Their output, verbatim:

$ lean OrbitSplit\.lean’OrbitSplit\.img\_eq\_iff\_closed’does not depend on any axioms’OrbitSplit\.not\_closed\_imp\_img\_ne’does not depend on any axioms’OrbitSplit\.neutrality\_excludes\_split’does not depend on any axioms

Not even propositional extensionality is used\. This is a statement about the combinatorial kernel only\. It says the kernel is unconditional and machine\-checked; it does not certify the empirical claims, the choice of automorphism group, or the implementation of any probe, all of which rest on the experiments instead\.img\_eq\_iff\_closedis the biconditional used as Proposition 4 in the paper;not\_closed\_imp\_img\_neis the contrapositive form used when the criterion predicts a severed orbit;neutrality\_excludes\_splitis the statement that a neutral report cannot cut an orbit\.

Reproducing the check requires only a Lean 4 toolchain:

$ lean lean/OrbitSplit\.lean

## Appendix BExtended results

[Table˜4](https://arxiv.org/html/2607.26344#A2.T4)gives every explainer on every dataset of the breadth sweep, rather than the range quoted in the paper\. Two features are worth noting\. The gradient\-based family and PGExplainer sit at or below10−810^\{\-8\}asymmetry, which is accumulation\-order noise, while GNNExplainer is eight orders of magnitude above it\. And the rate at which a report severs an orbit is not monotone inkk: it rises and falls as the cut crosses orbit boundaries, which is the signature the criterion predicts from the graph alone\.

[Table˜5](https://arxiv.org/html/2607.26344#A2.T5)gives the nitro\-pair audit at every budget rather than atk=10k\{=\}10alone\. The*arb\.*column equals the*one*column in every cell: whenever exactly one of two interchangeable groups is surfaced, the automorphic alternative is accepted by the model within tolerance, with no exceptions at any budget for any of the three explainers\. The counts are small,n=25n\{=\}25, and the paper reports a Wilson interval alongside the headline rate for that reason\.

[Table˜6](https://arxiv.org/html/2607.26344#A2.T6)gives the criterion against the mechanical check as a confusion matrix on the synthetic benchmarks\. The published BA\-2Motifs house generator contributes no symmetric instances at all, which is the benchmark accident the paper describes; the repaired attachment point restores them and the criterion is exercised there\.

[Table˜7](https://arxiv.org/html/2607.26344#A2.T7)gives, per dataset, the fraction of budgets in\[1,20\]\[1,20\]that admit a neutral report\.[Table˜8](https://arxiv.org/html/2607.26344#A2.T8)gives the full distribution behind the paper’s finding that equality of representations does not transfer to equality of attributions\.

Table 4:All seven explainers on the three real datasets of the breadth sweep\.*asym*is the mean asymmetry of the attribution under the automorphism,*agree*the agreement of the criterion with the mechanical model\-equivalence check, and thekkcolumns give the rate at which the reported top\-kksevers an orbit\. The gradient\-based explainers sit at floating\-point noise; GNNExplainer does not\.Table 5:The nitro\-pair audit at every budget, on the 25 MUTAG molecules whose two nitro groups are exchanged by an automorphism\.*one*is the count with exactly one group surfaced,*both*with both,*neither*with neither\.*arb\.*counts the*one*cases in which the automorphic alternative is accepted by the model within tolerance; it equals*one*at every budget and every explainer\.Table 6:Criterion versus mechanical check on the synthetic benchmarks, as a confusion matrix\. TP is a severed orbit that the model confirms admits an equally valid alternative\. The published BA\-2Motifs house generator yields no symmetric instances at all, which is the benchmark accident discussed in the paper; the repaired attachment restores them\.ExplainerBenchmarknnTPFPFNTNIntegratedGradientsBA\-2Motifs cycle5 \(published\)2808000200IntegratedGradientsBA\-2Motifs house \(repaired\)2808000200IntegratedGradientsTree\-Cycles112190093IntegratedGradientsTree\-Grid1403400106SaliencyBA\-2Motifs cycle5 \(published\)2808000200SaliencyBA\-2Motifs house \(repaired\)2808000200SaliencyTree\-Cycles112200092SaliencyTree\-Grid1404000100*overall*1624agreement 100\.00%Table 7:Budgets in\[1,20\]\[1,20\]admitting a neutral report, per dataset\.*predicted unsafe*is computed from the orbit sizes alone;*observed split*is measured from the reported top\-kk\. The gap between them is the quantity the criterion is required to explain\.Table 8:Does equality of representations transfer to equality of attributions? Rows one and two are the positive control, where a genuine automorphism relates the pair and Proposition 1 forces equality\. Rows three and four are pairs sharing a colour\-refinement class without being automorphic\. Equality largely fails there, which is why the paper stops the hierarchy at the representation\.Of the 165 instance–budget pairs on MUTAG whose reported top\-kksevers an orbit, 0 admit a neutral score\-optimal alternative of the same size\. 25 molecules do carry two distinct orbits at equal score, so the possibility the corollary describes is realised in the data; it simply never rescues a severed budget here\.

## Appendix CThe oscillation signature

![Refer to caption](https://arxiv.org/html/2607.26344v1/x3.png)Figure 3:The criterion’s signature on Tree\-Grid, computed from the graph alone before any model is consulted\. Shaded budgets are those whose cut consumes whole edge orbits\. For Integrated Gradients the rate of severing falls to zero at every one of them and rises to the maximum in between\. Saliency alternates in the same phase but less sharply, because it ranks different orbits into the report\. GNNExplainer, whose optimised mask is notσ\\sigma\-invariant, never returns to zero at any budget tested\. Rates are measured, not smoothed\.[Figure˜3](https://arxiv.org/html/2607.26344#A3.F3)is the clearest visual form of Proposition 4 and was cut from the main paper for space\. Nothing in the paper depends on it; the same behaviour is reported numerically in the validation paragraph\.

## Appendix DExperimental detail

#### Models\.

Three\-layer GCNs with hidden width6464and sum pooling, trained with Adam at learning rate0\.010\.01\. The epoch count was raised from6060to300300with dataset size until training accuracy cleared the0\.70\.7floor, and no further tuning was done: the phenomenon under study is a property of the reporting step, not of model quality, and a model that has not learned the task has no explanation worth auditing\. The bond\-reading network is a three\-layer GINE of the same width trained identically, except on Mutagenicity where0\.010\.01does not converge and0\.0030\.003is used\. GINE\-const is the same architecture with the bond feature replaced by a constant, so that it differs from GINE in the information available and not in the parameterisation\.

#### Seeds\.

Every measurement over seeds setstorchandnumpyseeds explicitly before each explainer call\. The stability comparison uses eight runs per instance, the cross\-seed decomposition six, and the incidence and criterion sweeps are deterministic given a seed and use one\. The main limitation the paper states in this respect is that model training itself is single\-seed, so the GINE separation rates are reported as measured rather than as means over restarts\.

#### Automorphism groups\.

Computed exactly withnautythroughpynauty, with vertices coloured by their complete feature vector\. Colouring byargmaxis adequate only for strictly one\-hot encodings and produces spurious automorphisms on mixed integer descriptors such as BBBP’s\. Where the bond\-preserving reading is wanted, the vertex\-coloured group is computed first and its elements are then filtered to those preserving edge labels, which yields the correct subgroup rather than an approximation of it\.

#### Tolerance\.

Model equivalence uses the relative test\|o1−o2\|≤10−4​max⁡\(\|o1\|,\|o2\|,1\)\|o\_\{1\}\-o\_\{2\}\|\\leq 10^\{\-4\}\\max\(\|o\_\{1\}\|,\|o\_\{2\}\|,1\)throughout\. An absolute threshold of10−510^\{\-5\}misclassifies 4 of 884 decisions in the largest sweep, all of which differ by exactly one unit in the last place of float32 at an output magnitude near128128\.

#### Cost\.

The full suite runs on CPU on one laptop core; no GPU is used at any point\. The automorphism computation that the remedy requires takes a median of 0\.11 ms per molecule and 0\.89 ms in the worst case observed\.