证明量化图神经网络验证极难但可判定，为安全评估提供理论基础。
Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
- 构建逻辑语言形式化量化图神经网络行为
- 证明验证任务为(co)NEXPTIME完全，计算上极难
- 实验显示量化模型轻量且保持良好精度与泛化能力
我们提出一种用于推理带有全局读出的量化聚合-组合图神经网络（ACR-GNNs）的逻辑语言。通过逻辑表征，我们证明了带有读出的量化GNN的验证任务属于(co)NEXPTIME完全类。这一结果表明量化GNN的验证在计算上高度不可行，推动了对GNN系统安全性保障的研究。实验还表明，量化后的ACR-GNN模型在保持与非量化模型相当的准确率和泛化能力的同时，具有更轻的计算开销。
原文摘要 · Abstract (English)
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 quantized GNNs with readout are (co)NEXPTIME-complete. This result implies that the verification of quantized GNNs is computationally intractable, prompting substantial research efforts toward ensuring the safety of GNN-based systems. We also experimentally demonstrate that quantized ACR-GNN models are lightweight while maintaining good accuracy and generalization capabilities with respect to non-quantized models.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。