Linear logic and deep learning [pdf]

>> So I’d like to begin by summarising some of the recent history in the field of artificial intelligence, or machine learning as its now called.

To be more precise, the field is still known as AI, but people outside the field only know (and care) about machine learning, presumably because that's what Googe, Facebook, et al are recruiting for.

This is a bit of a sad situation, really. AI, in its drive to solve major hard problems (that still remain unsolved btw), has always contributed powerful programming techniques and even entire language paradigms to computer science (functional programming, object orientation that basically started with Minsky's frames, all sorts of search algos etc).

Machine learning is just one such technique which has gained popularity outside AI. It's powerful, for restricted problems. But if it somehow replaces AI in peoples' mind, the goose that lays the golden eggs might just die.

At a super high level, the central problem is higher-order functions.

If you have a programming language, you can think of differentiation as being a higher-order function that takes a function a and returns a new function as a result. If your language has support for higher-order functions, then (a) you have to extend the definition of the derivative to cope with differentiation at higher type, and (b) ideally you'd like differentiation to be an operator in your programming language.

In general this is hard, so you have to cut the problem somewhere.

Pearlmutter and Siskind's basic idea is to use Reynolds defunctionalization transformation to turn higher-order programs into first-order programs, and then apply automatic differentiation to the resulting first-order program.

The approach in this talk is inspired by "differential lambda calculus", which is a setting where you retain full first-class functions, but restrict how you can use them by imposing certain typing constraints upon them (basically to ensure smoothness/differentiability of definable functions).

There is a mysterious connection between these ideas, since defunctionalization is closely related to the "geometry of interaction" semantics of linear logic, and differential lambda calculus is closely related to the vector space semantics of linear logic.

In addition to these semantic issues, there's also the question of how you hook it up to the actual algorithms people use to do gradient descent -- eg you need to use the Riesz representation theorem to justify representing the gradient as a matrix -- and that constrains how things could work even further. This is simultaneously annoying (because it makes things harder) and helpful (at higher type we have too much freedom in how to define the derivative, and so additional requirements help constrain the solution space).

So you might ask: why do we care so much about higher-order functions? The answer is that "higher-order function" is how semanticists pronounce "linking" and "separate compilation". It would be super great if we could take a bunch of teeny-tiny separately-developed models together, stick them together, and have everything work no problem.

Thanks for such a fantastic answer!

To a trained mathematician, deep learning is so so far away from the cutting edge. If there's anything that's going to make a massive, revolutionary not evolutionary, change in the deep learning landscape, it's not going to come from engineers walking around on the surface of what's already there, it'll come from pure mathematicians connecting it to the insights ripe for the picking found deep deep down in the theoretical dirt.

Fantastic stuff!

Does your work still keep the non-determinism of Ehrhard and Regnier?

This was the part that 'bothered' me, but it provided evidence of a link with process calculi.

I've also thought Ehrhard and Regnier's work was groundbreaking. It potentially opens up not just insights into differentiable programming, but a theory of concurrent computation and an algebraic theory of computation. My expectation is that it will reveal some deep links with other areas of mathematics, like group theory.