In terms of foundational research:
There will be a bunch of work connecting type theory (algebra) to deep learning (geometry), by using the ideas from HoTT.
Quantum AI will become increasingly a thing.
There will be a bunch of work connecting type theory (algebra) to deep learning (geometry), by using the ideas from HoTT.
Quantum AI will become increasingly a thing.
Michael Shulman et al have been working on a semantic model of type theory as category diagrams and discuss how sometimes it’s easier to solve your problem as a diagram picture and sometimes as a logical statement.
The mathematics they used for this “foundations” work in abstract math connects hypergraphs/CW complexes decorated with data to statements in a type theory, like a program.
The goal is to use this deep mathematical connection to find a type theory “close to” our AI, allowing it to make “intuitive” extensions of a statement via DNN, but validate that it makes sense within its “effective language” deductively.
My research in that area is automating proofs as a “basic” usage of that idea: an AI turns the desired statement into a (partial) picture it tries to use image completion on, to make it look like other proofs it’s seen, but the discriminator for that generative step can use the formal model, after turning the proposed image into a statement — is it logically consistent or not?
There’s a bunch of problems in that area, which has only started to be explored the past few years with the DL is manifolds and covering ML papers.
tl;dr: That math work gives us rules for how to turn geometric objects defined one way (tensors on a space) into objects defined another (formulae on varieties). Algebraic geometry meets AI.
For the second:
The Microsoft QuArC group under Dr Krysta Svore is working on developing ways to accelerate common industry algorithms via quantum computers — just calling out AI as a particularly impactful application since quantum computers will come online in 10-20 years.
They have some AI papers if you poke around — mostly that “best fit” for data is a good analog for “lowest energy”, and ways to use that for gains.
Embedding functional relationships is the future
The square in a category diagram is a legit object — and we can have type theories with the same features.
That’s useful for computational equivalence (eg, spec matches implementation) and path bundling to prevent case explosion.
About what you’d expect from adding homotopies to type theory.