From Neural Networks to Logical Theories: The Correspondence between Fibring Modal Logics and Fibring Neural Networks
This work provides a foundational link between neurosymbolic AI and computational logic, potentially aiding in interpreting neural network theories, though it is incremental in formalizing existing ideas.
The paper establishes a formal correspondence between fibring of neural networks and fibring of modal logics, enabling the derivation of non-uniform logical expressiveness results for Graph Neural Networks, Graph Attention Networks, and Transformer encoders.
Fibring of modal logics is a well-established formalism for combining countable families of modal logics into a single fibred language with common semantics, characterized by fibred models. Inspired by this formalism, fibring of neural networks was introduced as a neurosymbolic framework for combining learning and reasoning in neural networks. Fibring of neural networks uses the (pre-)activations of a trained network to evaluate a fibring function computing the weights of another network whose outputs are injected back into the original network. However, the exact correspondence between fibring of neural networks and fibring of modal logics was never formally established. In this paper, we close this gap by formalizing the idea of fibred models \emph{compatible} with fibred neural networks. Using this correspondence, we then derive non-uniform logical expressiveness results for Graph Neural Networks (GNNs), Graph Attention Networks (GATs) and Transformer encoders. Longer-term, the goal of this paper is to open the way for the use of fibring as a formalism for interpreting the logical theories learnt by neural networks with the tools of computational logic.