Presenting Neural Networks via Coherent Functors

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 $\hat{I}º$-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({\hat{I}}^1,Set)$ along a coherent functor ${\hat{I}}^1:RSpan(a_0,a_n)\to 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 $Co{h}_{\sim }$. Taken together, these results recast neural network inference as an extension problem in the 2-category $Co{h}_{\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.