6 papers
The Complexity of Verifying Feedforward Neural Networks in Quantised Settings
Eric Alsmann, Martin Lange, Marco Sälzer
We investigate the computational complexity of neural network verification in quantised settings. We distinguish three classes of Feedforward Neural Networks (FNNs): rational FNNs…
The Polynomial Counting Capabilities of Message Passing Neural Networks
Marco Sälzer, Pascal BergsträÃer, Anthony W. Lin
The counting power of Message Passing Neural Networks (MPNN) has been the subject of many recent papers, showing that they can express logic that involves counting up to a threshol…
The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics
Marco Sälzer, PrzemysÅaw Andrzej WaÅÄga, Martin Lange
In recent years, the expressive power of various neural architectures -- including graph neural networks (GNNs), transformers, and recurrent neural networks -- has been characteris…
Verifying Quantized Graph Neural Networks is PSPACE-complete
Marco Sälzer, François Schwarzentruber, Nicolas Troquard
In this paper, we investigate the verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-co…
A Logic for Reasoning About Aggregate-Combine Graph Neural Networks
Pierre Nunn, Marco Sälzer, François Schwarzentruber +1
We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We…
Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
Marco Sälzer, Eric Alsmann, Martin Lange
We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or i…