Search

We associate to every proof structure in multiplicative linear logic an ideal which represents the logical content of the proof as polynomial equations. We show how cut-elimination in multiplicative proof nets corresponds to instances of the Buchberger algorithm for computing Gr\"obner bases in elimination theory.

In singular models, the optimal set of parameters forms an analytic set with singularities and classical statistical inference cannot be applied to such models. This is significant for deep learning as neural networks are singular and thus "dividing" by the determinant of the Hessian or employing the Laplace approximation are not appropriate. Despite its potential for addressing fundamental issues in deep learning, singular learning theory appears to have made little inroads into the developing canon of deep learning theory. Via a mix of theory and experiment, we present an invitation to singular learning theory as a vehicle for understanding deep learning and suggest important future work to make singular learning theory directly applicable to how deep learning is performed in practice.

We introduce the $2$-simplicial Transformer, an extension of the Transformer which includes a form of higher-dimensional attention generalising the dot-product attention, and uses this attention to update entity representations with tensor products of value vectors. We show that this architecture is a useful inductive bias for logical reasoning in the context of deep reinforcement learning.

We calculate denotations under the Sweedler semantics of the Ehrhard-Regnier derivatives of various encodings of Turing machines into linear logic. We show that these derivatives calculate the rate of change of probabilities naturally arising in the Sweedler semantics of linear logic proofs. The resulting theory is applied to the problem of synthesising Turing machines by gradient descent., 62 pages, moved the section on naive Bayesian observers earlier (Section 6.2) with slight changes to notation, references added in the introduction to Section 7 and related work in Remark 7.16

We give an introduction to logic tailored for algebraists, explaining how proofs in linear logic can be viewed as algorithms for constructing morphisms in symmetric closed monoidal categories with additional structure. This is made explicit by showing how to represent proofs in linear logic as linear maps between vector spaces. The interesting part of this vector space semantics is based on the cofree cocommutative coalgebra of Sweedler., v2: the article has been substantially rewritten to improve the exposition, some false statements about cut-elimination were corrected, a new section about second-order linear logic was added, and the material on geometry of interaction has been removed (to be published elsewhere), v3: fixed typos, added references