Publications

TL;DR: We use compressed strings to derive tighter bounds on transformer length generalization and to explain apparently conflicting evidence about the C-RASP hypothesis.

TL;DR: We map the complexity of verifying feedforward networks under finite-width arithmetic. Verification remains NP-complete at fixed precision, while the choice of specification language matters for more general settings.

TL;DR: We identify when message passing neural networks can express polynomial counting constraints, with results for global properties, local properties, and nested modalities.

TL;DR: A logical characterization of quantized GNNs with global readout makes verification decidable, but the associated tasks are (co)NEXPTIME-complete.

TL;DR: Transformers can express counting conditions defined by polynomial inequalities, going beyond linear counting. This also yields an undecidability result for a simple transformer model without positional encodings.

TL;DR: We represent neural network input-output behavior exactly with weak Büchi automata, enabling automata-based verification and interpretation.

TL;DR: We establish (some) characterisations of the expressive capabilities of different TGNN models based on product logics.

TL;DR: We translate verification questions for graph neural networks using fixed-width arithmetic into logic and prove that the problem is PSPACE-complete.

TL;DR: We investigate the challenges and possibilities of formal reasoning for encoder-only transformers (EOT) by examining their satisfiability problem (SAT). We find SAT is undecidable for general EOT but identify decidable and NEXPTIME-hard scenarios for quantized EOT, highlighting the complexity of these cases.

TL;DR: We introduce a modal logic incorporating counting modalities into linear inequalities and demonstrate that each formula can be converted into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be efficiently transformed into formulas and that the satisfiability problem is PSPACE-complete, enabling polynomial space solutions for various applications like GNN querying and equivalence checking.

TL;DR: We prove that formal verification of different safety properties of graph-classifying MPNN is impossible in general and that verification problems for node-classifying GNN are solvable if the considered graphs have bounded degree.

TL;DR: We give a thorough proof for the NP-completeness of verifying output reachability of NN and show that the problem remains NP-hard if restricted to one-layered NN of minimal dimensionality.

TL;DR: We show that there are structures with infinite bisimulation quotient that ensure finite convergence of all mu-calculus formulas.