5 ms·

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. Q

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.

mountainriver 6y ago
I love this direction. I was studying homotopy a couple years back with this intention. Embedding functional relationships is the future
- deleted 6y ago
  [deleted]
ssivark 6y ago
Assuming this is neither sarcasm nor GPT3, WTF does it even mean?
- bopbeepboop 6y ago
  For the first: 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. https://www.microsoft.com/en-us/research/people/ksvore/ https://www.microsoft.com/en-us/research/people/ksvore/
tchalla 6y ago
What’s HoTT?
- AnimalMuppet 6y ago
  Homotopy type theory (https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory). Some people think it's the new mathematical theory of everything. I'm more skeptical.
  - bopbeepboop 6y ago
    My perspective is that it’s a useful idea for abstraction — which combined with category theory’s ability for composition is cool beans, at least in computer science. 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.

mountainriver 6y ago

I love this direction. I was studying homotopy a couple years back with this intention. Embedding functional relationships is the future

deleted 6y ago
[deleted]

ssivark 6y ago

Assuming this is neither sarcasm nor GPT3, WTF does it even mean?

bopbeepboop 6y ago
For the first: 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. https://www.microsoft.com/en-us/research/people/ksvore/ https://www.microsoft.com/en-us/research/people/ksvore/

tchalla 6y ago

What’s HoTT?

AnimalMuppet 6y ago
Homotopy type theory (https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory). Some people think it's the new mathematical theory of everything. I'm more skeptical.
- bopbeepboop 6y ago
  My perspective is that it’s a useful idea for abstraction — which combined with category theory’s ability for composition is cool beans, at least in computer science. 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.