提出可终止的循环图神经网络，能表达所有可定义的节点分类任务。
Halting Recurrent GNNs and the Graded $μ$-Calculus
- 设计新机制让循环GNN自动停止，无需知道图大小。
- 模型可表达所有在分级μ-演算中可定义的节点分类结果。
- 适合研究GNN表达能力与逻辑关系的学者参考。
图神经网络（GNN）是处理图结构数据的机器学习模型，其表达能力与在分级双模拟下不变的逻辑密切相关。现有循环GNN要么假设模型已知图大小，要么缺乏终止保证。本文提出一种循环GNN的终止机制，证明该模型即使对图大小无感知，也能表达所有在分级模态μ-演算中可定义的节点分类器。为证明核心结论，我们构建了分级μ-演算的新近似语义，具有独立价值。基于此语义，提出一种无须依赖图大小的计数型模型检测算法，并证明该算法可由一个终止的循环GNN实现。
原文摘要 · Abstract (English)
Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for recurrent GNNs. We prove that our halting model can express all node classifiers definable in graded modal mu-calculus, even for the standard GNN variant that is oblivious to the graph size. To prove our main result, we develop a new approximate semantics for graded mu-calculus, which we believe to be of independent interest. We leverage this new semantics into a new model-checking algorithm, called the counting algorithm, which is oblivious to the graph size. In a final step we show that the counting algorithm can be implemented on a halting recurrent GNN.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。