研究基于集合聚合的循环图神经网络
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.
This report is categorized under AITOP's "Papers" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Key entities and technical topics under continuous tracking include Recurrent GNNs, graph neural networks, formal verification.
Source attribution: curated from arXiv cs.AI (@Blai Bonet).
