Presenting Neural Networks via Coherent Functors

TL;DR

This paper introduces a novel approach to representing neural networks as coherent categories, framing inference as a formal extension problem within category theory, bridging machine learning and logical theories.

Contribution

It develops a categorical framework that models neural networks as coherent categories, enabling formal reasoning about network inference and architecture.

Findings

Neural networks can be represented as models of coherent theories.

Inference corresponds to a lifting problem in the 2-category of coherent categories.

Framework encompasses various architectures including sparse and convolutional networks.

Abstract

This paper develops a methodology for representing machine learning models as models of formal theories, grounded in the perspective that machine learning models are a form of database and that databases are models of theories in coherent logic. Two intermediate results support this approach: any functorial database schema has an associated $\kappa$-coherent theory whose models coincide with its instances, and data may be hard-coded into a coherent category such that any model of the resulting theory necessarily contains it. These tools are used to show that any dense feed-forward neural network architecture over the floating point numbers may be presented as a coherent category $G$ whose $Set$-models are the networks of that architecture, with inference arising as the precomposition functor $Coh(\iota, Set)$ along a coherent functor $\iota : RSpan(a_0, a_n) \rightarrow G$. This representation is extended to networks with weight and bias fixing and tying, encompassing sparse and convolutional architectures, via a 2-coequaliser construction in $Coh_\sim$. Taken together, these results recast neural network inference as an extension problem in the 2-category $Coh_\sim$ of coherent categories, supporting the interpretation of a network architecture as a formal hypothesis about the structure of data and of model training as a lifting of a dataset into a more constrained theory.