μG: A Process Algebra for Graph Neural Networks（图神经网络的进程代数）

《Journal of Logical and Algebraic Methods in Programming》：The μ G language for programming graph neural networks

　　

本文提出μG（muG，A Process Algebra for Graph Neural Networks），一种基于进程代数（Process Algebra）的形式化建模框架，用于对图神经网络（Graph Neural Network, GNN）的消息传递层与组合结构进行严格定义与推理。研究人员给出了μG语法的抽象语法、指称语义（Denotational Semantics）及结构化操作语义（Structural Operational Semantics, SOS），证明了两种语义等价、操作语义强合流（Strong Confluence）以及类型可靠性（Type Soundness）。该语言支持恒等（ι）、节点特征变换（ψ）、前像（pre-image ?σγ）与后像（post-image ?σγ）消息传递、顺序复合（;）、并行复合（∥）、条件选择（⊕）及迭代固定点算子（N★），并引入let/def宏、if-then-else及带初值的fixpoint与repeat循环等语法糖。研究人员还证明相关函数复合、平行复合及条件算子在链完备偏序集上连续，保证最小不动点（least fixed point）良定义与收敛性（?-近似判定谓词??）。该形式化框架可用于验证GNN架构的正确性并指导可解释GNN设计。

论文解读：μG——一种面向图神经网络的进程代数

研究背景与动机

现有图神经网络（Graph Neural Network, GNN）多采用消息传递神经网络（Message Passing Neural Network, MPNN）范式，通过若干轮邻域聚合与节点更新实现图表示学习。然而当前GNN模型缺乏统一且严格的形式化规范语言，难以对GNN层的组合、迭代、并行执行及终止性进行精确推理与验证，亦不利于比较不同架构的表达力。为弥补这一缺陷，研究人员提出了一种受进程代数（Process Algebra）启发的领域特定语言μG（muG），旨在以数学严谨的方式描述GNN的计算流程，建立其指称语义（Denotational Semantics）与结构化操作语义（Structural Operational Semantics, SOS），并证明二者等价及系统具备类型可靠性（Type Soundness）。该工作发表于《Journal of Logical and Algebraic Methods in Programming》。

主要关键技术方法

研究人员首先定义μG的抽象语法：包含恒等ι、函数应用ψ、带边/消息/聚合函数符号的前像?_σ^γ（incoming message passing）与后像?_σ^γ（outgoing message passing）、顺序复合N₁;N₂、并行复合N₁∥N₂、条件选择N₁⊕N₂及Kleene星迭代N^★，优先级为^★> ; > ∥ > ⊕。指称语义将GNN解释为节点标注函数空间Φ_G,ξ上的映射，给出各构造的归纳定义，其中?/?分别用消息函数f_γ与聚合函数f_σ对入/出邻域多集合做变换，迭代采用最小不动点算子FIX(λ?. cond(test, id, ? ° S_ds|[N|]))，收敛性由?-近似相等谓词x ?_?y（精确相等或数值向量逐分量差≤?）控制。操作语义以配置?N, η?上的迁移关系→_G,ξ给出SOS规则，含并行分支的叉积状态N₁?N₂与投影π_L/π_R，选择算子依据左投影是否全True决定分支。随后研究人员证明：(1) SOS的强合流性（Strong Confluence），即不同PAR规则应用顺序终归至相同可达终端状态；(2) 函数复合、平行复合与cond算子在链完备偏序集上连续（Lemmata 5.1–5.4），确保FIX良定义；(3) 指称语义与操作语义等价（Theorem 5.4：S_ds|[N|] = S_sos|[N|]），通过双向偏序嵌入证明；(4) 类型系统（Table 2）保障良类型（well-typed）μG项总映射到合法GNN函数（Type Soundness）。此外引入变量赋值let X=N in N'、函数定义def、if-then-else宏（(N₁∥ι);(N₂⊕N₃)）及带初值fixpoint（fix X=N in N'）与定次repeat循环作为语法糖。

研究结果

5.1 Denotational Semantics（指称语义）

研究人员定义语义解释函数S_ds|[·|]_G,ξ: N → Φ_G,ξ，将μG项映射为节点标注函数到节点标注函数的映射。ι解释为id；ψ解释为λv.f_ψ(η(V), η(v))，可同时捕获全局多集合与局部标注，分别特化为纯逐点变换或全局池化（global pooling）；?_σ^γ对每个节点v收集入邻域(u,v)经f_γ(η(u), ξ((u,v)), η(v))产生的消息多集合{{…}}，再经f_σ(MsgMultiset, η(v))生成新标注，?对称处理出邻域；顺序复合为函数复合S_ds|[N₂|] ° S_ds|[N₁|]；平行复合为直积×；选择为cond(π_L全True, S_ds|[N₁|]°π_R, S_ds|[N₂|]°π_R)；星迭代为FIX(λ?. cond(ληλ v. S_ds|N|(v) ?_?η(v), id, ? ° S_ds|[N|]))。N₁?N₂辅助定义为(S_ds|[N₁|]°π_L) × (S_ds|[N₂|]°π_R)。定理5.1证明FIX中泛函连续（依赖Lemmata 5.1–5.4），定理5.2保证S_ds|[·|]良定义。

5.2 Operational Semantics（操作语义）

配置?N, η?经→_G,ξ单步归约，表1列出ID（ι返回η）、APPLY（ψ生成含ι与λv.f_ψ(…)的对）、PREIMG/POSTIMG（展开?/?为消息收集与聚合）、SEQ₁/SEQ₂（先归约左部至ι再转右）、SPLIT（∥拆为N₁?N₂配双份η）、PAR₁/PAR₂（?中任一方可单步推进，保留另一投影）、MERGE（ι?ι合并回ι,η）、CHOICE₁/CHOICE₂（依π_L(η)是否全True选N₁或N₂，传入π_R(η)）、STAR（N^★展开为一轮( (ι∥N);ψ_??∥ι );( ι⊕N;N^★)）。S_sos|N|取?N,η?经→_G,ξ^★到达ι,η'时的η'，否则全底。定理5.3证明强合流：PAR₁与PAR₂对?的不同推进可经一步互相追齐至共同后继。

5.3 Language Macros（语言宏）

引入let X = N in N'（句法替换）、def F(X₁,…,X_k){N} in N'（函数宏替换）、if C then N₂else N₃≡ (C∥ι);(N₂⊕N₃)、fix X=N in N'（将初值N与常量预计算子表达式并行传入星迭代，用投影替换X与常量标识符）及repeat N for k（计数器初始化为零，用< />

5.4 Equivalence of Operational and Denotational Semantics（语义等价性）

引理5.5证明??N,η?→^★η' ? S_ds|N|=η'（操作语义推导蕴含指称语义结果），引理5.6反之证明指称语义结果被操作语义可实现（在偏序意义下），从而定理5.4得S_ds|[N|]=S_sos|[N|]。

5.5 Type Soundness（类型可靠性）

类型环境Γ ? N : Φ_G,ξ[T_in, T_out]经Table 2规则推导，要求ψ、γ、σ具匹配类型（f_ψ:T₁^★×T₁→T₂，f_γ:T₁×T_ξ×T₁→T₂，f_σ:T₂^★×T₁→T₃），顺序复合要求中间类型匹配，平行复合积类型，选择要求左右分支同输入输出类型，星要求N具相同输入输出类型。由此可证良类型μG项经SOS归约保持类型且最终映射到Φ_G,ξ中合法函数，即类型可靠性成立。

讨论与结论

研究人员建立了首个将GNN完整计算流程（含消息传递、层组合、并行、条件分支及迭代不动点）形式化的进程代数μG，严格定义了指称语义与结构化操作语义并证明其等价性与类型可靠性。该框架为GNN架构提供数学精确描述手段，可用于比较不同GNN变体表达力、验证特定GNN性质（如终止性、等价性）及指导可验证GNN编译器或中间表示（Intermediate Representation, IR）设计。?-近似判定与有限截断机制兼容实际训练中迭代层数上限设定。未来工作可包括扩展至异构图（heterogeneous graph）、引入注意力机制（attention mechanism）的形式化及基于μG的GNN验证工具实现。