Presenting Neural Networks via Coherent Functors
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.