证明量化图神经网络验证是计算上极难的，属PSPACE完全问题。
Verifying Quantized Graph Neural Networks is PSPACE-complete
- 提出线性约束有效性问题（LVP）来形式化验证量化GNN
- 证明该问题在合理激活函数下属于PSPACE类
- 揭示其计算复杂性，适合研究推理安全与理论边界的人
本文研究量化图神经网络（GNNs）的验证问题，其中数值采用固定位宽的算术表示。我们引入线性约束有效性（LVP）问题以验证GNN性质，并提供将LVP实例高效转化为逻辑语言的方法。我们证明了在任意合理的激活函数下，LVP属于PSPACE。同时，我们构建了一个证明系统，并证明其PSPACE-hardness，表明虽然量化GNN的推理是可行的，但整体上仍具有很高的计算挑战性。
原文摘要 · Abstract (English)
In this paper, we investigate the 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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。