You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
David Corfield (Apr 01 2025 at 07:18):I've been interested for a while in the contrast between the vector-space approach to semantics, used by LLMs, and [[type-theoretic approaches]]. Where one may exploit the capacity of a high-dimensional vector space to contain very many near orthogonal vectors to keep different meaning concepts apart, the type-theoretic way looks to constrict via the typing discipline. Dependent type theories allow towers of types, each depending on the one (and hence ones) below.
I was interested to see in this paper the appearance of a hierarchical structure within a vector space associated to an LLM:
Now, could there be a way to mediate between the two approaches, such as a way to generate towers of dependent types from a collection of vectors in a vector space?
You might think that [[linear dependent type theory]] could play a role in mediating between the two extremes, allowing towers of different heights topped off by vector spaces (if linear types are restricted to depend only on nonlinear ones).
Now, is there anything useful to say mathematically about this situation? Seems like approaches to phylogenetic tree formation should be near.
It's surely easier to pass from a tower of sets to a corresponding vector space than to reconstruct a tower in reverse, or rather that there would be significant choices to be made to optimize in some sense this latter process.
Ring any bells?