{"id":"5a3ac7cb-3877-466a-9566-d08563c8f22b","arxiv_id":"2512.19332","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"GNNs with ReLU can compute numerical graph queries that GNNs with bounded, saturating activations cannot, even when both use linear layers.","lead":"The paper studies graph neural networks as a query language and separates what different activation functions can compute. Its headline result: ReLU gives strictly more numerical expressive power than saturating activations, even when linear layers are allowed.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 6.6 is false on the truncated trees T[r,b,k]: boundary red/blue nodes have one white neighbour, so the uniform S_r/S_b form cannot hold. The proof of Theorem 6.8 needs a boundary-free formulation.","rationale":"The central separation claim (Theorem 6.8) depends on Lemma 6.6 and Lemma 6.7. Lemma 6.7's polynomial-parity argument appears sound, but Lemma 6.6's structural induction is not valid for the finite trees used. The paper's own definition of T[r,b,k] is inconsistent for finite trees: boundary nodes cannot satisfy the stated degree conditions. This is not a matter of real vs rational coefficients; it affects even expressions with rational/bool coefficients. The reader's weakest assumption mentioned Lemma 6.6's structural induction but attributed possible failure to arbitrary real coefficients; our check shows a more concrete failure: boundary truncation. The rational-coefficient qualifier overclaim is real, but secondary. A moderately simple fix (evaluate on a tree taller than the expression depth, or on the infinite biregular tree) may salvage Theorem 6.8, so we do not reject the claim outright. The verdict remains CONDITIONAL, with the added condition that Lemma 6.6 must be restated/proved for the actual (possibly infinite or interior) evaluation context.","tokens_in":27806,"tokens_out":28140,"duration_ms":261479,"concrete_test":"Compute the value of the bool-MPLang expression e := bool(^1 - 3/2) on the intended T[1,1,3] (the radius-3 ball of the infinite alternating tree) at a red node at depth 1 and at a red node at depth 3. The values are 1 and 0 respectively, contradicting Lemma 6.6's claim that all red nodes share one value S_r(1,1). More formally: check whether any finite tree can simultaneously satisfy the degree conditions in Sec. 6.1 for k=3 (red/blue nodes have two white neighbours, white nodes have r+b neighbours); it cannot, because leaves must have degree 1. If the authors instead intend a truncated tree, rerun the Lemma 6.6 induction on that tree with e; it fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of Theorem 6.8 rests on Lemma 6.6, which asserts that every bool-MPLang expression of ^-depth ≤ k evaluates on T[r,b,k] to a rigid 'nice' form, with the same S_r(r,b) at every red node and the same S_b at every blue node. The inductive step for ^ in Appendix C uses that red and blue nodes have exactly one w-type and one w'-type white neighbour. But T[r,b,k] is defined as a finite rooted tree of height k. In any finite tree, nodes at distance k have degree 1, so a red/blue node at distance k-1 has only one white neighbour (unless the degree conditions are violated). Thus the very object satisfying the stated conditions does not exist, or the boundary nodes have truncated neighbourhoods. Concretely, in the radius-3 ball (k=3, r=b=1), a depth-1 red node satisfies ^1=2, while a depth-3 red leaf has ^1=1. For e = bool(^1 - 3/2), these evaluate to 1 and 0, so no single S_r(r,b) can represent all red nodes. Lemma 6.6 is therefore false as stated. Since Theorem 6.8 applies Lemma 6.6 at the root of T[r,b,k] with k equal to the ^-depth of e^*, and the induction passes through boundary nodes, the proof has a genuine gap. A repair would evaluate on a larger ambient tree/infinite biregular tree so the radius-(^depth) neighbourhood of the root is interior, or restrict the induction to nodes whose radius-k neighbourhood is complete; neither is done in the paper. The rational-coefficient qualifier is a separate issue, but this tree-boundary problem is more directly load-bearing.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies MPLang, a declarative language that captures GNN-style message passing with linear aggregation and activation functions. It gives a walk-based normal form for the affine fragment A-MPLang, proves that over coloured graphs all uneven eventually constant activations are numerically equivalent to bool-MPLang (in the rational-coefficient fragment), and then aims to prove that ReLU-MPLang is numerically strictly more expressive than any eventually constant activation even in the presence of linear/identity layers. The main separation is Theorem 6.8, which claims that the query Q = ReLU(^red − ^blue) is not expressible in bool-MPLang, via an analysis of evaluations on red–blue symmetric trees T[r,b,k] and a polynomial-parity argument (Lemma 6.7).","tokens_in":28223,"tokens_out":11734,"duration_ms":123834,"significance":"If the main separation were fully established, it would be a valuable result: it would give the first numerical expressiveness gap between ReLU-GNNs and GNNs with eventually constant activations when identity/linear layers are allowed, and it would strengthen the logic-based understanding of GNN expressivity. The paper also contains useful positive results: the walk normal form for A-MPLang (Theorem 4.2) and the closure/Booleanisation results for eventually constant activations (Section 5). Lemma 6.7, an independent polynomial argument showing that 'nice' functions cannot encode |x−y|, is a solid technical contribution. However, the main separation is not yet reliably established: the tree lemma used in the proof has a boundary flaw, and the theorem statements around the ReLU/bool containment are too strong and, in one reading, false.","major_comments":[{"comment":"Lemma 6.6 is false as stated because T[r,b,k] is a finite rooted tree of height k, so its boundary nodes do not satisfy the uniform neighbourhood conditions used in the induction. For example, when k=3 and r=b=1, a red node at depth 1 has two white neighbours (one w-type, one w′-type), while a red leaf at depth 3 has only one white neighbour. The expression e = bool(^1 − 3/2) evaluates to 1 at the depth-1 red node and to 0 at the depth-3 red leaf, so no single symmetric function S_r(r,b) can describe all red nodes, contradicting Lemma 6.6. The proof of Lemma 6.6 explicitly uses that red/blue nodes have exactly one w-type and one w′-type white neighbour, which fails at the boundary. Since Theorem 6.8 applies Lemma 6.6 with k equal to the ^-depth of e*, and the structural induction passes through boundary nodes, the proof of Theorem 6.8 has a genuine gap. A repair would need to evaluate on","section":"§6.1, Lemma 6.6 / definition of T[r,b,k]"},{"comment":"Proposition 6.2 states that ReLU-MPLang numerically strictly contains bool-MPLang. The proof only shows that one particular query, Q = ReLU(^red − ^blue), is in ReLU-MPLang and not in bool-MPLang; it does not prove the containment direction bool-MPLang ⊆ ReLU-MPLang. This is not just a missing detail: for full real-coefficient bool-MPLang the containment is false. Let r be a Liouville number as in Lemma A.2 and consider the bool-MPLang expression bool(r·^red − ^blue). On star graphs with a red and b blue neighbours this query must output 1 when r a − b > 0 and 0 when r a − b ≤ 0, a discontinuous function of the linear input (a,b). Any ReLU-MPLang expression, built from addition, scalar multiplication, neighbourhood summation, and the continuous function ReLU, evaluates to a continuous piecewise-affine function of the input values, so it cannot equal this discontinuous Boolean-valued func","section":"§6, Proposition 6.2"},{"comment":"Theorem 6.1 is stated for arbitrary sets Σ of uneven eventually constant functions, but the proof route through Theorem 5.5 and Proposition 6.2 does not support this generality. Theorem 5.5 says that the rational fragment of Σ-MPLang is numerically equivalent to bool-MPLang, where the simulating bool expression may use real coefficients because the values σ(ℓ/d), σ(t−), σ(t+) of the eventually constant function need not be rational. The subsequent containment in rational ReLU-MPLang is therefore not obtained. In fact, Theorem 6.1 is false as stated: let σ be the uneven eventually constant function with σ(x)=√2 for x>0 and σ(x)=0 for x≤0. On coloured graphs the expression σ(1) in rational Σ-MPLang evaluates to √2 at every node, but every rational ReLU-MPLang expression evaluates to a rational number at every node of every coloured graph (by a straightforward induction, since ReLU preserve","section":"§5.2 / §6, Theorem 5.5 and Theorem 6.1"}],"minor_comments":[{"comment":"The abstract and the introduction omit the rational-coefficient qualifier when describing the equivalence of eventually constant activations. Theorem 5.5 is explicitly about the rational fragment, and the abstract should match the theorem statement.","section":"Abstract / §5.2"},{"comment":"The sentence 'Combined with Theorem 5.5, which shows that all eventually constant activation functions are equivalent to TrReLU' is inaccurate: Theorem 5.5 establishes equivalence with bool-MPLang, not with TrReLU. This wording should be corrected.","section":"§6, before Proposition 6.2"},{"comment":"The remark that on graphs of bounded depth the query of Theorem 6.8 is expressible, with proof omitted, is relevant to understanding why the construction needs unbounded depth. If this fact is used to justify the proof strategy, a proof or reference should be supplied.","section":"§6.2"}],"recommendation":"major_revision","confidential_remarks":"The manuscript contains promising ideas and at least one clean technical contribution (Lemma 6.7), but the central separation theorem is not currently supported. The finite-tree boundary problem in Lemma 6.6 is repairable, and the overly broad statements in Theorem 6.1/Proposition 6.2 can likely be corrected by restricting to rational-valued eventually constant activations and proving the needed containment direction. I recommend major revision rather than rejection because the intended result for standard activations such as TrReLU, sign, and bool is plausibly salvageable. However, the authors should be asked to state and prove the exact containment theorem they need, and to fix the tree construction or the induction before the paper can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"What should you know about this paper? The headline separation — ReLU-MPLang strictly contains bool-MPLang on k-coloured graphs — is not proven as written. The tree family T[r,b,k] used in the proof is internally inconsistent, and Lemma 6.6, the rigid-form lemma, is false on the truncated trees. That is a load-bearing flaw, not a cosmetic one.\n\nWhat is genuinely good: the A-MPLang normal form (Theorem 4.2) in terms of walk counts and walk-summed features is clean. The Boolean non-closure results for A-MPLang — especially the Liouville-number argument for non-closure under negation with real coefficients — are careful and interesting. Theorem 5.5, the numerical equivalence of rational Σ-MPLang and bool-MPLang for uneven eventually constant activations, looks right and is a useful extension of [8]. The embedding of L-MP2 into bool-MPLang and the strictness witness are also fine. The paper engages squarely with prior work.\n\nThe problem. T[r,b,k] is defined as a finite rooted tree of height k satisfying: w-type white nodes have r red and b blue neighbours, and red/blue nodes have one w-type and one w'-type white neighbour. In any finite tree, leaves have degree one. A red leaf at depth k has exactly one white neighbour, so it cannot satisfy the stated condition. In fact no finite tree satisfies all four conditions. Lemma 6.6 then fails: on T[r,b,3], take e = bool(^1 − 3/2). A red node at depth 1 has two white neighbours, so ^1 = 2 and e = 1; a red leaf at depth 3 has one white neighbour, so ^1 = 1 and e = 0. No single S_r(r,b) can represent both. The proof of Lemma 6.6 uses the two-neighbour fact for red/blue nodes in the ^ case, so the induction breaks exactly at the boundary. Since Theorem 6.8 evaluates at the root but the induction passes through boundary nodes, the main separation is unsupported. A repair probably exists — use a larger K or an infinite biregular tree and restrict to interior nodes — but it isn't in the paper.\n\nA separate, smaller issue: the abstract and Proposition 6.2 state the separation without the rational-coefficient qualifier that Theorem 6.1 itself carries. The full real-coefficient containment for arbitrary eventually constant activations is not established.\n\nBottom line: for someone working on logical characterizations of GNNs, the paper's first five sections are worth reading, and the separation claim is important if it can be fixed. As submitted, though, the central theorem is unproven. I'd send it to a referee — the idea is significant and the flaw is plausibly repairable — but the referee should put the tree-boundary problem at the top of the list.","headline":"The ReLU vs eventually-constant separation is unproven as written: the tree family T[r,b,k] is inconsistent and Lemma 6.6 fails at boundary nodes; the rest of the paper is solid but the headline needs a real fix.","tokens_in":28757,"tokens_out":10422,"would_cite":false,"duration_ms":103356,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"ReLU-MPLang, the logical language corresponding to ReLU graph neural networks, numerically strictly contains every MPLang variant with eventually constant activations on coloured graphs with at least two colours.","keywords":["MPLang","graph neural networks","activation functions","ReLU","expressive power","walk-sum normal forms","Boolean queries","eventually constant functions"],"falsifier":"Search for a bool-MPLang expression e such that e evaluates at the root of T[r,b,k] to |r−b| for all natural r,b—equivalently, run an exhaustive enumeration of bool-MPLang expressions up to a fixed ^-depth on small trees T[r,b,k] and check whether evaluation matches |r−b|. Any such expression, or any pair (r,b) where a claimed 'nice plus affine plus simple' form fails, would overturn Lemma 6.7 and with it Theorem 6.8.","tokens_in":27696,"feed_emoji":"🧠","tokens_out":6308,"duration_ms":59979,"temperature":0.7,"pith_summary":"The paper studies MPLang, a declarative language that captures the computation of graph neural networks through linear message passing plus an activation function. It shows that the activation-free fragment of MPLang has a complete normal form in terms of walk counts and walk-summed features, and that its Boolean queries are not closed under conjunction or modal iteration. For bounded, eventually constant activations (truncated ReLU, sign, bool), the paper proves that all such activations yield the same numerical and Boolean expressive power over coloured graphs. The central result is a strict separation: with ReLU, MPLang can express numerical queries—starting from ReLU(^red − ^blue)—that no eventually-constant-activated variant can express, even when linear layers are allowed. If correct, this pins the expressive advantage of modern GNNs on the choice of an unbounded activation function.","feed_headline":"ReLU beats every bounded activation in GNN numerical queries","feed_subtitle":"A node-counting query separates ReLU networks from truncated-ReLU, sign, and boolean-activation networks.","key_machinery":"The red–blue symmetric tree T[r,b,k] is a rooted tree of height k whose root is a white node with r red and b blue children, with red and blue nodes sitting between alternating white types (r red, b blue, or swapped). The paper classifies the functions arising from bool-MPLang evaluations on this family: a 'nice' function is a finite sum of polynomials multiplied by simple symmetric step functions. Lemma 6.6 shows by structural induction that every bool-MPLang expression of ^-depth at most k evaluates at white root-type nodes to F(r,b) + α(r,b) + β(r,b), with F nice, α affine, and β simple; red and blue node values are symmetric nice functions. Lemma 6.7 is the technical heart: it proves—via","core_discovery":"The main discovery is a strict expressive separation for numerical queries on k-coloured graphs with k ≥ 2: rational ReLU-MPLang numerically strictly contains rational Σ-MPLang for every finite set Σ of uneven eventually constant activations. The witness query is Q := ReLU(^red − ^blue), which computes how many more red than blue neighbours a node has, truncated below at zero. The paper proves Q is not definable in bool-MPLang by evaluating bool-expressions on a family of red–blue symmetric trees T[r,b,k]. There, every bool-MPLang expression of ^-depth at most k evaluates at the root to a function of the rigid form 'nice function plus affine function plus simple step function', and the paper","pith_inferences":["The separation is proved for numerical queries; the paper leaves open whether a Boolean query (one whose answer is just the sign of a numerical output) also separates ReLU from bounded activations. A plausible route is to take the same tree family and threshold Q at zero, but the paper does not claim this.","The main theorems are stated with rational coefficients in the language. Since the paper's own negation result for A-MPLang relies on irrational Liouville coefficients, it is possible that the containment direction behaves differently with arbitrary real coefficients—an extension that is not established here.","The 'nice function' classification suggests a general template: compare any two activation functions by the shape of the functions they induce on a family of symmetric trees. The same template could be applied to other unbounded activations such as GELU or ELU to test whether unboundedness is the operative property.","The walk-sum normal form implies that the separation might be rephrased in linear-algebraic terms: ReLU can apply a non-linear gate to a walk-count affine form, while bounded activations, on trees of unbounded depth, reduce to rigid piecewise-polynomial forms that cannot reproduce absolute differences."],"forward_implications":["ReLU-GNNs with linear layers compute numerical node queries that no truncated-ReLU-, sign-, or bool-activated GNN with linear layers can compute, on coloured graphs with at least two colours.","Because every uneven eventually constant activation is numerically equivalent to bool over coloured graphs, no combination of bounded activations can close the gap against ReLU.","The walk-based normal form for the activation-free fragment shows that linear (identity-only) GNNs see only walk counts and endpoint-feature sums, so non-linearities are necessary to reach modal-logic-level Boolean expressiveness.","Adding identity layers to an eventually-constant-activated GNN strictly increases its Boolean expressiveness, even though the specific bounded activation used does not matter."],"fun_headline_variants":["ReLU strictly beats bounded activations in GNN numerics","ReLU outdoes truncated ReLU and sign in GNN queries","ReLU wins over all eventually constant activations","ReLU separates from bounded activations in GNNs","Unbounded ReLU trumps bounded activations for GNN numbers"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof that every bool-MPLang expression on the red–blue symmetric trees collapses to a 'nice plus affine plus simple' function, and that no such function can match |r−b|; if even one expression escapes this rigid form, the ReLU-versus-bounded separation collapses.","fun_headline_variants_meta":{"raw":{"variants":["ReLU strictly beats bounded activations in GNN numerics","ReLU outdoes truncated ReLU and sign in GNN queries","ReLU wins over all eventually constant activations","ReLU separates from bounded activations in GNNs","Unbounded ReLU trumps bounded activations for GNN numbers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000183,"raw_usage":{"total_tokens":1140,"prompt_tokens":724,"completion_tokens":416,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":468,"completion_tokens_details":{"reasoning_tokens":345}},"tokens_in":468,"tokens_out":416,"duration_ms":4803,"temperature":1.0,"reasoning_tokens":345,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T14:46:12.300167+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search for a bool-MPLang expression e such that e evaluates at the root of T[r,b,k] to |r−b| for all natural r,b—equivalently, run an exhaustive enumeration of bool-MPLang expressions up to a fixed ^-depth on small trees T[r,b,k] and check whether evaluation matches |r−b|. Any such expression, or any pair (r,b) where a claimed 'nice plus affine plus simple' form fails, would overturn Lemma 6.7 and with it Theorem 6.8.","supporting_citations":[],"review_version":1}