Verifying Quantized Graph Neural Networks is PSPACE-complete
In this paper, we investigate verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs properties, and provide an efficient translation from LVP instances into a logical language. We show that LVP is in PSPACE, for any reasonable activation functions. We provide a proof system. We also prove PSPACE-hardness, indicating that while reasoning about quantized GNNs is feasible, it remains generally computationally challenging.
Code (0)
등록된 구현이 없습니다.
Tasks
TranslationSimilar Papers 제목 키워드 기반
Scalable Verification of Quantized Neural Networks (Technical Report)
Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for …
Computational EfficiencyQuantizationVerifying Quantized GNNs With Readout Is Decidable But Highly Intractable
We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for …
Containment of Simple Regular Path Queries
Testing containment of queries is a fundamental reasoning task in knowledge representation. We study here the containment problem for Conjunctive Regular Path Queries (CRPQs), a navigational query language extensively us…
On verifying expectations and observations of intelligent agents
Public observation logic (POL) is a variant of dynamic epistemic logic to reason about agent expectations and agent observations. Agents have certain expectations, regarding the situation at hand, that are actuated by th…
Winning the War by (Strategically) Losing Battles: Settling the Complexity of Grundy-Values in Undirected Geography
We settle two long-standing complexity-theoretical questions-open since 1981 and 1993-in combinatorial game theory (CGT). We prove that the Grundy value (a.k.a. nim-value, or nimber) of Undirected Geography is PSPACE-com…