I am a huge fan of mm0, the thesis[0] is so brilliantly written, and MMC is such a great step towards the kind of verified computing I really want to be doing
Ahh I thought I was the only one! One line per sentence makes the diffs so much nicer too, maybe we need git hooks to reject multiple sentences per line?
I didn't find note-taking particularly useful until I started keeping everything in a single notebook with dated pages.
This worked a lot better than (for example) trying to organise notes by category - it's often easier to remember when you were working on something than how you categorised it, and once you know roughly when, you can find it by binary search
I saw a similar (I think!) paper "Grassmannian Optimization Drives Generalization in Overparameterized DNN" at OPT-ML at neurips last week[0]
This is a little outside my area, but I think the relevant part of that abstract is "Gradient-based optimization follows horizontal lifts across low-dimensional subspaces in the Grassmannian Gr(r, p), where r p is the rank of the Hessian at the optimum"
I think this question is super interesting though: why can massively overparametrised models can still generalise?
Which repos worked well? I've had the same experience as op- unhelpful diagrams and bad information hierarchy. But I'm curious to see examples of where it's produced good output!
Really nice! Had a quick read, here's my quick summary:
- Arrays are typed `S : D` with shape S and strides D
- Each of `S` and `D` is a nested tuple (instead of the flat tuples one typically sees in a tensor framework)
- Together `S` and `D` define the layout of a tensor
- Not every layout is "tractable", but the tractable ones form a nice category
A really good exposition, my only criticism is that it's quite front-heavy- it would be nice to see a detailed example like in 2.3.8 earlier in the document; there is a lot of detail presented early that doesn't seem necessary to understand the core ideas.
Last comment: I suspect there is a connection to strictification[0], would love to know more if the authors see this!
Hellas.AI is building a compiler for categorical deep learning to power decentralised, serverless AI.
We're looking for an experienced Rust engineer. You must have demonstrated:
* Experience in designing and implementing BFT consensus protocols
* Ability to engage with academic literature on distributed systems
* Understanding of ZK proofs and proof aggregation (you don't need to design these, but you should know how to use them)
Nice-to-have: interest or experience in:
* Deep Learning / ML / AI, GPU programming
* Compilers and array programming languages
* Category Theory and string diagrams
If you have project(s) demonstrating your experience in one or more of these areas, get in touch!
Our process is simple: we read code you've written and research you've published, then interview you about it. We don't do tedious coding tests.
I've been hoping for a nice concrete example of braided monoidal categories for ages, who knew that the best one was string diagrams that represent actual string! Great post!
@the author - I assume you're aware that morphisms in symmetric monoidal categories can be represented using cospans of hypergraphs - do you know if there's a similar combinatorial representation for braided monoidal categories?
(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.
Hellas.AI is building a compiler for categorical deep learning to power decentralised, serverless AI.
If you're interested in any of the following, get in touch:
* Category Theory and string diagrams
* Compilers and array programming languages
* Deep Learning/ML/AI and/or GPU programming (e.g. CUDA/
WGSL)
* Building and deploying distributed systems
* Peer-to-peer software and blockchain
If you have project(s) demonstrating your experience in one or more of these areas, get in touch!
Our process is simple: we read code you've written and research you've published, then interview you about it.
We don't do tedious coding tests.
Some experience of Rust or a functional language (Haskell, OCaml, any Lisp) is preferred.
Seems bad. "An attacker was able to achieve code execution in the content process by exploiting a use-after-free in Animation timelines. We have had reports of this vulnerability being exploited in the wild."
I only had a quick look, but it looks like they tweaked the state update so the model can be run with parallel scan instead of having to do it sequentially.
At least for chinese there are off-the-shelf word segmenters you can use like jieba[0]- I used it in gptlingo and it Just Works(TM).
The "show pronounciations" setting just turns on pinyin above characters - what I want is to type pinyin and enter chinese characters. Actually showing the pinyin above characters is quite distracting!
> Duolingo is good at going from nothing to something
Seconding this. I got noticeably better at Chinese after using duolingo every day. I feel like I hit a ceiling now and it's not helping too much, but it definitely worked.
I used postgrest (without htmx) on an old project; it's impressive how far you can push it.
HTMX seems like a perfect fit for it too, although I'm not sure how much I really want to maintain htmx templates inside SQL functions...
[0]: https://digama0.github.io/mm0/thesis.pdf