AI 中文总结
该研究揭示GNN的Top-k解释存在自同构诱导的非正则性，提出Lean 4实现的无参数准则判断分数最优报告是否分裂轨道，发现其在Mutagenicity数据集中普遍存在，报告轨道可消除任意性。
AI 中文摘要
基于梯度的图神经网络（GNN）解释器在给定具有两个化学等价硝基的分子时，会为它们分配仅在最后一位不同的归因分数。它别无选择：消息传递恰好是置换等变的，因此输入的任何自同构都会使所有归因保持不变。然而，标准报告的Top-k边会指定其中一个硝基，而选择哪一个由数组的顺序决定。我们证明这是一种结构障碍而非实现失误：当输入的自同构群未确定最小有效解释时，没有规则能同时满足单值性、最小性和对称性尊重。对于实践中使用的精确k报告，我们提出一个无参数准则，该准则在Lean 4中实现机械化且无公理依赖，仅通过图本身即可判断该大小的每个分数最优报告是否必然分裂轨道。在21298个实例-预算决策中，该准则与机械模型等价性检查完全一致，且未发现任何分裂情况存在中性替代方案。这种障碍很常见：在开创性可解释性论文使用的Mutagenicity数据集中，93.4%的分子存在非平凡自同构，因此在连续域中成立的对称输入测度零论在此失效。在这些论文报告的稀疏性预算下，具有两个可互换硝基的分子中有24.0%（25个中的6个）仅指定其中一个，且每个都在机械验证下表现出任意性。模型的“失明”也会产生对称性：每个MUTAG分子包含化学可区分但网络无法区分的原子，匹配对照实验表明，这种区分由模型读取的内容而非参数化方式决定。报告轨道可消除这种任意性，每图耗时0.11毫秒，额外增加0.43条边。
英文摘要
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-k edges, 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-k reports 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.
Comments11 pages, 3 figures
