Verifying Quantized Graph Neural Networks is PSPACE-complete

Marco Sälzer, François Schwarzentruber, Nicolas Troquard

Published in IJCAI, 2025

We study the verification of graph neural networks whose numerical values use fixed-width arithmetic. We formulate a validity problem with linear constraints, translate it into a logical language, and provide a proof system. Matching upper and lower bounds establish PSPACE-completeness.