Graph neural networks form a class of deep learning architectures specifically designed to work with graph-structured data. As such, they share the inherent limitations and problems of deep learning, especially regarding the issues of explainability and trustworthiness. We propose $\mu\mathcal{G}$, an original domain-specific language for the specification of graph neural networks that aims to overcome these issues. The language's syntax is introduced, and its meaning is rigorously defined by a denotational semantics. An equivalent characterization in the form of an operational semantics is also provided and, together with a type system, is used to prove the type soundness of $\mu\mathcal{G}$. We show how $\mu\mathcal{G}$ programs can be represented in a more user-friendly graphical visualization, and provide examples of its generality by showing how it can be used to define some of the most popular graph neural network models, or to develop any custom graph processing application.

翻译：图神经网络构成了一类专门设计用于处理图结构数据的深度学习架构。因此，它们也继承了深度学习固有的局限性和问题，尤其是在可解释性和可信度方面。我们提出了 $\mu\mathcal{G}$，一种用于规范图神经网络的原创领域特定语言，旨在克服这些问题。本文介绍了该语言的语法，并通过指称语义严格定义了其含义。同时，还提供了以操作语义形式表达的等价刻画，并结合类型系统，用于证明 $\mu\mathcal{G}$ 的类型可靠性。我们展示了如何以更用户友好的图形可视化方式表示 $\mu\mathcal{G}$ 程序，并通过展示如何使用它来定义一些最流行的图神经网络模型，或开发任何自定义的图处理应用，来证明其通用性。