{"id":"e09a7d9c-c2c4-4f27-a9f1-afc0e96deb4f","arxiv_id":"2607.26344","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"partial","parameter_count":2,"one_line_summary":"On symmetric graphs, an exact-k GNN explanation cannot be simultaneously single-valued, minimal, and symmetry-respecting, so any report naming one edge from an automorphism orbit is an arbitrary tie-break.","lead":"This paper shows that when a molecule has a symmetry, a graph neural network's top-k explanation can be arbitrary: an equivariant explainer must give identical scores to interchangeable edges, so picking one of them is a tie-break, not evidence. The authors prove a no-go theorem, provide a machine-checked criterion for detecting forced tie-breaks, and measure that the problem is common in standard molecular datasets.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The trilemma's trigger condition Min(S)^H=∅ is never verified; the measured top-k severing is a separate reporting effect. A fidelity-based check of Min(S)^H would clarify whether the theorem applies to the empirical cases.","rationale":"The reader's weakest assumption concerned the definition of validity being model-output-based; my concern is narrower: even granting that definition, the paper does not verify that the trilemma's condition Min(S)^H=∅ holds in the empirical cases. The top-k severing phenomenon is a direct consequence of Proposition 1 and the reporting step, independent of the trilemma. Thus the paper's headline 'obstruction is common' may overstate the applicability of Theorem 1 unless the condition is checked. This is a scope/emphasis issue, not a correctness issue, so the reader's CONDITIONAL verdict stands. I credit the paper for honestly calling the validation a consistency check and for the Lean mechanisation of the combinatorial core.","tokens_in":15589,"tokens_out":17294,"duration_ms":160101,"concrete_test":"For the 25 nitro-pair MUTAG molecules (and a sample of symmetric MUTAG molecules), compute edge orbits under H=Aut(G) (vertex colours as the model reads them). Enumerate unions of edge orbits (≤2^r for r edge orbits); for each union U, evaluate the frozen GCN's predicted-class logit after masking U and record Valid(U) iff the logit change is within a stated tolerance (e.g., relative 1e-4). Find the minimal valid unions (valid U with no valid proper sub-union). If any such minimal valid union exists, then Min(S)^H is nonempty. Report the number of molecules with Min(S)^H=∅; if it is substantially below the reported severing rates, the trilemma is not the operative mechanism behind the top-k phenomenon.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 1 is correct, but the paper's empirical package does not establish that its trigger condition, Min(S)^H = ∅, holds for the molecules studied. The 93.4% incidence of nontrivial automorphisms (Table 1) and the 24.0% rate of one-group-only top-k reports (Table 3) concern exact-k reporting (Proposition 4/Corollary 2), not the nonexistence of an H-fixed minimal valid explanation. A symmetric graph can have H-fixed minimal sufficient subgraphs, in which case a single-valued, minimal, neutral rule exists and the top-k arbitrariness is a separate reporting artifact. The paper never computes S or Min(S) for real instances, so the trilemma's practical reach is unquantified. This matters for the abstract's claim that 'the obstruction is common': the theorem's obstruction is a precise set-theoretic condition, not the mere presence of automorphisms.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies top-k explanations of GNNs on graphs with nontrivial automorphisms. Because message passing is permutation equivariant, any validity criterion built from model outputs is invariant under Aut(G); hence rules for selecting explanation subgraphs face exact ties. The central theoretical result (Theorem 1) is a conditional trilemma: a single-valued, minimal, and neutral selection rule exists exactly when the set of minimal valid explanations contains an element fixed by the full automorphism group. For the exact-k reporting used in practice, Propositions 4 and Corollary 2 give a graph-only subset-sum criterion for whether every score-optimal report of a given size must sever an edge orbit. The combinatorial core is mechanised in Lean 4 with no axiom dependencies. Empirically, the paper measures the incidence of automorphisms in several datasets, validates the criterion against a mechanical model-equivalence check on 21,298 decisions, documents attribution-level ties versus top-k-level severing on 25 nitro-pair MUTAG molecules, and proposes an orbit-aware reporting algorithm.","tokens_in":1475,"tokens_out":2780,"duration_ms":210320,"significance":"The exact-k reporting obstruction is a real and practically relevant phenomenon. It is convincingly isolated: for equivariant explainers, attribution is tied exactly, and the top-k report can still select one orbit representative with no model-based reason. The paper's strengths include a machine-checked combinatorial kernel, a parameter-free check that needs only Aut(G) and the mask, very large empirical agreement under its stated tolerance, and a fully scripted/reproducible pipeline. The paper also honestly labels the mechanical check as a consistency check rather than an independent prediction. The main caveat is that the broader 'obstruction is common' claim in the abstract relies on equating the presence of automorphisms and top-k severing with the trilemma trigger Min(S)^H=empty, which is never verified. That overreach does not invalidate the exact-k contribution, but it needs repair.","major_comments":[{"comment":"The paper states after Corollary 1 that 'the instances measured below are exactly those where [Min(S)^H=empty] holds.' This is not established anywhere. The empirical results (Tables 1, 3, 5, 6) concern exact-k reporting under a sigma-invariant mask (Proposition 4 / Corollary 2), not the nonexistence of an H-fixed minimal valid explanation. A symmetric graph can have an H-fixed minimal sufficient subgraph while a top-1 report severs an orbit; the trilemma then does not trigger even though top-k is non-neutral. The abstract's 'the obstruction is common' therefore conflates the exact-k reporting obstruction with the conditional trilemma. To keep the claim, define a concrete Valid criterion, compute or bound Min(S) for the datasets/instances, and verify Min(S)^H is empty, or soften the abstract and conclusion to claim only the exact-k reporting obstruction.","section":"The Trilemma / Corollary 1"},{"comment":"The abstract claims that the criterion 'agrees with a mechanical model-equivalence check without exception' over all 21,298 decisions. Appendix Table 4 reports agreement of 99.4-99.8% for several rows (e.g., PROTEINS GNNExplainer 99.4%). The main text's 100.0% is under a relative tolerance, and under an absolute tolerance the figure drops to 99.83%. State which tolerance Table 4's 'agree' column uses, which decisions are included in the 21,298 total, and why the appendix rates are not exceptions. Without this, the 'without exception' claim is ambiguous and potentially overstated.","section":"Robustness across Architectures / Appendix Table 4"}],"minor_comments":[{"comment":"The neutrality definition treats sigma.G as equal to G at the point where Proposition 3 concludes hat-sigma(Phi(G))=Phi(G). With concrete node-indexed tensors, sigma.G is a different input. State explicitly whether graphs are considered up to relabeling, and how a rule is extended equivariantly to all relabeled inputs in the converse direction.","section":"Theory / Proposition 3"},{"comment":"The terms 'manufactured' and 'intrinsic' pairs are used in Table 2 but defined only in the text. Add a short definition to the caption or a Symbol/Definition block.","section":"Table 2"},{"comment":"The abstract says attribution scores are equal 'to the last bit', while the body reports an integrated-gradient asymmetry of about 2e-9. Report the actual maximum ULP distance or say 'to floating-point accumulation noise'.","section":"Abstract / Results"},{"comment":"The sentence 'The disparity is manufactured wholly by the reporting step' is accurate for the exactly equivariant explainers, but not for GNNExplainer, whose optimised attribution itself is non-equivariant (ratios up to 2.93x). Qualify the sentence so it does not appear to apply to the GNNExplainer rows of Table 3.","section":"When a Report Severs an Orbit / GNNExplainer"},{"comment":"The Lean development mechanises Proposition 4's orbit-set lemma, but Corollary 2's subset-sum condition does not appear to be part of the Lean files. State precisely which part of the exact-k criterion is machine-checked, so the abstract's 'criterion, mechanised in Lean 4' is not overread.","section":"Appendix A / Abstract"}],"recommendation":"major_revision","confidential_remarks":"The core theorem and exact-k reporting criterion are sound, and the machine-checked kernel plus reproducible scripts are genuine strengths. The main risk is the empirical overclaim about the trilemma's reach: the paper never verifies Min(S)^H=empty for the datasets it says trigger the theorem. I would ask for either a direct test of that condition on the small nitro-pair set or a revised abstract/conclusion that confines the 'common obstruction' claim to exact-k top-k reporting. Once that is resolved, the paper is publishable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe thing to know: this paper has a genuinely useful observation — that exact equivariance of GNNs makes top-k explanation reports over symmetric graphs arbitrary tie-breaks — and it proves the relevant combinatorial criterion both cleanly and in Lean 4 with no axioms. The empirical work is extensive and the reporting effect is real. But the paper's most quoted claim, that the trilemma's obstruction is common, is not actually verified. The measured severing is an exact-k reporting effect, not the nonexistence of a minimal explanation fixed by the automorphism group. The theorem's trigger condition, Min(S)^H = ∅, is never computed.\n\nWhat is new and good. The prior group theory is credited honestly. The composition with top-k is the contribution, and it's a good one: a parameter-free criterion that decides from the graph and mask whether every score-optimal report of size k must split an orbit. The Lean mechanization is a nice touch — 96 lines, no axiom dependencies, discharge of the three key statements. The validation over 21,298 decisions is a consistency check, as the paper admits, and it's a strong one. The benchmark accident (the house motif's attachment vertex killing its own automorphism) is a genuinely useful finding for anyone generating synthetic graphs. The orbit-aware reporting remedy is simple and practical.\n\nSoft spots. The stress-test concern lands: Theorem 1 is conditional on Min(S)^H = ∅, and the paper never establishes that this holds for the molecules studied. A symmetric graph can have an H-fixed minimal valid explanation; top-k can still sever an orbit because the budget doesn't line up. The 93.4% automorphism incidence and the 24% nitro-pair rate speak to the reporting criterion (Proposition 4 / Corollary 2), not to the trilemma. The sentence at the end of Corollary 1 — \"the instances measured below are exactly those where it holds\" — is not supported by anything in the experiments. The abstract's \"the obstruction is common\" reads as referring to the trilemma, but the evidence supports a narrower statement about top-k reports.\n\nOther soft spots are minor. The validity criterion is assumed to be a function of the frozen model's outputs, so σ-invariance transfers; that's stated clearly, and it's the right frame for post-hoc explainability, but it does limit the scope. The upward-closedness assumption for the orbit remedy is flagged. The empirical package has small samples in the nitro-pair audit (25 molecules) and some single-seed training; the paper acknowledges both.\n\nBottom line. The combinatorial core is correct, the reporting phenomenon is real and measured, and the paper is honest about what it has and hasn't done. The main overclaim is the reach of the trilemma. A referee should ask the authors to either verify Min(S)^H on a sample of molecules or soften the claim to the reporting-level result, which is strong enough on its own. I'd send this to peer review.","headline":"The combinatorial core is correct and machine-checked, but the paper's headline claim that the trilemma's obstruction is common is not actually verified — the measured effect is a top-k reporting artifact, not the trigger condition.","tokens_in":16294,"tokens_out":4035,"would_cite":true,"duration_ms":35328,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"For a symmetric graph, no single top-k explanation can be minimal, neutral, and unique unless a minimal valid explanation is fixed by the automorphism group; reports that name one interchangeable edge are arbitrary tie-breaks.","keywords":["graph neural networks","explainability","automorphisms","top-k explanations","equivariance","symmetry","non-canonicity","mutagenicity"],"falsifier":"Take any symmetric graph where the paper's criterion predicts a severed orbit at some budget. Form the top-k subgraph, apply the automorphism to it, feed both as hard masks to the frozen model, and compare the predicted-class logits. If the outputs differ by more than one float32 unit in the last place—the paper's observed tolerance—then the automorphic alternative is not equally valid, contradicting the paper's claim that every severed orbit is arbitrary. A second, structural falsifier would be any instance with no automorphism-fixed minimal valid explanation for which a single-valued, minima","tokens_in":15455,"feed_emoji":"⚖️","tokens_out":7055,"duration_ms":64320,"temperature":0.7,"pith_summary":"This paper argues that when a graph has a nontrivial automorphism—two interchangeable nitro groups in a molecule, say—a top-k explanation of a graph neural network cannot simultaneously be single-valued, minimal, and symmetry-respecting, unless one minimal valid explanation is fixed by the whole automorphism group. Message passing is exactly permutation equivariant, so any attribution derived from the model's outputs ties the interchangeable elements to the last bit; only the reporting step breaks the tie, by array order. The paper proves this as a trilemma, gives a parameter-free combinatorial criterion that decides from the graph and mask alone whether a given exact-k budget must split an orbit, and verifies the criterion against a mechanical model-equivalence check on 21,298 decisions with no exceptions. It measures the phenomenon as common: 93.4% of Mutagenicity graphs admit relevant nontrivial automorphisms, and at k=10, 24.0% of 25 MUTAG molecules with two interchangeable nitro groups surface exactly one, with the automorphic alternative accepted by the model in every such case. A practical consequence is that reporting whole orbits instead of individual edges removes the arbitrariness at negligible cost.","feed_headline":"Graph symmetry makes top-k AI explanation choices arbitrary","feed_subtitle":"No explanation rule can be single-valued, minimal, and symmetry-respecting when no optimal subgraph survives the automorphism group.","key_machinery":"Theorem 1 (the conditional trilemma) is the load-bearing object: single-valued, minimal, and neutral cannot coexist exactly when no minimal valid explanation is fixed by the automorphism group. Proposition 1 (exact equivariance) supplies the premise by showing message passing makes model outputs and hence validity exactly invariant under automorphisms. Proposition 4 and Corollary 2 convert the trilemma into a graph-only decision rule for exact-k reports: a report is neutral exactly when the cut severs no edge orbit, and a neutral score-optimal report exists exactly when the leftover budget is a sum of complete orbit sizes from the tied block. This criterion is mechanised as a machine-checked","core_discovery":"The central claim is Theorem 1: for an input graph G with automorphism group H, a selection rule that returns exactly one minimal valid explanation and respects symmetry exists exactly when the set of minimal valid explanations contains a member fixed by H. Since message passing is exactly permutation equivariant, every validity criterion built from the model's outputs is exactly H-invariant; therefore, when no minimal explanation survives the symmetry, any single top-k report must choose among model-equivalent alternatives, and the choice is arbitrary. For exact-k reports, a combinatorial condition decides whether every score-optimal report of that size severs an orbit; the paper finds seve","pith_inferences":["Because the formal kernel is really a statement about a permutation acting on a finite set, the non-canonicity likely transfers beyond GNNs to any equivariant scoring procedure that must emit one representative from a tied orbit.","A testable extension would audit transformer-style graph models: since their receptive fields are coarser, the relevant equivalence relation is coarser still, likely producing larger orbits and more frequent severed budgets—the paper leaves this untested.","The paper's orbit-aware reporting suggests a redefinition of explanation-evaluation metrics: treating orbit members as equivalent would make the stability gap disappear by construction, whereas current fidelity and sparsity metrics on single masks cannot express the symmetry.","The 24.0% rate rests on 25 molecules and the paper reports a wide interval; a replication on larger molecular datasets with many interchangeable functional groups would tighten the estimate."],"forward_implications":["Any equivariant explainer's top-k output on a symmetric input can name one member of an orbit the model scores identically; the displayed edge is a convention, not evidence.","A stability score of 1 does not certify canonicity: tie-breaking by array index attains it, while an orbit-sampling rule that produces equally faithful outputs scores lower.","Reporting whole orbits instead of single edges removes the arbitrariness, at about 0.11 ms per molecule and 0.43 extra edges on MUTAG.","The common dismissal of symmetric inputs as measure-zero is wrong on graphs: 93.4% of Mutagenicity instances carry relevant nontrivial automorphisms, so the obstruction is routine.","Common synthetic benchmarks understate the phenomenon because their generator attaches motifs through a vertex its own automorphism moves; re-attaching through a fixed apex restores symmetry."],"fun_headline_variants":["Symmetry makes top-k GNN explanations arbitrary","GNN explainers' top-k picks are symmetry-forced arbitrary","Automorphism ties: GNN top-k choices are non-canonical","When no single top-k subgraph survives symmetry, choices are arbitrary"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The argument collapses if validity is not a function of the frozen model's outputs: if a human or chemical definition of 'valid explanation' distinguishes two automorphic substructures, Proposition 1's exact invariance no longer transfers to the set of valid explanations, and the trilemma need not bite.","fun_headline_variants_meta":{"raw":{"variants":["Symmetry makes top-k GNN explanations arbitrary","GNN explainers' top-k picks are symmetry-forced arbitrary","Automorphism ties: GNN top-k choices are non-canonical","When no single top-k subgraph survives symmetry, choices are arbitrary"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000209,"raw_usage":{"total_tokens":1302,"prompt_tokens":857,"completion_tokens":445,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":601,"completion_tokens_details":{"reasoning_tokens":373}},"tokens_in":601,"tokens_out":445,"duration_ms":4218,"temperature":1.0,"reasoning_tokens":373,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T00:06:23.529914+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any symmetric graph where the paper's criterion predicts a severed orbit at some budget. Form the top-k subgraph, apply the automorphism to it, feed both as hard masks to the frozen model, and compare the predicted-class logits. If the outputs differ by more than one float32 unit in the last place—the paper's observed tolerance—then the automorphic alternative is not equally valid, contradicting the paper's claim that every severed orbit is arbitrary. A second, structural falsifier would be any instance with no automorphism-fixed minimal valid explanation for which a single-valued, minima","supporting_citations":[],"review_version":1}