From Neural Networks to Logical Theories: The Correspondence between Fibring Modal Logics and Fibring Neural Networks
Authors: Ouns El Harzli
Bernardo Cuenca Grau
Artur d'Avila Garcez
Ian Horrocks
Tarek R. Besold
Venue: ICLR 2026 Poster (2026)
Keywords: fibring
modal logics
logical expressiveness
graph neural networks
transformer encoders
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Fibring of modal logics is a well-established formalism for combining countable families of modal logics into a single fibred language with common semantics, characterized by fibred models. Inspired by this formalism, fibring of neural networks was introduced as a neurosymbolic framework for combining learning and reasoning in neural networks. Fibring of neural networks uses the (pre-)activations of a trained network to evaluate a fibring function computing the weights of another network whose outputs are injected back into the original network. However, the exact correspondence between fibring of neural networks and fibring of modal logics was never formally established. In this paper, we close this gap by formalizing the idea of fibred models compatible with fibred neural networks. Using this correspondence, we then derive non-uniform logical expressiveness results for Graph Neural Networks (GNNs), Graph Attention Networks (GATs) and Transformer encoders. Longer-term, the goal of this paper is to open the way for the use of fibring as a formalism for interpreting the logical theories learnt by neural networks with the tools of computational logic.

Published as a conference paper at ICLR 2026
FROM NEURAL NETWORKS TO LOGICAL THEORIES: THE CORRESPONDENCE BETWEEN FIBRING MODAL LOGICS AND FIBRING NEURAL NETWORKS
Ouns El Harzli
Bernardo Cuenca Grau
Artur D'Avila Gareez*
Ian Horrocks'
Tarek R. Besold
I Depaarmment of Computer Science, University of Oxford, UK Sony AI Barcelona, Spain
*Sony AI Tokyo, Japan 4 CCiy St George's, s, University of London, UK
ABSTRACT
Fibring of modal logics a well-established formalism for combining countable families of modal logics into a single fibred language with common semantics, characterized by fibred models. Inspired by this formalism, fibring of neural net- works was introduced as a neurosymbolic framework for combining learning and reasoning in neural networks. Fibring of neural networks uses the (pre-)activationn a trained network to evaluate a fibring function computing the weights another network whose outputs are injected back into the original network. However, the exact correspondence between fibring of neural networks and fibring modal log- ics was never formally established. In this paper, we close this gap by formalizing the idea of fibred models compatible with fibred neural networks. Using this corre- spondence, then derive non-uniform logical expressiveness results for Graph Neural Networks (GNNs), Graph Attention Networks (GAT's and Transformer encoders. Longer-term, the goal of this paper is to open the way for the use of fibring as a formalism for interpreting the logical theories learnt by neural networks with the tools of computational logic.
INTRODUCTION
The advent of large language models has created unprecedented interest in the task of reasoning in neural networks. Logical reasoning is arguably the best perspective study and develop this
capability in neural networks. Logic offers precise definitions, validity conditions and a formalism that
amenable verification. As result, there has been surge of interest in the field of neurosymbolic Al that studies the integration of neural networks with logical reasoning (Besold et al., 2022 Lamb
al. 2020 d' Avila Garcez & Lamb 2023).
Fibring of neural networks (Garcez & Gabbay 2004) is a theoretical concept from the neurosymbolic
Al literature introduced way of combining neural network architectures for learning and reasoning.
The idea of fibring is to make the parameters of a network a function of another network, with the resulting output injected back into the original network when computing the output of the combined (fibred) neural network. This theoretical framework was initially inspired by the concept of fibring logics (Gabbay 1999). in particular combining modal logics (Chellas) 1980), which play an important role in systems verification; temporal logic, special case of modal logic, is extensively used in formal verification (Vardi& & Wolper 1986). Fibred neural networks were shown (Garcez Gabbay 2004) to be strictly more expressive than the usual composition of neural networks. Fibred networks intended to offer a framework for the study of the combination of learning and reasoning in neural
"Correspondence ouns. el.. .hazz1 1@cs. w.s..xx.... ac.uk.kk

---

Published as a conference paper at ICLR 2026
networks, whereby one network's learning influences another network's inference. In fibred modal logic language, the Kripke model" and the possible world in which a formula is evaluated are a function of a possible world in another Kripke model. However, the precise correspondence between fibring of neural networks and fibring of modal logics was not formally established until now.
An important research area in neurosymbolic AI aims to establish correspondences between logic and modern neural architectures, motivated by the prospect of rendering the latter more reliable, interpretable or verifiable. In particular, Graph Neural Networks (GNNs) and Transformers have become essential components in contemporary machine learning. each tackling specific but sometimes intersecting challenges across a wide range of applications. GNNs excel at processing structured graph data, having found extensive use in fields such as social network analysis, drug discovery, and knowlede loowledge graphs (Salamat et al., 202T; Xiong et al. 2021 Ye et al. 2022). Transformers have revolutionized natural language processing by modeling intricate contextual relationships in sequential data, providing unprecedented capabilities for tasks such as language understanding and generation
/Vaswani et al. 2017 Devlin al. 2019; Brown et al. 2020 OpenAl 2023 Bronstein et al. 2021). The capabilities of these architectures have sparked a significant research effort to analyze rigorously their logical expressiveness, i.e. the classes of formal languages that they can compute, and their formal verification. An interesting connection exists between GNNs, and Transformer encoders (Bronstein et al. 202T): Transformer encoders can be viewed as GNNs applied to complete graphs with added positional encoding and an attention mechanism. This connection, however, has not been exploited in the literature on logical expressivity and formal verification. This gap leaves potential for unifying logical characterizations of both architectures.
Logical expressiveness of modern architectures. Existing logical expressiveness results for GNNs and Transformers can be categorized into: discriminative power (e.g. is there a logical classifier that can distinguish the same pairs of nodes GNN?); wniform expressiveness (e.g. is there a logical formula whose truth values coincide with the output of a GNN given any input graph and node?); and non-uniform expressiveness (in which the logical formulas can depend on the input). In this categorization, uniform expressiveness stand out as the most powerful kind, providing complete logical characterization for neural architectures (i.e. providing a single logical formula for each instance (choice of weights) of a neural architecture independently of the input). Initial results established that the discriminative power of standard GNNs is upper-bounded by the Weisfeiler- Leman (WL) test (Barceló et al.) (020). Subsequently, Grohe (2023) established non-uniform expressiveness results for GNNs in terms of Boolean circuits and descriptive complexity. More recently, uniform expressiveness results of broad classes of GNNs have been derived (Nunn et al. 2024, Benedikt et al. 2024) using known logics called Presburger logics, which involve counting modalities and linear inequalities. Using existing results about the satisfiability of such logics, results about the computational complexity of formal verification problems for neural networks follow as corollaries (e.g. answering the question: given an output and a GNN, is there an input the GNN that yields that output?). In particular, Benedikt et al. (022)) provides a taxonomy for the decidability of these verification problems depending on the types of aggregations and activation functions being used. CCunnaa Grau et al. (2025) established uniform expressiveness results for bounded GNNs in terms of fragments of first-order logic, showcasing how restrictive yet practical assumptions on the class of GNNs may simplify significantly their logical characterization. Transformer encoders have also been studied through the lens of circuit complexity theory. Unique Hard Attention Transformers (UHATs) have been mapped to fragments of the complexity class of AC" languages with extensions based on a restricted form of first-order logic (Hao et al. (022). Average Hard Attention Transformers (AHATs) have been shown capable of capturing more complex languages, including those outside AC and more recently a uniform lower bound has been established w.r.t. linear temporal logic using a language called LTL. (C, +), which also involves counting modalities (Barcelo et al. 2024). While expressiveness results for GNNs and Transformers share certain similarities (e.g. counting modalities), there is still no unified theory that accounts for both architectures.
Contributions. In this paper, we propose fibring of modal logics as a new formalism to study the logical expressiveness of neural architectures, including GNNs and Transformers. We start by redefining fibring neural networks (Garcez& & Gabbay 2004) to make its use easier in the context
'The word model here refers to logic structures with assignments of truth-values true or false, differently from the use of the word in neural networks.
2

---

Published as a conference paper at ICLR 2026
of the above literature. We then formally establish an exact correspondence between fibring neural networks and fibring modal logics. That is, (i) we define a fibred language based on a fibring architecture; (ii) we introduce the notion of compatible fibred models (with fibred neural networks and their inputs) on which to interpret the formulas; (iii) we prove that our proposed fibred logic is valid fibred logic by demonstrating that the class of compatible fibred models is non-empty and closed under Kripke-model isomorphism; and (iv) we construct the formulas from our fibred logic whose truth values coincide with the outputs of fibred neural networks. Subsequently, we prove that fibred neural networks can be used to non-umt uniformly describe large classes of GNNs, Graph Attention Networks (GATs) and Transformer encoder architectures. It follows that the corresponding fibred languages provide non-uniform expressiveness results for these network architectures. Our hope is that fibring can become unifying formalism for the study of GNNs and Transformers in neurosymbolic AI.
As future directions of research, we speculate that fibring as a formalism might hold the key to deriving and unifying uniform expressiveness results for GNNs and Transformer encoders, and we present our main arguments for this possible unification in Section 6 We argue that the proposed fibring framework provides new intuitive way of thinking about GNNs and Transformers successive combinations of underlying modal logics, and we discuss how this new perspective might be useful for the comparative evaluations, interpretability and verification of modern neural networks.
The remainder of the paper is organized as follows. Section 2 introduces the notation used throughout the paper. Section 3 provides the new definition of fibring. Section 4 proves the correspondence between fibring networks and modal logics. Section 5ection|5appples this result to derive expressiveness results for GNNs, GATs and Transformer Encoders. Section (ection66cconcieee concludes the paper and discusses directions for future work.
2 PRELIMINARIES
We work with vectors and matrices of rational numbers. The ith entry of a vector v is written e;, and the entry in row i, column of matrix A is written A.j- If two matrices have the same number of columns, we can place them side by side to form a larger matrix, called their concatenation.
A neural architecture A. is specified by the number of its layers L,, the dimension of each layer de. and an activation map of Qd + Qui for each hidden layer. With L layers, dg and dr are referred to as the input and output dimensions, respectively, and for each hidden layer f, the activation map of computable in polynomial time. We may also talk about a portion of the architecture ranging from layer p to layer q. and call this the sub aub-architecture AP9, If q = L, we write Art for simplicity.
network instance of an architecture assigns weights and biases, known as the set of parameters, to each layer. The weights of layer é form matrix W xdexde-1, and the biases form vector b' E Qd To apply a network instance N to an input vector x, we compute the weighted sum of the input weighted by the parameters followed by the application of the activation function in the usual way proceeding from the input layer to the output. The final output of the network is a vector of the output's dimension. Formally, the application of N to Qdia generates a sequence h², ..... h- of vectors defined as h' W x bb, where x" = x, x" = o' o'(h). The result (xx) of applying A to x is the vector h', We also talk about sub-networks. The sub-network. A/ra consists of the layers from p through q and parameters. If = L. we write Nrt..
3 FIBRING NEURAL NETWORKS
In this section, we introduce definition of fibred neural networks which generalizes the original definition of Garcez& & Gabbay (2004) to any number and possible combinations of neural networks.
A fibring architecture is directed tree whose nodes v are labeled with neural architectures A.. Each edge (v, e') is labeled with: (i) layer number l' in the parent architecture; and (ii) set of positions S in that layer denoting the fibred neurons. We impose the additional requirement that for any two edges (v, w) and (t, u) sharing the parent node and labeled with the same layer number, the corresponding sets of positions must be disjoint. Finally, we denote by F the class of fibring architectures which verify the property that: (i) the architecture at the root has two linear layers with
3

---

Published as a conference paper at ICLR 2026
input dimension n and output dimension 1, and (ii) every edge leaving the root node is labeled with the same layer number
A fibred network N is tuple (N.F, where N is network instance, F is a fibring architecture, and ff is finite collection of fibring functions matching F, i.c. one function f(w,")) for each edge (v, u') in F, which specifies how to build an instance of the child architecture and what input to give it; specifically,, for an edge (v, 2²) labeled with layer number f, the fibring function f(r,o)) maps vectors of dimension S de network instance of architecture Agr and valid input vector for that architecture.
To apply a fibred neural network N to an input x, we start the root. Whenever we reach a layer that has edges leading to children, we pause, call the corresponding fibring function, and pass part of the current vector into the child network. The child network produces a new vector, which is spliced back into the parent's 's computation at the specified positions. The overall computation proceeds recursively until the output layer the root reached.
Formally, the computation is defined inductively. FF has only the root node u, then N( = ((x). Otherwise, let u1:-... Mk be the children of with edges (u, u4) labeled (e,, St), let Fi be the subtree rooted us, and let be the restriction of f to edges in F,. Assume the children are ordered so that & < E I S lx. For each stage 1 < S k, define a tuple N4, Ys. h,) as follows:
(x), Ne (h; (h;-1); i 1,
i 1,
X;
(N, y:) = f(u,a)(Xi))
h, x, with entries in S, replaced by (N., F.. (y.), the application of the fibred network to y,.
Child
Firiig tuncton
Prevachvaoons
Waghts
Figure I: Illustration of fibring between two architectures. The pre-activations a given layer within the parent network are fed into fibring function to produce the input and the weights of the child network, the output of the child network is then reinjected at the same pre-activations.
The final output is:
N(x) -
the output of the root network is scalar, we can interpret the fibred network as a classifier the usual way: input x, it outputs true if the final value is strictly greater than 0, and false otherwise.
4

---

Published as a conference paper at ICLR 2026
4 EXACT CORRESPONDENCE BETWEEN FIBRING LOGICS AND FIBRING NETWORKS
In this section, introduce fibred modal language for combining different modal systems and show it captures exactly the behavior of fibred neural networks
Modal logics and fibring (Gabbay 1999): Fix finite set of propositions PROP {Pr..... Pr. and a countable collection of modal operators D (one for each index i). For each i, logic C; has formulas built from propositions, T (true), Boolean connectives, and the modal operators D. The semantics is the usual Kripke semanties: each L, uses a class of Kripke models, and 4gp holds at a world w in a model when y holds at all accessible worlds w, from w according to a pre-defined accessibility relation R such that R( R(w,, w) holds ]
To fibre these logics, we allow all the modal operators D in one combined language. That is, formulas are built from the grammar:
== P p1 A p2 - D
where p E PROP and ranges over the fibred modal logics Li.
A fibred model chooses, for each i, one Kripke model for Li, and also provides way of jumping from worlds of other models into the model for i. Intuitively, evaluating 4yp at a world in model i either uses the native accessibility for the model if i, first jumps into model and then evaluates there 3| Formally, a fibred model M consists of one Kripke model m; for each logic C, together with family of logical fibring functions ft. Each fa maps each world in another model mj (j * i) to a world in m, while f; tells us how to jump from another component into the i-th one.
Satisfaction in fibred model M is defined follows. If w is world in m, then:
M, F p iff w is in the valuation of p in m;
M, } T always.
M,, F f1 A P2 iff M, w F F P1 and MM, w F 42.
M, w F u iff not M, w F
M, = 1 iff (i) = i and for all w/ with (w, w') in the accessibility relation of m,, we
have M :p: or (ii) j + and M, f,(w) - Dzp.
fibred logic for a fibring architecture: Let F be a fibring architecture. For each node e in F and each layer number f of A.,, associate distinct modal operator m.,e, interpreted over the class of all finite Kripke models; let be the resulting fibred logic. Based on L we will define another fibred logic C,= using the notion of compatible models, defined next.
Definition 4.1. Let m be Kripke model and N' network instance. A map that assigns to each world of m an input vector for A is (m,,N)adnisssiba if is injective and, for all worlds w, w',
w is related to w² in m = (N((ww) = (T(()))
Definition 4.2. Let M be a fibred model of L and denote with ma, the component Kripke model in M for node v in F and layer number e in A Let N = W.F,J), let x E {0, 1)", and let u be the root of F. We say that M is compatible with (N, x) if we can assign:
to each node v in F, a network instance N, of A.,. and
to each pair (v, E) of node in F and a layer in Ag, a bijection T., from a finite set of Kripke worlds finite set of vectors,
such that the following compatibility conditions hold:
In Kripke model, the accessibility relation can be any relation the of worlds, i.c. fully determined by a set of pairs of worlds. "e assume that the classes of models are disjoint so that each world's home model is unambiguous and we also assume that all component Kripke models are finite.
5

---

Published as a conference paper at ICLR 2026
(CO) Nu. / and Tu,1 maps each world w in m,,1 to the vector in {0, 13" whose i-th bit is 1 exactly when proposition pr is true at w.
(CI) Tue is (m,,e,Ny -admissible.
(C2) Assume v has children Ui..... 2k. ordered by the layer numbers i...., la labeling edges
(v, vz), and let w be the world reached via the composition of logical fibring functions from (TT,1) (x()) to Kripke model m.,1. Running (No, Fu, fo) on ne,1 (w) produces tuples M, h,) for Sis k. Then:
1. .r.. = NG and y; = Te,, (fr,a()
h, Te,. (fu.e, (w)).
-1 3. The set of propositions that are true at world To.4 (hx) in model mv,4 agrees with the set of propositions that are true at ),(,) (y:) in model mæj.1 for 1 iis k.
For fixed pair (v, E) of node in JF and layer number l in Ags let:
3N; x, .M a fibred model of L compatible with (N,, x) such that the (v, --component of M is m
Comp=(u,
In words, (o, E) is the projection of all compatible fibred models onto their (v, E) component. Proposition 4.3. The class Compy(u, E) is non-empty and closed under Kripke-mode isomorphism.
Proof. Non-empty. The class Comp E) contains at least the Kripke models of fibred models obtained by explicitly running the computation of fibred networks N vectors x.
Specifically, for each N F) and x, we can construct compatible fibred model as follows.
We start from the root model: the domain of the root model contains distinct element wa for each vector z E {0, 1)", two worlds W2, W'y' are related iff (z)) = (Z'z), and the valuation is given by: Pj holds at world W2 in the root model iff 2j = 1.
We the fibred neural network N on all vectors E {0, (recursively generating sequences of tuples Ng yı, h₂)) and we collect at each (v, f) all vectors attained by the computations, that is, for each (v, &,) we collect vectors h, and for each (2,, 1), we collect vectors y,. Furthermore, we run the fibred neural network A on the specific vector x and we collect at each v, the network instance M attained by the computation.
We then define Kripke models as follows: the domain of m,, contains a distinct element wy for each vector collected at (v, E). two worlds wy, wy are related iff (g the network instance collected at v.
(v) = =Att (v') where N,,
The valuations are defined recursively starting from the root model: a proposition p holds at world wh in model mo.e, iff there is world wy in M.,1 such that h h; is attained by the computation of (Ne, Fus (v)
(v) and p holds at wy in model m,, and proposition p holds world wy in model ma.11 iff there is a world wy in m such that y = y; is attained by the computation of (N,, Fr., (v) and holds at Wh, in model ma.f4
Finally, we require that the (logical) fibring function from m,,1 to my,4; verifies for each world my in 1,,1, fere, (wx) Wh, where h; is the vector attained by the computation of (Ne, Fv, fo)(v); and the (logical) fibring function from m.,1 m verifies, for each world wy in M.,1, Ju, (ww)
Wy: where y, is the vector attained by the computation of (N,, Fu, F.).
The above proof construction covers all compatibility conditions and ensures that the resulting fibred model is compatible with (N, x) by taking the bijections Tu. + v.
Closed under Kripke-model isomorphism. Let m E Comp= E) come from some compatible M, and let m z m' be an isomorphism. Form new fibred model M' by replacing the (v, f)- component of M with m' and replace the bijection To. by T,, o -1 This preserves (C2)-(C2): edges, valuations, and fibring jumps are transported through without changing any observable behavior. Hence M' is still compatible with the same (N, x), so m' Comp,(v,

---

Published as a conference paper at ICLR 2026
This shows that the subclass of compatible models is valid fibred logic, since the projections of compatible models represent a non-empty class of Kripke models closed under isomorphism (hence a reasonable class of Kripke models). We refer to this fibred logic as Ly.
Equivalence between fibring neural networks and a fragment of fibred logic:
Definition 4.4. Let F. be a fibring architecture and let be a propositional formula. The formula (1p,, F) CF recursively defined as follows:
If F has only single node, then ()(, sp
Otherwise, let ....... uk be the children of the root, with corresponding subtrees Fi.-.. Fk- For each i, let 4 be the largest layer label on an edge leaving v, (or 4 = if none). Then set
(l. = De,d F1) A ... Dvele Fx).
Theorem 4.5. Let F E & be a fibring architecture rooted u. For every network instance A of the root architecture Ann there is propositional formula y such that, for every input {0, 1)", for every collection of fibring functions f matching F. and every fibred model M compatible with (NFF. F.F) f) and x, we have that the following holds:
M, (T + () iff FN, classifies x as True.
Proof idea. In compatible fibred model, the accessibility relations between worlds mirror the behavior of network instances on their inputs (condition CI), and the fibring functions on worlds mirror the way a parent network delegates part of its computation children (condition C2). Thus evaluating the fibred network on x corresponds exactly to checking the truth value of the formula (yp, F) at the matching world, since both follow the same recursive structure given Definition 4.4
Proof. Fix a network instance N of the root architecture. Define the characteristic formula of N by
V
A h,=1
Pk PPp))
bE(O,1)": NOh20
h-=0
Fix F E 3, x E 10" and M compatible with (N, F) and x. We prove by in- duction on the depth of F that, for the world w = (zu,1) at the root: M, w F (),,F) iff (N,F, classifies x as true.
Base case (leaf). If F has only the root then (), yp and by (CO), at the root model mu.1. 1p satisfies: m,,1 uu,1 (h) = & if ((h) 0, E 10"
Induction step. Suppose the root has children 01,---,, uh with labels (4,, St), subtrees F, and f restrictions of f to F,, Run the root until layer é,, obtain x;; fibre to un by (Wi,y1) = R (xi); run the child fibred network F1, f1) yn; spisce its output back to get hy; and continue similarly for 2, ...... k. By (C1)-(22) and the semantics of Dy evaluating ((),, = A, De,,, ((,FF) at w amounts to evaluating each (1p, Fi) at the world reached by the corresponding fibring jump. By the induction hypothesis, each of those subformulas is true exactly when the corresponding child computation returns the vector that is spliced into the parent. Hence M, w -= (1(p, F) iff the overall fibred computation yields final root output 0, i.c.. iff F. classifies x truc.
APPLICATION TO NON-UNIFORM EXPRESSIVENESS GNNs, GATS AND TRANSFORMER ENCODERS
Graph Neural Networks. A Graph Neural Network (GNN) for A is a tuple G ((A HEr (B (b1) For each layer f, matrices A Xdixte- and B E Qdixde- weight matrices and vector be E Qdit is bias vector. A Graph Attention Network (GAT) g' for A contains all the elements of a GNN plus an additional collection {a V2' of attention vectors, where a² E d2 Both GNNs and GATs apply to undirected graphs G = EV, where a node vector x, E (0, 1 is associated to each node V and where the neighhorhood of node is defined
7

---

Published as a conference paper at ICLR 2026
as N(w) = for e V fu, 2) E). Their application to graph G with node vectors := (Xu) yields a sequence (xx) uev: (x=) of node vectors and the final result is graph with the same nodes and edges as G but with updated node vectors {x heev. When there is no ambiguity, we will refer x as G æ, u), the result at node u of applying GNN (or GAT) 9 to graph G with node features æ.
In the application of GNN & to G, x is defined, for each u E V, as x = = where xy x and h = B x + EvEN(u) A x + b". The application of GAT G' to G is defined analogously by replacing this expression with h = a B
+ a x b where the x -
attention coefficient ag is the component associated to node in the following vector:
hardmax(a" ET' (A x "II'B xx (EN())
(2)
The hardmax function applied to vector sets all occurrences of its largest value to the inverse of the number of its occurrences in the vector and all remaining components to O. The expression within the hardmax function is a vector with component for each node w E N(u) U {2} and where each component computed as the dot product of two vectors.
Transformer Encoders with Hard Attention. A Transformer encoder T for architecture A is defined similarly to a GAT as T = to specific types of input. While GATs are applied to arbitrary graphs, Transformer encoders are restricted to complete graphs, where each node is connected to every other node (Bronstein et al.) 2021). Additionally, the input graph for T is constructed from ordered sequence of tokens, with each token assigned a vector representation, which is then combined with a positional encoding vector construct a token feature. More precisely, for a complete graph with s nodes associated to a token sequence S of length each node is uniquely associated to a token at position E {o..... s- } in S and each token associated to token feature xę which is obtained as the sum X₃ vec(E)+ (t, s). where vec is a vector representation function mapping tokens vectors in {0, 1)do do and pos is positional encoding function mapping pairs of positions and sequence length to vectors in Qd The application of 'T S and token features æ == (xx)ees then obtained by applying expressions (5) and (2) to the complete graph with node features {xe Jees. We will also note T(S, æx, E), the result token & of applying Transformer encoder 'I to sequence S with token features (XE)EES, i.e. T(S, x {) is the application of Transformer encoder T to (S, g)
(B 1b' (a)) but is applicable only
Scope of technical results. In this paper, we restrict ourselves to GNNs and GATs with local sum aggregation, rational coefficients, and applied to Boolean vectors. Our technical results also assume that each of the truncated ReLU function mapping each component 2; of x to min(1, (1, max(0, (0, x.)). We also consider GATs and Transformers with hard attention only. To avoid repetitions, the technical results in this section will be stated for GATs, but they easily extend to GNNs and Transformer encoders, by considering that GNN is GAT without attention, and Transformer encoder is GAT on complete graphs with positional encodings.
If the output dimension of the GNN GAT (respectively, Transformer encoder) is 1, we can interpret them as node (respectively, token) classifiers: on input (G, x) (respectively, (S, x)), for each node u (respectively, for each token E). outputs true if x > 0 (respectively, x 0) and false otherwise. By abuse of notation, we sometimes write G x. u) true (or false) and the same for T(S, x, E).
5.1 FIBRED NEURAL NETWORKS CAN NON-UNIFORMLY DESCRIBE GNNS, GATS AND TRANSFORMER ENCODERS
The following result establishes that fibred neural networks provide a non-unifome description of GATs, i.c. given GAT G. for each input G, u, there is a different fibred neural network whose computation coincides with that of G. Interestingly, for given input (G, u), the fibring architecture is the same, and only the fibring functions vary for different node features æ. This property is key to derive the (non-uniform) logical expressiveness result.
Theorem 5.1. For every tuple T = (G, G, u), where G is a GAT with input/output dimensions n G (V, E) graph, and E V, there exist fibring architecture Fr, network instance N of the root architecure and a family 9, ( )a of collections of fibring functions matching F', indexed
8

---

Published as a conference paper at ICLR 2026
by possible node features (xe)ee,, such that, for all the fibred neural network (No F fi) applied to Xy computes G(G, x, u).
Proof idea. For each tuple (G, G, u), the tree structure of the corresponding fibring architecture is given by the unraveling tree of node u. in G at the depth of G. Indeed, a GAT computes recursively w.r.t. the depth of its unraveling tree, as do fibred neural networks w.r.t. the depth of their fibring architecture. At each node, the fibring function returns the node features of the neighboring nodes and assigns the weights of the relevant layer of G. the computation of the fibred neural network, the step of "replacing the entries in S; the vector x; by F,, (y:) ) is used to concatenate the outputs of the computations of the previous layer. The concatenation of outputs at the previous layer is then aggregated (or the attention layer is computed), using the relevant weights (or attention vectors) assigned by the fibring function upstream of the concatenation. The detailed proof is provided in the Appendix(A)
The same result holds for GNNs and Transformer encoders simply by removing the nodes and edges in the fibring architecture F that encode the GAT attention mechanism and from the fact that Transformer encoder is GAT applied to complete graph with positional encoding incorporated into token features (x&)ees-
5.2 GNNS, GATS AND TRANSFORMER ENCODERS AS FRAGMENTS OF FIBRED LOGICS
The following result establishes a non-uniform expressiveness result for GATs, characterized by a countably infinite family of formulas in the fragment of the fibred logic of interest.
Theorem 5.2. Let
UGGG,u), N FFr and 9, =ff }e be in Theorem 5.1 Denote u² the root F There exists a formula q- in Lyr such that for each x = (Xu)uEV, for each fibved model M compatible with (NT, F and Xw. the following holds:
ftt
M, (T (x.
iff G(G, x, u) true
Proof idea. It suffices to consider the fibred neural networks which reproduce the computations of G and to invoke the correspondence between fibred neural networks and our fibred logic. Since the formulas in our fibred logic only depend on the network at the root, and the fibring architecture, follows that the formula does not depend the node features.
Proof. Let r = (9, G, u) be tuple with G GAT with input/output dimensions n/1, G a graph and node in G. For each æ node features for G, consider fibred neural network Ng = (NT,FF) fi) obtained from Theorem [5.1]
By Theorem 4.5 applied to T and FT, there exists a propositional formula & such that for each fibred model M compatible with Ni and Xu, M, Furthermore by Theorem 5.1 Ng. (x..) 0 iff G(G, u) = true, which gives the result. L
(x.) } (1pp", FT) iff NY (x..) > 0.
The same result also holds for GNNs and Transformer encoders by replacing the fibring architecture FrT obtained from Theorem In particular, to incorporate positional encodings for Transformers, suffices to replace T.,1 by the bijection Tg.1 from worlds mę.1 to (pos(t, 8), + pos(l, 8)) where is the position of token & and is the length of the sequence.
DISCUSSION, CONCLUSION AND FUTURE WORK
For given instance G of neural architecture (a GNN, GAT or Transformer encoder), our non-uniform expressiveness results provide a countable family formulas that characterize the network instance. We note that the result of Cuenca Grau et al. (2025) bounded GNNs also implics a non-uniform expressiveness result in terms of first-order logic formulas: to construct countable family of formulas that characterize a GNN G, we can for example enumerate for & E N the first-order logic formula of the bounded GNN obtained by applying 9 to all graphs with degree
Closing the gap to uniform expressiveness requires collapsing, for each instance G. the corresponding family into a single formula in another logic. With the uniform expressiveness result of Benedikk al. (022)), already know that, for GNNs, the family must collapse to Presburger formula. The

---

Published as a conference paper at ICLR 2026
problem remains open for GAT's and Transformer encoders. In particular, for Transformer encoders only a lower bound of the resulting logic is known (Barcelo et al.) 2024).
We now present ideas towards the unification of uniform expresiveness results using fibring. Con- sider the countable family of fibred neural networks characterizing a GNN, given in the proof of Theorem [51] These fibred neural networks follow a common recursive structure, and by applying them to all possible input vectors x E {0, 1]", we can collect at each component (Kripke models of compatible fibred models) the vectors attained by the computations of the fibred neural networks, following the procedure in the proof of Proposition 4.3 Given the correspondence between the structure of the fibring architectures and the layers of the GNN (as seen in the proof of Theorem [5.]]. the set of vectors collected by this procedure is closely related to the E-spectrum of the GNN, defindd in Benedikt et al. (2024) as the set of all vectors attainable by the GNN at the ε-th layer when applied to all possible inputs. In particular, the finiteness of the 9-spectrum is key argument used in the derivation of their uniform expressiveness results. An idea would thus be to identify commonalities between the fibred formulas for different inputs associated to the same GNN, in order to map them to the single Presburger formula. Many technical details must be made precise to close this gap, and we leave this research future work. We believe, however, that the definition of fibring provided here will help systematize this investigation. Repeating the exercise to find commonalities in the fibred formulas for GAT's and Transformer encoders constitutes, in this way, new approach towards deriving uniform expressiveness results. The fibring formalism is expected to provide a unified lens, although non-uniform at this point, on the logical expressiveness of different network architectures. and might even hold the promise of offering common methodology to uncover expressiveness results in the future.
The intuition of fibred logics applied to neural architectures, viewing neural networks as combining underlying logics, is appealing and similar in spirit to the current trend in interpretability research which tries to break down network computations into several modular reasoning steps, e.g. (Ameisen al. 2025 He et al. 2025). We believe that scrutinizing the commonalities between fibred formulas for typical inputs, thereby reverse-engineering the fibred logical theories learned by neural networks, constitutes an exciting new take on the future possible extraction of interpretable logical rules capturing neural network's 'ss most relevant computations. Therefore, we posit that our approach to logical expressiveness via fibring may share common ground with interpretability research and hope that this paper will serve as a foundation in this direction. Furthermore, achieving uniform expressiveness results using the fibring formalism could enable new results on formal verification by leveraging existing results the complexity of modal and fibred logics, e.g. (Wu et al., 2015).
This paper is the first to establish the exact correspondence between fibring neural networks and fibring modal logies. The formalism has allowed us to derive non-uniform logical expressiveness results for several modern neural architectures. A gap remains unresolved to bridge non-uniform and uniform expressiveness results, and we hope our work will inspire further research in this direction. We think that fibring as formalism has the potential to enable the unification of expressiveness results for various network architectures, which were initially derived using different methodologies. with future applications in interpretability and verification.
REFERENCES
Emmanuel Ameisen, Jack Lindsey, Adam Pearce, Wes Gurnee, Nicholas L. Turner, Brian Chen, Craig Citro, David Abrahams, Shan Carter, Basil Hosmer, Jonathan Marcus, Michael Sklar, Adly Templeton, Trenton Bricken, Callum McDougall, Hoagy Cunningham, Thomas Henighan, Adam Jermyn, Andy Jones, Andrew Persic, Zhenyi Qi, T. Ben Thompson, Sam Zimmerman, Kelley Rivoire, Thomas Conerly, Chris Olah, and Joshua Batson. Circuit trac- ing: Revealing computational graphs in language models. Anthropic / Transformer-Circuit Blog preprint, March 27 2025. URL: /ttpp:: htttp:://transforneee circuits. sdrcuitts.uub2225. pub/2025/ atttribution-grappla wecaaphhspseee wwt.ttsthoooooo.oooooooo.....s.t .htt
Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan L. Reutter, and Juan Pablo Silva. The logical expressiveness of graph neural networks. In 8th International Conference on Learning Representations (ICLR), 2020.
Pablo Barcelo, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. Logical languages accepted by transformer encoders with hard attention. In The Twelfth International
10

---

Published as a conference paper at ICLR 2026
Conference Learning Representations, 2024.
id=gbrH2q077 7ma
Michael Benedikt, Chia- Lu, Boris Motik, and Tony Tan. Decidability of Graph Neural Networks via Logical Characterizations. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson (eds.), 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024), volume 297 of Leibniz International Proceedings in Informatics (LIPlcs), pp. 127:1-127:20, Dagstuhl, Germany, 2024. Schloss Dagstuhl Leibniz- für Informatik. ISBN 978-3-95977-322-5. doi: 11442300IPIIs.CCAALP222..11. URL https://droo IIc. ICALP 2024 127
Tarek R. Besold, Artur d' Avila Garcez, Sebastian Bader, Howard Bowman, Pedro Domingos, Pascal Hitzler, Kai-Uwe Kühhbberee,, Luís C. Lamb, Priscila Machado Vieira Lima, Leo de Penning, Gadi Pinkas, Hoifung Poon, and Gerson Zaverucha. Neural-Symbol Learning and Reasoning: A Survey and Interpretation, volume 342 of Frontiers in Artificial Intelligence and Applications, chapter 1, pp. 1-51. IOS Press, 2022.
Michael M. Bronstein, Joan Bruna, Taco Cohen, and Petar Velickovic. Geometric deep learning: Grids, groups, graphs, geodesies, and gauges. CoRR, abs/2104.13478, 2021. URL https?
//arxiv.orq/ abs abwp://bb//12..... 13478
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D. Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. In Advances in Neural Information Processing Systems, volume 33, pp.
1877-1901, 2020.
Brian F. Chellas. Modal Logic: An Introduction. Cambridge University Press, Cambridge, 1980. ISBN 9780521295154.
Bernardo Cuenca Grau, Eva Feng, and Przemyslaw A. Walega. The correspondence between bounded graph neural networks and fragments of first-order logic, 2025, URL https: /ttp://aavvv/..///// org/
abs 3bbs/2503 08021
Jacob Devlin, Ming- Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies. Volume 1 (Long and Short Papers), pp. 4171-4186. Association for Computational Linguistics, 2019.
Artur d' Avila Garcez and Lufs C. Lamb. Neurosymbolic AI: the 3rd wave. Artificial Intelligence (rrriw.566111:12227-1222 November 2023. doi: 10. 1001107777400422003--444444-44 URL https 023-10448
//doi.o2g/10.100077/55
Dov M. Gabbay. Fibring Logics. Clarendon Press, New York, 1999.
Artur S. d' Avila Garcez and Dov M. Gabbay, Fibring neural networks. In Proceedings of the 19th National Conference on Artifical Intelligence, AAAI'04, pp. 342-347, AAAI Press, 2004. ISBN 0262511835.
Martin Grohe. The descriptive complexity of graph neural networks. In 38th ACM/EEE Symposium on Logic in Computer Science (LICS), pp. 1-14, 2023, doi: 111109LICCS56622222...00000
Yiding Hao, Dana Angluin, and Robert Frank. Formal language recognition by hard attention trans- formers: Perspectives from circuit complexity. Transactions of the Association for Computational Linguistics, 10:800-810, 2022.
Yinhan He, Wendy Zheng, Yushun Dong, Yaochen Zhu, Chen Chen, and Jundong Li. Towards global-level mechanistic interpretability: A perspective of modular circuits of large language models. In Forty- International Conference on Machine Learning, 2025. URL https 7/openrevi wtw.
11

---

Published as a conference paper at ICLR 2026
Luis C. Lamb, Artur d' Avila Garcez, Marco Gori, Marcelo O. R. Prates, Pedro H. C. Avelar, and Moshe Y. Vardi. Graph neural networks meet neural-symbolic computing: A survey and perspective. In Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI), pp. 4877-4884, 7 2020. doi: 10.24963/jjai 2020/679. Survey track.
Pierre Nunn, Marco Sälzer, François Schwarzentruber, and Nicolas Troquard. A logic for rea-
soning about aggregate-combin graph neural networks. In Kate Larson (ed.), Proceedings of the Chirty-Thire International Joint Conference on Artificial Intelligence, IJCAI-24, pp. 3532-
3540. International Joint Conferences on Artificial Intelligence Organization, 8 2024. doi: 10.24963/jeeai.22249999 /iBL//tttpss//oo.orr//////
jjai. 2024/392 Main
Track.
OpenAl. GPT-4 technical report. arXiv preprint arXi::2303.08774 2023. URL htttttttt/ssxiii. arg/abs/2303. 08774
Amirreza Salamat, Xiao Luo, and Ali Jafari. Heterographrec: heterogeneous graph-based neural networks for social recommendations. Knowledge-Based Systems, 217:1068 17, 2021. ISSN 0950-7051. doi: hutps//ddboooo///looobl.oooooo..
URL https: www
sci rect. com http://.w.....eeeeaeaaaa.aaaaaaa 20055111000000000 800800
Moshe Y. Vardi and Pierre Wolper. Automata-theoretic techniques for modal logics of pro- grams. Journal of Computer and System Sciences, 32(2):183-22) 1986. ISSN 0022-0000.
doi: http://cioeesarrraaaaa/////00000 com/
URL https: www www.scinceeirrrttttttt
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. Attention all you need. Luxburg, S. Bengio. H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (eds.), Ad- vances in Neural Information Processing Systems, volume 30. Curran Associates, Inc.. 2017. URL https:://proceedinngge wwwp:eewwwereeeeeeeee....e F5l13355
Guyon, U. Von
fi wfl.ss/paper//0//
Yin Wu, Min Jiang, Zhongqiang Huang, Fei Chao, and Changle Zhou. An np-complete fragment of fibring logic. Annals Mathematics and Artificial Intelligence, 75(3-4):311-417, 2015. doi:
12.1007/s10472-015-9446
Jiacheng Xiong, Zhaoping Xiong, Kaixian Chen, Hualiang Jiang, and Mingyue Zheng. Graph neural networks for automated de novo drug design. Drug Discovery Today, 132-)333,--133,, 2021.
Zi Ye, Yogan Jaya Kumar, Goh Ong Sing, Fengyan Song, and Junsong Wang. comprehensive survey of graph neural networks for knowledge graphs. IEEE Access, 10.75728-75747,200 2022.
12

---

Published as a conference paper at ICLR 2026
A PROOF OF THEOREM 5.1
Let T (G. G. u) where g = (EA')=1 (B 1/ (V. E) is a graph with maximum degree and is a node in G.
(a is a GAT instance, G
Define A as the two-layer linear network whose first layer is the concatenation of m + identity matrices (with no bias) and the second layer is the concatenation of the matrix B and m times the matrix A L (with bias b²).
Definition A.1. Let G = E") be graph. A lazy walk in G is a finite sequence of nodes (uo, ... uk) such that for each E {1....,k} .k] u u, or (u--1, u.) E E. A lazy walk differs from a path in that one can stay on the same node multiple times.
Definition A.2. Let G (V, E) be graph, u E V, and L N. The (lazy) unravelling of node in G at depth L is the graph that is the tree having:
root
a node (u, u1,..., uz) for each lazy walk (u, u1....,uu! ue) in G with 1 < S L, and
edge between (u, U1,.... ue-1) and (u, u1,..., ue) when ue-1 = us or (ue-1, up) E É (assuming that uo is u).
The fibring architecture F is constructed from the lazy unravelling of u in G at depth L to which we add (in order to encode the attention mechanism) some nodes and edges in the following way: for each EE {1... ... }} (assuming that ug is u), each node (u, U1 ... Ug-1) 1) has extra child node ey., and we require that each node by has no child node. Note that by this construction, each node (u, u1.... ue) has [N(m)) 2 children nodes (namely the nodes (u, (1,01, .. ue, w) for {uz} UN(ee), and the node vz+1).
Let be node features for G.
The label of the edge between(u, Mi,... , Me-1) and (u, ui,...,, wz) is defined by layer number 1 and the set of positions designed the final output vector is the concatenation of the children computations. Its fibring function is as follows: on input the node feature x it returns the concatenation of vectors x" for w E {ue} (uu)) and a network with the relevant weights of layer f & designed so that, in the computation of the fibred network, the network N ((..aa).....))) applied to the concatenation of vectors h h4-441 for w E {ue} } U N(ue) returns the concatenation of uz).
A A o (h
(and B ah//-61) when
The label of the edge between (u. U1 u1..... 11-1) and dy is defined by layer number 2 and the set of positions is all positions of layer 2. Its fibring function takes as input vector y and returns the same vector y (self-fibring) and a network using the relevant attention vector a (and the bias) of layer I designed so that when y is the concatenation of vectors y for {uz} U N(ue), then No, (y) is the sum of vectors L--f. yu L-f (plus the bias b²-").
The neural architectures labelling nodes have the dimensions and nonlinearities required realise the networks described above (in particular, the neural architectures labelling nodes Uy uses the hardmax nonlinearity), and it is easy that the of neural architectures labelling nodes, layer numbers, and sets of positions labelling edges are fully determined by T (in particular, they do not depend on x).
As result, since Uy is a leaf node, it follows that, in the computation of the fibred network, the output vector node (u, #1,..... Me-1) is given by No, (y) where y is the concatenation of the children computations, i.e. from nodes (u, ui...., Me-1. ug)-
We prove by (descending) induction on the depth that the fibred network N (N F fn] verifies (x())) = h
Base (L- 1): By construction, each child computation is given by the concatenation of A | x2. (and
B' x(.) for E {WL-1} UN(uz-1), where 4 is neighbour reached at depth L 1 starting from the root u. Applying No, to the concatenation these children computations yields the sum of vectors 1 - A x (plus the bias b²), which is h h
13

---

Published as a conference paper at ICLR 2026
Induction step (L - é - 1): By inductive hypothesis, the output vector at each node (u, U...... ue) h.
I. where ug is a neighbour reached at depth starting from the root u. Computing the output at
node (u, u1........................ ue wt-1): )): by construction, each child computation thus given by the concatenation of A 1- oh -) (and B4-é+1 ohh--f)) for E {we-1} U N(ue-1). Applying No. to the h-t-! A 1--+1 xL-
concatenation of these children computations yields the sum of vectors aue (plus the bias b)- which is h4-441,
14


Reviews:
[{"review_id": "xL7mKK6voS", "reviewer": "Reviewer_ouqW", "summary": "This paper presents a formal correspondence between fibring modal logics and fibring neural networks and makes the following key contributions:\n1.  It defines the concept of compatible fibred models and proves that fibred neural networks can be interpreted as logical formulas in this framework\n2. It establishes non-uniform expressiveness results for Graph Neural Networks, Graph Attention Networks, and Transformer encoders.\n3. It suggests using fibring as a potential unifying formalism for studying logical expressiveness of different neural architectures.", "questions": "N/A", "limitations": "", "rating": 8, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. **Relevance**\nThe paper addresses a critical challenge: formally characterize the logical expressivity of various neural network architectures \n\n2. **Significance and Novelty**\nTo the best of my knowledge, the proposed approach is novel in its problem formulation, the formal correspondence  between fibring modal logics and fibring neural networks, and the important theoretical results established.  Fibring could potentially be very significant and serve as a unifying formalism for studying logical expressiveness of different neural architectures.\n\n3. **Soundness and Presentation**\nOverall, the paper is well organized and well written. The key theoretical results are formally proven.", "weaknesses": "I could not find any major weaknesses. \n\nOne minor error in the formal definition of the recursive computation of a fibred neural network: in line 169, \"N^{l_{i−1}:l_i} (**y_{i−1}**)\" should be replaced with   \"N^{l_{i−1}:l_i} (**h_{i−1}**)\". In order words,  h_{i-1} should be used instead of y_{i-1}. y_{i-1} is the input of the instance network of u_{i-1}. It is the output of that instance network combined with x_{i-1} (i.e., h_{i-1} ) that should directly be used to compute x_i", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Sa0YRghxoO", "reviewer": "Reviewer_mpQY", "summary": "The paper makes two key theoretical contributions. First, it establishes the connection between fibred neural networks and fibring modal logics. Specifically, the formulation relies on showing that evaluating the fibred network on an input is equivalent to checking the truth value of a formula in the fibring logic. Next, they apply this equivalence to derive logical expressiveness of well-known deep models such as GNNs, GATs and transformers. In particular, they focus on non-uniform logical expressiveness, i.e., is there a logical formula that coincides with with the output of the deep model depending on the input. The proof relies on showing that there exists a fibred network that produces the same input as the Graph Neural Network. Thus, using  the equivalence established between fibred neural networks and firing modal logic, the non-uniform expressiveness can be established.", "questions": "What are the practical implications of showing uniform vs non-uniform expressiveness of models? How would they potentially be useful in practice?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "Strengths\n+ Seems to be the first work to make the prove non-uniform expressiveness results for well known Deep models including transformers\n+ discovering the connection between fibring logics to prove logical expressiveness results could have implications on future theoretical results for more general logical expressiveness results which could be significant for interpretable AI.\nThe paper seems to make novel theoretical contributions that can prove useful in understanding why and how models like transformers can perform logical reasoning.", "weaknesses": "Weakness\n- While this is a theoretical paper, it would have been nice to provide some application benefits that could potentially result from these theoretical advances. \n- In terms of the presentation, it will be helpful to have maybe a summary of results that are known in logical expressiveness and what remains open problems, and how the proposed results addresses some of these. Section 6 describes this but it would be easier to understand the significance with a concise summary of the contributions.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "8tYeUXAUDa", "reviewer": "Reviewer_7tsZ", "summary": "This paper formally connects fibring of modal logics and fibring of neural networks, addressing a gap in the literature. It introduces fibred models compatible with neural networks and derives non-uniform logical expressiveness results for GNNs, GATs, and Transformers. The long-term goal, according to the authors, is to enable fibring as a tool for interpreting neural networks using computational logic.", "questions": "- What are the practical advantages of establishing a connection between fibring neural networks and fibring modal logic? Could the authors provide examples or use cases where this connection is beneficial?\n- The connection between fibring neural networks and GNNs is described as fuzzy. Could the authors provide a clearer explanation or additional examples to strengthen this link?\n- Theorems 5.1 and 5.2 discuss the existence of equivalent fibred neural networks. Could the authors provide guidance or methods for identifying or constructing these networks in practice?\n- How could the theoretical results be applied in real-world scenarios? Could the authors include experiments or simulations to demonstrate the practical implications of their findings?\n- The paper suggests that the results apply to Transformers, but the discussion focuses on GNNs and GATs. Could the authors clarify or expand on how their findings extend to Transformer architectures?\n- The paper derives non-uniform logical expressiveness results for GNNs, GATs, and Transformers. Could the authors clarify what non-uniform expressiveness entails and how it differs from uniform expressiveness in this context?\n- The authors mention a long-term goal of using fibring to interpret neural networks. Could they provide a roadmap or examples of how this interpretation might work in practice?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "- The paper presents a novel and rigorous mathematical proof connecting fibring modal logic and fibring neural networks, filling a gap in the literature.\n- It extends this framework to GNNs, GATs, and Transformers, which are widely used architectures in modern AI.\n- The theoretical foundation is solid, with clear definitions and formalizations of fibred models for neural networks.", "weaknesses": "- The practical relevance of connecting fibring neural networks to fibring modal logic is unclear. What are the advantages of this connection for real-world applications or further research?\n- Fibring neural networks are a niche approach in neuro-symbolic integration and are rarely used in practice. This raises concerns about the applicability of the paper’s findings.\n- The goal of connecting fibring neural networks and GNNs is not well-articulated. The connection feels fuzzy, and a clearer presentation is needed to justify its importance.\n- Theorems 5.1 and 5.2 prove the existence of a fibred neural network equivalent to a given GNN but provide no practical insights on how to identify or construct such a network. Additionally, the advantages of using the equivalent fibred neural network over the original GNN are unclear.\n- The paper claims its findings apply to Transformer architectures, but the discussion focuses on GNNs and GATs. While GATs and Transformers share connections, this is insufficient to generalize the results to Transformers.\n- The paper is purely theoretical, and the connection between fibring logic, fibred neural networks, and GNNs remains abstract. How can these results be applied in practice? Experiments or case studies would strengthen the paper’s impact.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "HKE0ki5gip", "reviewer": "Reviewer_k2Zz", "summary": "Fibring of neural networks was introduced as a neurosymbolic framework to integrate learning and reasoning within neural networks. This paper bridges the gap between the fibring of neural networks and the fibring of modal logics by formalizing fibred models that are compatible with fibred neural networks. Building on this foundation, the authors derive results on the non-uniform logical expressiveness of Graph Neural Networks (GNNs), Graph Attention Networks (GATs), and Transformer encoders.", "questions": "1. In line 191, what is meant by the “accessibility relation”? Could the authors provide a formal definition or illustrative examples to clarify this concept?\n2. The authors claim that non-uniform logical expressiveness results can be derived from several modern neural architectures. I wonder whether these models need to be pre-trained on specific datasets. \n3. Furthermore, what specific logical expressions can be derived from GNNs, GATs, and Transformers? Could the authors provide more illustrative examples or figures to demonstrate this derivation process?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "The paper establishes the connections between the fibring of neural networks and the fibring of modal logic. It provides a rigorous formalization linking fibred logic to fibred neural networks and demonstrates how this theory can be applied to widely used neural architectures, including GNNs, GATs, and Transformers, to enhance interpretability.", "weaknesses": "Although the paper is solid, some details are not explained clearly, making the overall presentation rather obscure. For instance, an illustrative figure for the fibred network could help clarify the concept. Please see the detailed questions below.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)