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

Gradient-based GNN explainers fail to provide canonical top-k edge attributions for graphs with structural automorphisms, such as chemically equivalent functional groups. Because message passing is permutation equivariant, any attribution must be invariant under automorphisms, forcing exact-k reports to arbitrarily select edges from a single orbit. The authors provide a parameter-free criterion, verified in Lean 4, to identify when score-optimal explanations necessarily violate symmetry.