LIBMG: A Python library for programming graph neural networks in μG

Graph neural networks have proven their effectiveness across a wide spectrum of graph-based tasks. Despite their successes, they share the same limitations as other deep learning architectures and pose additional challenges for their formal verification. To overcome these problems, we proposed a specification language, μG, that can be used to program graph neural networks. This language has been implemented in a Python library called LIBMG that handles the definition, compilation, visualization, and explanation of μG graph neural network models. We illustrate its usage by showing how it was used to implement a Computation Tree Logic model checker in our previous work, and evaluate its performance on the benchmarks of the Model Checking Contest. In the future, we plan to use μG to further investigate the issues of explainability and verification of graph neural networks.