4 ms·

Catgrad: A categorical deep learning compiler

77 points by remexre 2y ago

deleted 2y ago
[deleted]
abeppu 2y ago
So, learning about the categorical structure is interesting, but is there a specific advantage to seeing these concepts directly informing the implementation vs as a post-hoc way of explaining what autodiff is doing? E.g. Tensorflow is creating and transforming graphs of computation. Despite being written before most of the categorical work cited was done, isn't it doing the "same" thing, but we just wouldn't find names or comments in the code that closely align with the categorical work?
- deleted 2y ago
  [deleted]
tripplyons 2y ago
How does this compare to the XLA's ability to compile full training steps from JAX?
bguberfain 2y ago
It remembers me Theano [0]. [0] https://en.wikipedia.org/wiki/Theano_(software) https://en.wikipedia.org/wiki/Theano_(software)
catgary 2y ago
This is a nice project, but “You only linearize once” is more-or-less the type theory version of “Reverse Derivative Categories”, so JAX really does this already.
- statusfailed 2y ago
  (author here) the goals of catgrad are a bit different to JAX - first of all, the "autodiff" algorithm is really a general approach to composing optics, of which autodiff is just a special case. Among other things, this means you can "plug your own language" into the syntax library to get a "free" autodiff algorithm. Second, catgrad itself is more like an IR right now - we're using it at hellas.ai to serve as a serverless runtime for models. More philosophically, the motto is "write programs as morphisms directly". Rather than writing a term in some type theory which you then (maybe) give a categorical semantics, why not just work directly in a category? Long term, the goal is to have a compiler which is a stack of categories with functors as compiler passes. The idea being that in contrast to typical compilers where you are "stuck" at a given abstraction level, this would allow you to view your code at various levels of abstractions. So for example, you could write a program, then write an x86-specific optimization for one function which you can then prove correct with respect to the more abstract program specification.
  - nh23423fefe 2y ago
    can you expand on "write programs as morphisms directly" I'm someone super interested in category theory and ITT, but I can't quite parse what you are trying to convey even though I think I have the prereqs to understand the answer.
  - efferifick 2y ago
    > Among other things, this means you can "plug your own language" into the syntax library to get a "free" autodiff algorithm. Hello, as a compiler engineer I am interested in this area. Can you expand a little bit more? How would I be able to plug in my own language for example? > So for example, you could write a program, then write an x86-specific optimization for one function which you can then prove correct with respect to the more abstract program specification. So, what you are saying is that catgrad alllows me to write a program and then also plug in a compiler pass? I.e., the application author can also be the compiler developer?
  - catgary 2y ago
    I get it, but once you’ve compiled your program down to a computational graph…well those are basically morphisms in a monoidal/multi category, no? And then you can have a stack of MLIR dialects that represent different levels of abstraction, where optimization passes are functors between the multicategory determined by that dialect, then you hand it off to LLVM for CPU execution, or maybe you want to run it with WebGPU, go down to CUDA, etc.
cyanydeez 2y ago
i always find it fascinating when projects like these can seem to find a proper overview for the AI curious non-PhD students.
drumnerd 2y ago
I think about cones all the time when doing machine learning. If I have an object O that can be mapped to A and B I can learn a function from A to B or B to A if I can generate Os. That’s my view of self supervised learning.
incrudible 2y ago
Category theory always reminds me of this quip by Feynman: https://www.youtube.com/watch?v=B-eh2SD54fM https://www.youtube.com/watch?v=B-eh2SD54fM When I hear people talking in the jargon of category theory, I do not understand what they say, but I have a suspicion that it is something rather mundane that I would understand if they were using the more specific terms for the given context. I understand the appeal of generalization from a mathematical perspective, but from a practical programming perspective, I fail to understand the value proposition.
- feanaro 2y ago
  How do you discover the principles in the first place? You can discover them once and then apply them in all applicable places precisely because you generalised them. You have a point that the result may very well be more easily explained in concrete terms to practitioners of a given field in which you applied it, though.
- steego 2y ago
  While I understand Feynman’s point that mathematicians love to generalize everything and that physicists focus on what actually works in the real world, as programmers, we’re doing something different from both of those groups. We’re engaged in a mix of engineering and analysis. We need to build systems that hold together under real conditions. Category theory might seem obsessed with abstraction. In some ways, it is. However, when skilled practitioners apply these tools to areas of computer science and engineering, the point isn’t to create generalized abstractions. The point is identify the minimal, leak-proof abstractions needed to fulfill some desired quality. While I understand the language sounds very general, cryptic and off-putting, it’s also very precise. While category theory might seem like a discipline that’s obsessed with generalizations, in practice, the abstractions one constructs using categorical tools can be very specific. The point isn’t always to construct the most general abstractions, it’s to construct abstraction that actually work 100% of the time. The irony is, mathematicians and computer scientists who are concerned with rigor often do this by proving specific cases first and then incrementally generalizing, not the other way around.
- catgary 2y ago

77 points by remexre 2y ago

deleted 2y ago

[deleted]

So, learning about the categorical structure is interesting, but is there a specific advantage to seeing these concepts directly informing the implementation vs as a post-hoc way of explaining what autodiff is doing? E.g. Tensorflow is creating and transforming graphs of computation. Despite being written before most of the categorical work cited was done, isn't it doing the "same" thing, but we just wouldn't find names or comments in the code that closely align with the categorical work?

deleted 2y ago
[deleted]

tripplyons 2y ago

How does this compare to the XLA's ability to compile full training steps from JAX?

bguberfain 2y ago

It remembers me Theano [0]. [0] https://en.wikipedia.org/wiki/Theano_(software) https://en.wikipedia.org/wiki/Theano_(software)

catgary 2y ago

This is a nice project, but “You only linearize once” is more-or-less the type theory version of “Reverse Derivative Categories”, so JAX really does this already.

statusfailed 2y ago
(author here) the goals of catgrad are a bit different to JAX - first of all, the "autodiff" algorithm is really a general approach to composing optics, of which autodiff is just a special case. Among other things, this means you can "plug your own language" into the syntax library to get a "free" autodiff algorithm. Second, catgrad itself is more like an IR right now - we're using it at hellas.ai to serve as a serverless runtime for models. More philosophically, the motto is "write programs as morphisms directly". Rather than writing a term in some type theory which you then (maybe) give a categorical semantics, why not just work directly in a category? Long term, the goal is to have a compiler which is a stack of categories with functors as compiler passes. The idea being that in contrast to typical compilers where you are "stuck" at a given abstraction level, this would allow you to view your code at various levels of abstractions. So for example, you could write a program, then write an x86-specific optimization for one function which you can then prove correct with respect to the more abstract program specification.
- nh23423fefe 2y ago
  can you expand on "write programs as morphisms directly" I'm someone super interested in category theory and ITT, but I can't quite parse what you are trying to convey even though I think I have the prereqs to understand the answer.
- efferifick 2y ago
  > Among other things, this means you can "plug your own language" into the syntax library to get a "free" autodiff algorithm. Hello, as a compiler engineer I am interested in this area. Can you expand a little bit more? How would I be able to plug in my own language for example? > So for example, you could write a program, then write an x86-specific optimization for one function which you can then prove correct with respect to the more abstract program specification. So, what you are saying is that catgrad alllows me to write a program and then also plug in a compiler pass? I.e., the application author can also be the compiler developer?
- catgary 2y ago
  I get it, but once you’ve compiled your program down to a computational graph…well those are basically morphisms in a monoidal/multi category, no? And then you can have a stack of MLIR dialects that represent different levels of abstraction, where optimization passes are functors between the multicategory determined by that dialect, then you hand it off to LLVM for CPU execution, or maybe you want to run it with WebGPU, go down to CUDA, etc.

cyanydeez 2y ago

i always find it fascinating when projects like these can seem to find a proper overview for the AI curious non-PhD students.

drumnerd 2y ago

I think about cones all the time when doing machine learning. If I have an object O that can be mapped to A and B I can learn a function from A to B or B to A if I can generate Os. That’s my view of self supervised learning.

incrudible 2y ago

Category theory always reminds me of this quip by Feynman: https://www.youtube.com/watch?v=B-eh2SD54fM https://www.youtube.com/watch?v=B-eh2SD54fM When I hear people talking in the jargon of category theory, I do not understand what they say, but I have a suspicion that it is something rather mundane that I would understand if they were using the more specific terms for the given context. I understand the appeal of generalization from a mathematical perspective, but from a practical programming perspective, I fail to understand the value proposition.

feanaro 2y ago
How do you discover the principles in the first place? You can discover them once and then apply them in all applicable places precisely because you generalised them. You have a point that the result may very well be more easily explained in concrete terms to practitioners of a given field in which you applied it, though.
steego 2y ago
While I understand Feynman’s point that mathematicians love to generalize everything and that physicists focus on what actually works in the real world, as programmers, we’re doing something different from both of those groups. We’re engaged in a mix of engineering and analysis. We need to build systems that hold together under real conditions. Category theory might seem obsessed with abstraction. In some ways, it is. However, when skilled practitioners apply these tools to areas of computer science and engineering, the point isn’t to create generalized abstractions. The point is identify the minimal, leak-proof abstractions needed to fulfill some desired quality. While I understand the language sounds very general, cryptic and off-putting, it’s also very precise. While category theory might seem like a discipline that’s obsessed with generalizations, in practice, the abstractions one constructs using categorical tools can be very specific. The point isn’t always to construct the most general abstractions, it’s to construct abstraction that actually work 100% of the time. The irony is, mathematicians and computer scientists who are concerned with rigor often do this by proving specific cases first and then incrementally generalizing, not the other way around.
catgary 2y ago