There's a lot of claim and so little technical details on that page.
How was the formalization of Python accomplished? What formal proof framework do you use?
How do you reproduce the optimizations across several instances / runs of the program? (since the source code doesn't change... assuming you don't redo the same work over and over?)
What visibility, tracking and logging is there into the actual code running? Debugging is an extremely important part of building software, especially if there's a demon switching out binary code constantly underneath. Even if the recompiler is perfect (it won't be), user code never is.
Why is the superoptimization and visibility into the data not surfaced back to the level of the source code? This seems like a waste.
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.
So the output binary is basically a black box at this point? There is no way for people to verify what your model has generated is actually what we want the code to do?That also means that every time we want to make a change to our application we are forced to re-run it from your caching system, completely locking us to you for all software output?
First, thanks for the quick reply! Basically, it leaves each run of the application linked to your cloud services, so does that mean that offline and isolated runs cant use it.
Second, are you just sending profiles of what is running or is data that is being processed shared?
> So the output binary is basically a black box at this point?
To the extent that a formal proof is a black box ... ?
Which leads to an intriguing thought. If our languages and other infrastructure supported formal proofs that compiler output matched input it would obviate the motivation for reproducible builds.
- superoptimization specialized to a particular piece of hardware
- patching binaries while they are running
all great
That being said, I'm getting some weird vibes from the prose on this site. Little phrases and claims that seem intended for the purposes of marketing, but conflate things with clear technical meaning in confusing ways.
For instance: I watched the video ("a code execution model has to be right every time") which implicitly communicates something like "the model cannot hallucinate" ... of course, the agentic LM is still probabilistic, but it is wrapped with verification tools (to reason about semantic equivalence), and is likely post-trained to be good at using those tools.
This strikes me as a conflation between the model and the harness which is intended to strike a marketing point (like: "it doesn't hallucinate") but which is clearly a ridiculous claim to make (falling down the slope: any harness which does error correction for improper tool calls might also be a "model which makes no mistakes")
Also: "self-improving code"
that's not really it, is it? Self-improving code would be code that runs itself and improves itself. This is code I run, which Maxwell watches and improves ... no?
Related: I dislike the usage of the word "model" in the above discussions on the site. Do we want to call everything a "model" now? Can anyone invent a new frontier "model" by post training an agentic LM with tools?
Also, let's say you are optimizing kernels on GPUs. This can be subtly fraught: for instance, it was well-known for awhile that one should only use certain pieces of software (vLLM, for instance) to reproduce papers (which used vLLM) there are non-deterministic sources of randomness (including, of course, floating point) that would prevent one from recovering the performance claimed in a paper ...
I agree with you that Maxwell is like a JIT (with superoptimization inside of it: a very smart one which can propose smart things using the underlying agentic model, and reason about semantic equivalences to figure out what to commit or not) and that that is a natural analogy.
But people who write JITs don't call the overall process (original code, JIT) "self-improving code", do they?
What is the "self" in (original code, JIT)? Is it the entire process? But the JIT doesn't make itself better as it runs? Is all code that runs in a managed runtime with dynamic analysis self-improving?
A much better term might be "dynamically-improving code"
But related and to the point of my original message: the phrase "self-improving" has been used in vogue by AI research / labs ... and this is another example of something which is not a clear term, and seems intended for marketing
I read the entire manifesto thinking the discourse about a code execution model would lead to a revelation that this is a model that can reduce bugs in code in realtime and make sure the code runs to the original spec or blueprint. Instead it turned out to be about a model that keeps on optimising code that can go faster and faster over time. That's very exciting in its own right, don't get me wrong, but I was really starting to hope this would be about creating code that breaks less etc.
Maybe it means both but perhaps the emphasis is on speed.
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.
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 homepage does not do a very good job of explaining what we're looking at:
It appears to be a combination of two things:
1) A formalization of the Python language
2) An LLM which hooks into running programs and hot-swaps code with verifiably-equivalent behavior but better runtime performance, found via superoptimization and then verified via the formalization rules
This is brilliant, and in hindsight one of those "I can't believe nobody had thought of this yet" sort of things.
> This is brilliant, and in hindsight one of those "I can't believe nobody had thought of this yet" sort of things.
Please speak for yourself. We've seen many such ideas here even putting an LLM into a CPU to do branch predictions. Using it to write a (jit) compiler with correctness preserving transformations is not something that didn't occur to most compiler folks.
The intersection of the above two points requires non trivial expertise (and note that point 2 requires different low level expertise for the “swapping” part and the “optimization” part)
Just compile for your specific hardware sort of like what Gentoo does. I don't want you continuously running a model - sort of defeats the purpose of performance gains.
I like how the Manifesto is written, the Turing example at the top got me thinking more holistically about different impressive computer science achievements
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).
this is an israeli company, use at your own risk (to life, the planet and humanity). plus you dont want an israeli company in your stack swapping code with malware and trojans.
How was the formalization of Python accomplished? What formal proof framework do you use?
How do you reproduce the optimizations across several instances / runs of the program? (since the source code doesn't change... assuming you don't redo the same work over and over?)
What visibility, tracking and logging is there into the actual code running? Debugging is an extremely important part of building software, especially if there's a demon switching out binary code constantly underneath. Even if the recompiler is perfect (it won't be), user code never is.
Why is the superoptimization and visibility into the data not surfaced back to the level of the source code? This seems like a waste.
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.
Thanks!!!
To the extent that a formal proof is a black box ... ?
Which leads to an intriguing thought. If our languages and other infrastructure supported formal proofs that compiler output matched input it would obviate the motivation for reproducible builds.
- verification
- superoptimization specialized to a particular piece of hardware
- patching binaries while they are running
all great
That being said, I'm getting some weird vibes from the prose on this site. Little phrases and claims that seem intended for the purposes of marketing, but conflate things with clear technical meaning in confusing ways.
For instance: I watched the video ("a code execution model has to be right every time") which implicitly communicates something like "the model cannot hallucinate" ... of course, the agentic LM is still probabilistic, but it is wrapped with verification tools (to reason about semantic equivalence), and is likely post-trained to be good at using those tools.
This strikes me as a conflation between the model and the harness which is intended to strike a marketing point (like: "it doesn't hallucinate") but which is clearly a ridiculous claim to make (falling down the slope: any harness which does error correction for improper tool calls might also be a "model which makes no mistakes")
Also: "self-improving code"
that's not really it, is it? Self-improving code would be code that runs itself and improves itself. This is code I run, which Maxwell watches and improves ... no?
Related: I dislike the usage of the word "model" in the above discussions on the site. Do we want to call everything a "model" now? Can anyone invent a new frontier "model" by post training an agentic LM with tools?
Also, let's say you are optimizing kernels on GPUs. This can be subtly fraught: for instance, it was well-known for awhile that one should only use certain pieces of software (vLLM, for instance) to reproduce papers (which used vLLM) there are non-deterministic sources of randomness (including, of course, floating point) that would prevent one from recovering the performance claimed in a paper ...
But people who write JITs don't call the overall process (original code, JIT) "self-improving code", do they?
What is the "self" in (original code, JIT)? Is it the entire process? But the JIT doesn't make itself better as it runs? Is all code that runs in a managed runtime with dynamic analysis self-improving?
A much better term might be "dynamically-improving code"
But related and to the point of my original message: the phrase "self-improving" has been used in vogue by AI research / labs ... and this is another example of something which is not a clear term, and seems intended for marketing
Maybe it means both but perhaps the emphasis is on speed.
https://github.com/bendlang/bend
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.
The homepage does not do a very good job of explaining what we're looking at:
It appears to be a combination of two things:
1) A formalization of the Python language
2) An LLM which hooks into running programs and hot-swaps code with verifiably-equivalent behavior but better runtime performance, found via superoptimization and then verified via the formalization rules
This is brilliant, and in hindsight one of those "I can't believe nobody had thought of this yet" sort of things.
Please speak for yourself. We've seen many such ideas here even putting an LLM into a CPU to do branch predictions. Using it to write a (jit) compiler with correctness preserving transformations is not something that didn't occur to most compiler folks.
Nobody is afraid of Israel anymore go scare some Americans instead
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.