ABSTRACT. We study the expressive power of graph transformers (GTs) and GPS-networks, under both soft-attention and average hard-attention, by providing exact logical characterizations. In the setting with real numbers, GPS-networks have the same expressive power as graded modal logic with the (non-counting) global modality (GML+G), relative to vertex properties definable in first-order logic (FO). With floating-point numbers, GPS-networks are equally expressive as graded modal logic with the counting global modality (GML+GC), and this characterization is absolute (not restricted to FO-definable properties). Analogous results hold for GTs in terms of propositional logic with the global modality (PL+G) and its counting variant (PL+GC). A key insight is that the transition from reals to floats swaps relative global counting (possible with reals, lost with floats and with FO) for absolute global counting (impossible with reals, gained with floats).

ABSTRACT. We provide an extended summary of results in our preprint [ 1 ] in which we study the expressive power of message-passing aggregate-combine-readout graph neural networks (ACR-GNNs). Particularly, we focus on the first-order (FO) properties expressible by this formalism. While a tight logical characterisation remains a difficult open question, we make two contributions towards answering it. First, we show that sum aggregation and readout suffice for GNNs to capture FO properties that cannot be expressed in the logic C2 on both directed and undirected graphs. This strengthens known results by Hauke and Wałęga [2] where aggregation and readout functions are specially crafted for the task. Second, we identify two natural ways of restoring characterisability (with regard to C2) for ACR-GNNs. One option is to limit local aggregation (without imposing restrictions on global readout), whilst the second is to run ACR-GNNs over graphs of bounded degree (but unbounded size). In both cases, the FO properties captured by GNNs are exactly those definable by a formula in graded modal logic with global counting modalities. Our results thus establish an innate lower- and upper-bound in terms of how far (fragments of) C2 can be taken to characterise GNNs, and imply that is indeed the unbounded interaction of aggregation and readout that pushes the logical expressive power of GNNs above C

ABSTRACT. The Weisfeiler--Leman (WL) algorithm was originally introduced as a refinement procedure for analysing graph symmetries and as a tool for graph isomorphism testing. It distinguishes a large class of graphs up to isomorphism. For the k-dimensional WL algorithm, its indistinguishability power coincides with that of the finite-variable fragment of first-order logic with counting quantifiers, C_k. We study indistinguishability from an algebraic perspective. We introduce a program algebra with counting capabilities and a local version of k-WL, and show that both coincide in expressive power with the guarded fragment of counting logic, GC_k.

ABSTRACT. We compare the expressive power of state space models (SSMs) and recurrent neural networks (RNNs) in two domains: over words and over temporal graphs. Building on recent logical characterisations of SSMs via fragments of pure-past linear temporal logic (pLTLf), we lift the analysis to the graph domain. Our main results show that graph SSMs (GSSMs) are at least as expressive as the product logic pLTLf x K, combining pure-past LTL with graded modal logic over the neighbourhood, while recursive temporal graph neural networks (recTGNNs) capture the strictly stronger logic μTLf x K, a mu-calculus-style product logic. This mirrors the situation for words: SSMs recognise pLTLf-definable, i.e. star-free properties, whereas RNNs can simulate arbitrary finite automata and therefore recognise all regular properties. The structural parallel reveals a fundamental architectural boundary: the ability to compute fixpoints over sequences of arbitrary length lies beyond SSMs in both domains.

ABSTRACT. Neural networks are susceptible to adversarial examples---inputs with subtle perturbations that trigger erroneous outputs and potentially catastrophic failures. Neural network verification addresses this by formally checking whether given postconditions are entailed by specific preconditions. Most state-of-the-art verifiers rely on abstract interpretation to overapproximate neuron bounds layer by layer, utilizing branch-and-bound methods to achieve completeness. However, a significant gap exists between theoretical soundness and practical implementation: standard floating-point arithmetic introduces rounding errors that accumulate during computation, potentially leading to unsound verification results. While the continuous constraint solving community has long addressed numerical inaccuracies by accounting for floating-point rounding errors, this rigorous treatment is not yet widespread in neural network verification. Our preliminary experimental results demonstrate that unsoundness issues manifest in several state-of-the-art neural network verifiers. To bridge this gap, we propose JET, a GPU-based sound continuous constraint solver. JET integrates sound floating-point interval arithmetic with constraint propagation and a search method, providing a framework that guarantees numerical soundness while leveraging the parallel performance on GPU.

ABSTRACT. We present IsaGrad, a formalisation of reverse automatic differentiation (RAD) over mutable computational graphs using the Imperative HOL library of Isabelle, and verify its functional correctness using separation logic. We use IsaGrad as the differentiation engine for two machine learning case studies: training a multi-layer perceptron and a recurrent neural network. Leveraging Isabelle's code generation, we extract imperative-style Haskell programs where the training process is backed by our verified algorithm. To our knowledge, our implementation is the first of its kind to prove the functional correctness of an imperative, heap-based RAD algorithm. Beyond showcasing Imperative HOL’s expressiveness, this work demonstrates how formal verification increases confidence in computational graphs used for gradient-based optimisation, including neural network training.

ABSTRACT. Neural networks are a fundamental aspect of modern artificial intelligence, playing a key role in various important machine learning architectures including transformers and graph neural networks. Recently, logical characterisations have been used to study the expressive power of many machine learning architectures, but logical characterisations of plain neural networks have received less attention. In this paper, we provide fuzzy logic characterisations of rational-weight ReLU-activated neural networks via two well-established fuzzy logics: Rational Pavelka Logic RPL (and extensions thereof) and (fragments of) LΠ½. The activation values of the neural networks are allowed to be arbitrary real numbers. We also provide fuzzy logic characterisations of a generalised polynomial ring over ℚ in countably many variables where the use of the ReLU-function is permitted.

ABSTRACT. This paper presents an overview of a line of research on representing neural networks in Łukasiewicz logic and applying this representation to formal property verification. The approach relies on the correspondence between neural network computations and rational McNaughton functions, enabling the translation of certain neural architectures into logical formulas. We summarize previously published results on the logical representation of ReLU–TId neural networks and on the encoding of reachability and robustness properties in Łukasiewicz logic.

ABSTRACT. Neural networks can be used as powerful predictors, but they are opaque. This is a serious drawback when they are used in areas such as medical diagnosis, where decisions must be auditable. In this paper, we present a pipeline that turns a trained neural network into a small set of human-readable logical rules, and then rebuilds those compiled rules back into a neural-symbolic network with fixed rules for interpretable prediction. Starting from a standard feed-forward classifier, we extract rule-based specifications using an existing symbolic knowledge extraction tool, and recompile them into a differentiable logic model in which logical operations such as conjunction, disjunction, and numerical inequalities are realised as smooth layers. Rulesets extracted in this way are typically large and contain redundancies. We therefore introduce a selection procedure that combines systematic rule removal with a contribution measure based on Shapley values adapted from cooperative game theory, allowing us to identify the rules that genuinely drive predictions. On a clinical classification task, the pipeline compresses the original network into just four rules while retaining 92% predictive accuracy, yielding a compact and interpretable approximation of the original model. Broader empirical validation across further domains is left to future work.