Abstract We introduce a geometric model of shallow multiplicative exponential linear logic (MELL) using the Hilbert scheme. Building on previous work interpreting multiplicative linear logic (MLL) proofs as systems of linear equations, we show that shallow MELL proofs can be modelled by locally projective schemes. The key insight is that while MLL proofs correspond to equations between formulas, the exponential fragment of shallow proofs corresponds to equations between these equations. We prove that the model is invariant under cut-elimination by constructing explicit isomorphisms between the schemes associated with proofs related by cut-reduction steps. A key technical tool is the interpretation of the exponential modality using the Hilbert scheme, which parameterises closed subschemes of projective space. We demonstrate the model through detailed examples, including an analysis of Church numerals that reveals how the Hilbert scheme captures the geometric content of promoted formulas. This work establishes new connections between proof theory and algebraic geometry, suggesting broader relationships between computation and scheme theory.

Abstract The Curry–Howard correspondence is often described as relating proofs (in intuitionistic natural deduction) to programs (terms in simply-typed lambda calculus). However, this narrative is hardly a perfect fit, due to the computational content of cut-elimination and the logical origins of the lambda calculus. We revisit Howard’s work and interpret it as an isomorphism between a category of formulas and proofs in intuitionistic sequent calculus and a category of types and terms in simply-typed lambda calculus. In our telling of the story, the fundamental duality is not between proofs and programs but between emphlocal (sequent calculus) and global (lambda calculus or natural deduction) points of view on a common logico-computational mathematical structure.

The Local Learning Coefficient (LLC) is introduced as a novel complexity measure for deep neural networks (DNNs). Recognizing the limitations of traditional complexity measures, the LLC leverages Singular Learning Theory (SLT), which has long recognized the significance of singularities in the loss landscape geometry. This paper provides an extensive exploration of the LLC’s theoretical underpinnings, offering both a clear definition and intuitive insights into its application. Moreover, we propose a new scalable estimator for the LLC, which is then effectively applied across diverse architectures including deep linear networks up to 100M parameters, ResNet image models, and transformer language models. Empirical evidence suggests that the LLC provides valuable insights into how training heuristics might influence the effective complexity of DNNs. Ultimately, the LLC emerges as a crucial tool for reconciling the apparent contradiction between deep learning’s complexity and the principle of parsimony.

We introduce refined variants of the Local Learning Coefficient (LLC), a measure of model complexity grounded in singular learning theory, to study the development of internal structure in transformer language models during training. By applying these refined LLCs (rLLCs) to individual components of a two-layer attention-only transformer, we gain novel insights into the progressive differentiation and specialization of attention heads. Our methodology reveals how attention heads differentiate into distinct functional roles over the course of training, analyzes the types of data these heads specialize to process, and discovers a previously unidentified multigram circuit. These findings demonstrate that rLLCs provide a principled, quantitative toolkit for developmental interpretability, which aims to understand models through their evolution across the learning process. This work advances the field of developmental interpretability by providing a mathematically rigorous approach to understanding neural networks through the lens of their learning process. More broadly, this work takes a step towards establishing the correspondence between data distributional structure, geometric properties of the loss landscape, learning dynamics, and emergent computational structures in neural networks.

In singular models, the optimal set of parameters forms an analytic set with singularities, and a 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 is not appropriate. Despite its potential for addressing fundamental issues in deep learning, a singular learning theory appears to have made little inroads into the developing canon of a deep learning theory. Via a mix of theory and experiment, we present an invitation to the singular learning theory as a vehicle for understanding deep learning and suggest an important future work to make the singular learning theory directly applicable to how deep learning is performed in practice.

Abstract The Sweedler semantics of intuitionistic differential linear logic takes values in the category of vector spaces, using the cofree cocommutative coalgebra to interpret the exponential and primitive elements to interpret the differential structure. In this paper, we explicitly compute the denotations under this semantics of an interesting class of proofs in linear logic, introduced by Girard: the encodings of step functions of Turing machines. Along the way we prove some useful technical results about linear independence of denotations of Church numerals and binary integers.

Abstract We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply typed differential λ-calculus.