研究基于集合聚合的循环图神经网络
Recurrent GraphNeural NetworkswithSet-BasedAggregation
这篇论文对研究图神经网络和形式化验证的工程师来说很有价值，因为它提供了一种新的方法来构建和解释循环图神经网络。
本文提出一种新的循环图神经网络（Recurrent GNNs）模型，使用集合聚合（set-based aggregation）方法。研究证明，在满足特定条件下，该模型可以编译为模态μ-演算B$Σ^{\circ}_1$片段的布尔闭包，从而实现从网络权重到符号解释的可验证路径。
Recurrent GraphNeural NetworkswithSet-BasedAggregation
Recurrent GNNs iterate message passing to convergence, and their logical characterizations to date rely on multi-set aggregation, graded (counting) logics, and halting or acceptance conditions that cannot be verified from the network's parameters. We study recurrent GNNs with set-based aggregation and identify sufficient conditions checkable from the weights for networks to compile into formulas and formulas into networks. The main result is an effective, two-directional equivalence between a class of networks and the Boolean closure of reachability and safety properties, the fragment B$Σ^{\circ}_1$ of the modal $μ$-calculus. The fragment is not an artifact: it is the exact expressive level of stabilization over finite vocabulary, which supports fixed points of a single polarity and Boolean combinations thereof, but not the composition of fixed points of opposite polarities. The correspondence needs no counting logic, no external halting signal, and no non-effective acceptance condition, yielding a verifiable path from weights to symbolic explanations for networks meeting the conditions.
