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.
- 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 ...
This was a lot more exciting than I expected.
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.
Let me say that I like the idea:
- 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 ...
How is the compute of the model weighed against the compute that it saves?
The manifesto is so cool!
Is it 100% deterministic?
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.