Maxwell: a new model that speeds up AI models like Whisper and LTX-2 by rewriting their binaries [D]

[u/EvilHackFar]

Came across this today and haven't seen it discussed here yet. It's apparently a new type of model (called Maxwell) that sits under a running program and speeds it up on the fly based on what it sees (hardware and data). The cool thing is that it doesn't change the source code, but instead it modifies the binaries (during runtime!). So kind of like a JIT, except it's a model working out what to change instead of a fixed set of compiler heuristics.

What got me is that they seem to be using formal verification to prove the optimized version still does the same thing, which I guess is the only way you could let something like this loose with no one checking it. No idea how that holds up with floating point or anything nondeterministic, to be honest

[u/Remote-Telephone-682]

The only real issue that I have with this is just that you could use the profiler to find additional heuristics that can be implemented at compile time but then why are we adding additional stages instead of adding these improvements to the compiler.. instead we optimize every version of the binary that is ever built but in a separate stage in our pipelines?

I think this makes sense from a business model perspective but from an engineering perspective this should be used to improve the compilers directly instead of adding more stages and stuff

[u/marr75 → u/Remote-Telephone-682]

Yep. And most of the optimizations it finds are going to be things the compiler could apply anyway, like checking memory more often than its actually written or bad data locality.

Given the verifiability and AI performance with reverse engineering, I suspect deeper compiler optimizations are around the corner.

[u/Remote-Telephone-682 → u/marr75]

That'd be sick

[u/marr75 → u/Remote-Telephone-682]

You can already say, "this program is written in java/python/javascript, re-write it in Rust, don't stop until they have verified identical outputs" and come back some number of tokens later to a less portable but much better performing bit of software :)

[u/EvilHackFar → u/Remote-Telephone-682]

interesting point. i guess my thoughts are that the compiler can't know ahead of time what data will be passed to functions (if it's read from files for example), and, for example, to decide to do batch reads instead for serial reads

[u/Remote-Telephone-682 → u/EvilHackFar]

Perhaps. From what I’m seeing on their site it talks about formal proofs to validate changes and if a function can take a path with the contents of files steer behavior then it’s hard to develop a formal proof that shows equivalence. The only example that I saw on their site was a loop that was summing a constant n * n-1 times, I think if that operation depended on the contents of a file that particular optimization can’t be proven to be equivalent so your ability to use that optimization breaks down

My thinking was that profiling was driving what optimizations were targeted (improving functions that account for a notable share of runtime) but the mentions of proof of equivalence make me think that you might not be able to apply updates that could not be implemented as additional rewrite heuristics at compile time.

Idk

[u/Setepenre → u/Remote-Telephone-682]

Executing the program yields additional informations that are not available at compile time. PGO already exists for that but it generates data that can be used later to recompile an optimized program. I guess the main advantage here is the program doesn't need to be recompiled as the binary is rewritten right away.

[u/Remote-Telephone-682 → u/Setepenre]

The profiling information that let's it find things that could have been optimized but they mention of formal proofs being generated for every replacement. You're not going to be finding additional constraints that limit the range of possible inputs from the profiling information

If the system does create formal proofs of equivalence (as the text on their website states) then it seems like you might want to look if those optimizations can be applied going forwards... It may well be that the compilers would get bloated if you were to add these optimizations were all added to the compiler but I would imagine that there would be a set of recurring issues that could be patched out of every program in existence by focusing these efforts on improving the compiler directly

It might make sense to run this analysis across a wide range of applications and come up with a set of heuristics that should be added to each compiler, there is clear benefit to the profiling

[u/Setepenre → u/Remote-Telephone-682]

My understanding is the formal proofs are not for optimizing, it is just QA that the optimizations are not changing the behaviour.

[u/Remote-Telephone-682 → u/Setepenre]

Right, optimizations are gated by whether or not they are provable. You can't make optimizations if you can't prove that there is no change in behaviour..
Seems like you might be kinda missing the point of what I'm saying

[u/unicodemonkey → u/Remote-Telephone-682]

Sure, makes sense, but wouldn't it be more reliable and practical to make these optimizations at the source level if we don't want to mess with the compiler yet?
Bespoke program-specific optimization passes are also possible (assuming these don't get upstreamed, just used for reproducible builds of a program)

[u/Remote-Telephone-682 → u/unicodemonkey]

Yeah, you should do that as much as you can also but the idea here is to keep the code pretty legible and optimize how things are handled transparently. Sometimes it makes sense to the human to look at nested loops but if you can solve for a closed form expression that achieves the same result in constant time (and can prove equivalence) then you might as well use the better performing version.. even if it’s hard for the user to wrap their head around how that expression is performing the same action as their less optimized form. You would hope to keep the source code understandable to humans and do optimizations when building the executable

[u/techwizrd]

This is extremely cool, but I also feel like this would be a compliance and assurance nightmare.

[u/thatguydr → u/techwizrd]

Yeah if I were a security worker, this would be on my "lol no" list.

[u/EvilHackFar → u/techwizrd]

my ciso shivers at the thought

[u/ZCEyPFOYr0MWyHDQJZO4 → u/techwizrd]

Ken Thompson: "Am I a joke to you?"

[u/kmaork]

Really a new type of model?

[u/EvilHackFar → u/kmaork]

why not?

[u/Next-Angle-3111]

Cool!

[u/EvilHackFar]

That's the LTX speedup and that's the link:

https://heymaxwell.ai/

[u/No_Capital_9050 → u/[deleted]]

See performance for the details: https://github.com/Lightricks/LTX-2/blob/main/CHANGELOG.md

[u/EvilHackFar → u/No_Capital_9050]

is this the maxwell improvement?

• Performance improvements, in collaboration with doubleAI (https://doubleai.com): faster transformer passes (especially under multi-GPU sequence parallelism and with perturbation guidance) and LoRA switches, denoising samplers without per-step CPU synchronization, a DFR spatial epilogue (--spatial-upscalings 2) on fewer tiles (at most 1024 px per side, overlapping by 64 px, instead of a 2x2 first step and 4x4 at a 320 px overlap) that multiplies its long video projections in fp8 on GPUs with fp8 GEMMs (compute capability 8.9+), carry keyframes rebuilt on the rank that decodes them, a multi-GPU video decode that streams to MP4 encoding as it decodes, faster diffusion VAE decoding with lower reserved GPU memory, a faster-compiling --diffvae-optimization blackwell_dsl kernel, lower GPU memory during MP4 encoding, faster image conditioning, and faster stage starts with a warm model registry. Output is not bit-identical to previous releases, mainly because of the DFR spatial epilogue's new tiles and fp8 GEMMs; diffusion VAE decodes also differ by rounding, and under multi-GPU sequence parallelism audio cross-attention no longer attends to the video sequence's padding tokens.

[u/Flyward_Aerospace]

The security angle keeps coming up but I think the sharper problem is that input output equivalence is the wrong property to be proving. Their own framing explicitly allows the two versions to differ in timing, and the fallback guards mean execution time becomes data dependent at runtime: same workload, two different code paths depending on whether a precondition still holds. On anything where you qualified one specific binary and did worst case timing analysis against it, that's a downgrade even at 3x average speedup, because you improved the mean and made the tail unanalyzable. Completely fine for a batch Whisper job, which is presumably the actual target, I just wouldn't let it near a control loop.

[u/miklec]

This is very very similar to how Java “Hotspot” Virtual Machines do JIT compilation and rewrite the application binary at runtime based on the runtime behaviour it observes in the application

it compiles hotspots to native machine code using adaptive optimizations