laginimaineb

To name a couple.

(a) Scope: Maxwell can optimise portions of both your own code, but also of underlying libraries too (think libc), according to your data flow and env. These aren't places where you necessarily have source code or an easy way to replace it.

(b) It's dynamic: like a JIT, if your data flow _changes_, Maxwell detects new bottlenecks and reoptimises. A good example is an inference pipeline where e.g. the concurrency or seqlens can change suddenly (depending on what your users do). If you reoptimise for each such case, you'll do so forever (and there are many different operational points, each requiring their own algorithmic approach).

Uhm I wrote the blog, and I'm quite proud to say it is human written... And nowhere did I say anything about AI assistance. Happy to address any questions about substance if you like.

I don't follow.

If you don't use Maxwell everything works as is.

Maxwell does swaps in memory during runtime, not on disk.

And we of course sign every output and do externalise the proof of equivalence.

Actually Maxwell can reuse optimisations across users by clever caching. (A cool side effect is that the more it is used, the faster it becomes for everyone).

Bend is a formal language, but its use is quite different (also, Bend is much too narrow for Maxwell's use case...).

We need proofs of equivalence (including for code with side effects!) between original code, and new code, possibly in some other language. Say Python and a raw SIMD implementation. To do this we have a full 'embedding' of said languages in the same formal framework. It also requires modeling exactly what 'state' means in dynamic high level languages.

That gets you nowhere near the same level of acceleration.

More technical details forthcoming of course, including about formalisation... We indeed do not redo the same work over and over, but rather cache intelligently. We take special care not to interfere with debugging workflows (much in the same way that, e.g., the Tier 2 JIT does, in CPython). And as for visibility into the level of source code, what do you mean? The rewritten binary portions don't always have associated code, let alone in the language of origin.

Yes, CEMs can also help reduce bugs. To give an example, we found several memory safety bugs in core CPython code, through our formalisation. We'll release more details on that soon.

The verification is, which allows the optimisation to be extremely broad and non deterministic.

It's really unlike a compiler. For example, for a function like 'sort', the optimisation can:

- Use quicksort if the data distribution is generic.

- Use insertion sort if the data is nearly sorted

And so on... As long as these can be proven sound, Maxwell can pick the best optimisation in real time.

(I work at doubleAI.) The benchmark numbers (90% wins, 2.24x speedup on average, with key attention workloads accelerated ~15x) are one part of the story. The other: AI-generated kernels can pass simple verifiers with room to spare and still break in production. Our writeup walks through one such case: a fused embedding-gradient + RMSNorm backward kernel. As an example, we took the fastest (highest scoring) submission on the benchmark, for this task, submitted by other competitors, put it in our training code, and... everything broke (the loss diverged). The bug turned out to be subtle and hard to nail down (even changing the input distribution or the optimiser made it invisible). More details are in our blogpost.

We find these kinds of bugs very interesting: defending against humans is not the same problem as defending against agents. As models are becoming more powerful, they're also getting great at subverting verifiers (going through the 'path of least resistance'). This means that stronger verifiers are becoming increasingly more necessary, something we at doubleAI specialise in. You can also read our previous blogposts where we discuss this.

Happy to answer technical questions.

Actually, I would imagine they are nothing like one another.

However, Exynos uses a TrustZone TEE implementation to implement the KeyMaster module, just like Qualcomm's Snapdragon. This means that unless that TEE implementation uses a hardware key which is not software accessible, the same issue would be present. Of course, reverse-engineering a new TEE implementation would take a long time... But it sounds like it could be fun.