arXiv subjects

Veeti Ahvonen

Publications and source records attributed to Veeti Ahvonen.

8 recordsLinked to original sources

arXiv2026

Encoder-Decoder Transformers: Logical Characterizations and Periodicity

We give logical characterizations of encoder-decoder transformers, the foundational architecture for LLMs that also sees use in various settings that benefit from cross-attention, in the practical setting of floating-point numbers and soft attention. First, we characterize such transformers via a new temporal logic that extends propositional logic with a counting global modality over the encoder input and a past modality over the decoder input, as well as via a type of distributed automata. We consider three frameworks: with and without a final softmax step in the transformer, and in the setting where each model generates tokens via autoregression. Second, we show that both autoregressive transformers and sentences of counting propositional logic - the fragment of the previous logic obtained by omitting the past modality - recognize exactly the commutative star-free languages. Finally, we find that the sequences of tokens the transformers generate are ultimately periodic (and each token appears in the period at most once). This allows us to characterize autoregressive transformers via sentences of counting propositional logic that generate tokens without autoregression, i.e., we can effectively eliminate recursion from the transformers.

cs.LO↗

arXiv2026

Expressive Power of Graph Transformers via Logic

Transformers are the basis of modern large language models, but relatively little is known about their precise expressive power on graphs. We study the expressive power of graph transformers (GTs) by Dwivedi and Bresson (2020) and GPS-networks by Rampásek et al. (2022), both under soft-attention and average hard-attention. Our study covers two scenarios: the theoretical setting with real numbers and the more practical case with floats. With reals, we show that in restriction to vertex properties definable in first-order logic (FO), GPS-networks have the same expressive power as graded modal logic (GML) with the global modality. With floats, GPS-networks turn out to be equally expressive as GML with the counting global modality. The latter result is absolute, not restricting to properties definable in a background logic. We also obtain similar characterizations for GTs in terms of propositional logic with the global modality (for reals) and the counting global modality (for floats).

cs.LO↗

arXiv2025

Formula size game and model checking for modal substitution calculus

Recent research has applied modal substitution calculus (MSC) and its variants to characterize various computational frameworks such as graph neural networks (GNNs) and distributed computing systems. For example, it has been shown that the expressive power of recurrent graph neural networks coincides with graded modal substitution calculus GMSC, which is the extension of MSC with counting modalities. GMSC can be further extended with the counting global modality, resulting in the logic GGMSC which corresponds to GNNs with global readout mechanisms. In this paper we introduce a formula-size game that characterizes the expressive power of MSC, GMSC, GGMSC, and related logics. Furthermore, we study the expressiveness and model checking of logics in this family. We prove that MSC and its extensions (GMSC, GGMSC) are as expressive as linear tape-bounded Turing machines, while asynchronous variants are linked to modal mu-calculus and modal computation logic MCL. We establish that for MSC, GMSC and GGMSC, both combined and data complexity of model checking are PSPACE-complete, and for their asynchronous variants, both complexities are PTIME-complete. We also establish that for the propositional fragment SC of MSC, the combined complexity of model checking is PSPACE-complete, while for asynchronous SC it is PTIME-complete, and in both cases, data complexity is constant. As a corollary, we observe that SC satisfiability is PSPACE-complete and NP-complete for its asynchronous variant. Finally, we construct a universal reduction from all recursively enumerable problems to MSC model checking.

cs.LO↗

arXiv2025

Graph neural networks and MSO

We give an alternative proof for the existing result that recurrent graph neural networks working with reals have the same expressive power in restriction to monadic second-order logic MSO as the graded modal substitution calculus. The proof is based on constructing distributed automata that capture all MSO-definable node properties over trees. We also consider some variants of the acceptance conditions.

cs.LO↗

arXiv2025

Descriptive complexity for neural networks via Boolean networks

We investigate the expressive power of neural networks from the point of view of descriptive complexity. We study neural networks that use floating-point numbers and piecewise polynomial activation functions from two perspectives: 1) the general scenario where neural networks run for an unlimited number of rounds and have unrestricted topologies, and 2) classical feedforward neural networks that have the topology of layered acyclic graphs and run for only a constant number of rounds. We characterize these neural networks via Boolean networks formalized via a recursive rule-based logic. In particular, we show that the sizes of the neural networks and the corresponding Boolean rule formulae are polynomially related. In fact, in the direction from Boolean rules to neural networks, the blow-up is only linear. Our translations result in a time delay, which is the number of rounds that it takes to simulate a single computation step. In the translation from neural networks to Boolean rules, the time delay of the resulting formula is polylogarithmic in the size of the neural network. In the converse translation, the time delay of the neural network is linear in the formula size. Ultimately, we obtain translations between neural networks, Boolean networks, the diamond-free fragment of modal substitution calculus, and a class of recursive Boolean circuits. Our translations offer a method, for almost any activation function F, of translating any neural network in our setting into an equivalent neural network that uses F at each node. This even includes linear activation functions, which is possible due to using floats rather than actual reals!

cs.CC↗

arXiv2025

Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats

In pioneering work from 2019, Barceló and coauthors identified logics that precisely match the expressive power of constant iteration-depth graph neural networks (GNNs) relative to properties definable in first-order logic. In this article, we give exact logical characterizations of recurrent GNNs in two scenarios: (1) in the setting with floating-point numbers and (2) with reals. For floats, the formalism matching recurrent GNNs is a rule-based modal logic with counting, while for reals we use a suitable infinitary modal logic, also with counting. These results give exact matches between logics and GNNs in the recurrent setting without relativising to a background logic in either case, but using some natural assumptions about floating-point arithmetic. Applying our characterizations, we also prove that, relative to graph properties definable in monadic second-order logic (MSO), our infinitary and rule-based logics are equally expressive. This implies that recurrent GNNs with reals and floats have the same expressive power over MSO-definable properties and shows that, for such properties, also recurrent GNNs with reals are characterized by a (finitary!) rule-based modal logic. In the general case, in contrast, the expressive power with floats is weaker than with reals. In addition to logic-oriented results, we also characterize recurrent GNNs, with both reals and floats, via distributed automata, drawing links to distributed computing models.

cs.LO↗

arXiv2024

Graded modal logic and counting message passing automata

We examine the relationship of graded (multi)modal logic to counting (multichannel) message passing automata with applications to the Weisfeiler-Leman algorithm. We introduce the notion of graded multimodal types, which are formulae of graded multimodal logic that encode the local information of a pointed Kripke-model. We also introduce message passing automata that carry out a generalization of the Weisfeiler-Leman algorithm for distinguishing non-isomorphic graph nodes. We show that the classes of pointed Kripke-models recognizable by these automata are definable by a countable (possibly infinite) disjunction of graded multimodal formulae and vice versa. In particular, this equivalence also holds between recursively enumerable disjunctions and recursively enumerable automata. We also show a way of carrying out the Weisfeiler-Leman algorithm with a formula of first order logic that has been augmented with Härtig's quantifier and greatest fixed points.

cs.LO↗

arXiv2023

Descriptive complexity for distributed computing with circuits

We consider distributed algorithms in the realistic scenario where distributed message passing is operated via circuits. We show that within this setting, modal substitution calculus MSC captures the expressive power of circuits. The translations between circuits and MSC-programs are linear in both directions. Furthermore, we show that the colouring algorithm based on Cole-Vishkin can be specified via logarithmic size programs.

cs.LO↗