자기동형사상에 의한 상위 k개 설명의 비-고유성 문제: 그래프 신경망에서의 연구

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

분자 내 두 개의 화학적으로 동일한 니트로 그룹이 존재하는 경우, 기울기 기반 GNN 설명기는 이들의 기여도 점수를 마지막 비트 값으로 할당합니다. 이는 불가피하며, 메시지 전달 과정 자체가 순열 등변성을 가지므로 입력 그래프의 어떤 자기동형사상이라도 모든 기여도에 영향을 미치지 않습니다. 그러나 일반적인 보고 방식인 상위 k개 에지는 이 두 그룹 중 하나만을 선택하며, 그 선택은 배열의 순서에 의해 결정됩니다. 본 연구에서는 이것이 구현상의 오류가 아닌 구조적인 제약임을 보여줍니다. 입력 그래프의 자기동형사상군에 의해 고정된 최소 유효 설명이 없을 경우, 어떤 규칙도 동시에 단일 값, 최소값, 그리고 대칭성을 만족할 수 없습니다. 실제 사용되는 정확한 k개 보고 방식에 대해, Lean 4를 사용하여 어떠한 공리에도 의존하지 않고 그래프 자체만으로 모든 최적의 보고 방식이 특정 궤도를 분할해야 하는지 여부를 결정하는 파라미터-프리 기준을 제시합니다. 21298개의 인스턴스 예시에서 이 기준은 예외 없이 기계적인 모델 동등성 검사와 일치하며, 발견된 모든 분할되는 경우에 대해 중립적인 대안이 존재하지 않았습니다. 이러한 제약은 일반적입니다. Mutagenicity 데이터셋(기존 설명 가능성 연구에서 사용)의 93.4%에서 비자명한 자기동형사상이 발생하므로, 연속적인 영역에서는 유효했던 대칭 입력에 대한 '측정 가능한 확률이 매우 낮다'는 주장은 여기서 무너집니다. 보고서의 희소성 제약 조건 하에서, 두 개의 교환 가능한 니트로 그룹을 가진 분자 중 24.0% (6개 중 25개)가 정확히 하나의 그룹만을 보여주며, 이는 기계적인 검증에 의해 임의적으로 결정됩니다. 모델의 '맹점' 또한 대칭성을 야기합니다: 모든 MUTAG 분자는 화학적으로 구별되는 원자를 포함하며, 네트워크는 이를 명확하게 구분할 수 없습니다. 제어 실험을 통해 이러한 현상이 모델의 파라미터 설정이 아닌 모델이 읽는 정보에 의해 결정됨을 보여줍니다. 궤도를 보고하는 방식은 0.11ms의 시간과 그래프당 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.