Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
Artem Chernobrovkin, Marco Sälzer, François Schwarzentruber, Nicolas Troquard
Published in KR, 2026
We introduce a logic for quantized graph neural networks that combine local aggregation with global readout. It gives a precise way to reason about these models and establishes (co)NEXPTIME-completeness for verification tasks. Experiments also examine how quantization affects model size, accuracy, and generalization.
An earlier preprint was titled Verifying Graph Neural Networks with Readout is Intractable.