statusfailed
Joined 4 years ago
Karma
97
Submissions
33
Member since
Sep 18
https://statusfailed.com/about.html
View on Hacker NewsRecent submissions
Comment · 7 months ago
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
Comment · 7 months ago
The Milk-V Jupiter 2 (coming out in April) is RV23 too
Comment · 8 months ago
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?
Comment · 8 months ago
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
Comment · 10 months ago
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?
Comment · 11 months ago
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!
Comment · 1 year ago
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!
[0]: in the sense i mean here: https://arxiv.org/pdf/2201.11738v3
Comment · 1 year ago
Hellas.AI | Remote | Full Time or Contract | https://hellas.ai
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.
Email us at [email protected]
Comment · 1 year ago
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?
Comment · 1 year 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.
Comment · 1 year ago
Hellas.AI | Remote | Full Time or Contract | https://hellas.ai
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.
Email us at [email protected]