验证带有读出层的量化图神经网络是可判定但高度不可行的
Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
AI总结：
本文提出一种逻辑语言用于推理带有全局读出的量化聚合-结合图神经网络（ACR-GNNs），证明其验证任务为（co）NEXPTIME完全问题，表明量化GNN的验证计算上不可行，同时实验显示量化ACR-GNN模型轻量且保持良好精度和泛化能力。
摘要：
我们介绍了一种逻辑语言，用于推理带有全局读出的量化聚合-结合图神经网络（ACR-GNNs）。我们提供了逻辑特征，并利用其证明带有读出的量化GNN的验证任务是（co）NEXPTIME完全的。这一结果表明，量化GNN的验证在计算上是不可行的，促使大量研究致力于确保基于GNN的系统安全。我们还通过实验表明，量化ACR-GNN模型在保持良好精度和泛化能力的同时，具有轻量的特点。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
