75 comments

  • epsylon 2 days ago ago

    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.

    • laginimaineb 2 days ago ago

      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.

      • calgoo 2 days ago ago

        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?

        • laginimaineb 2 days ago ago

          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.

          • calgoo 2 days ago ago

            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?

            Thanks!!!

        • fc417fc802 2 days ago ago

          > 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.

  • mccoyb 2 days ago ago

    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 ...

    • gavinray 2 days ago ago

        > Self-improving code would be code that runs itself and improves itself.
      
      I don't find the description any less accurate than saying that a JIT'ed application is self-improving code.
      • mccoyb 2 days ago ago

        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

    • luckystarr a day ago ago

      [dead]

  • krmmalik 2 days ago ago

    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.

    • f0e4c2f7 2 days ago ago

      For the first thing you're talking about check out bend.

      https://github.com/bendlang/bend

      • laginimaineb 2 days ago ago

        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.

      • krmmalik 2 days ago ago

        Thanks!

    • laginimaineb 2 days ago ago

      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.

  • gavinray 2 days ago ago

    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.

    • amelius 2 days ago ago

      > 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.

      • amelius a day ago ago

        This is just someone working on a niche problem and asking "how would invoking an oracle help here?" Happens everywhere. It is the modern equivalent of "X but now on a computer" or "X but now on the internet". You could even let an LLM make such combinations and filter out the interesting ones.

    • levineyoav 2 days ago ago

      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)

    • alirezaxdehghan a day ago ago

      isn't that just jit with extra steps?

      • netdevphoenix a day ago ago

        Is the JIT as good as an AI model for a specific Java program?

        • the_sleaze_ a day ago ago

          If you had an AI model for your specific java program why wouldn't you optimize it beforehand?

          • pfg_ a day ago ago

            Because you can't prove that the optimized version is the same as the original version

  • Revanche1367 2 days ago ago

    While the people behind this project seem to be real and apparently have credentials, this article is giving me serious whatever the textual version of uncanny valley is called. It hits so many of what reads like assorted buzzwords meant for marketing but guised in programmer-speak. One moment, they’re talking about the Curry-Howard correspondence and then next moment they’re describing what a data type is to people who are presumably more than casually familiar with LLMs. And the worst offense imo is linking to that “November Singularity” bs clearly written by AI to sell hype to people without much of a technical background (blog writer even admits some articles are written with AI “assistance”).

    • laginimaineb a day ago ago

      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.

      • Revanche1367 a day ago ago

        It says at the bottom of the main page some articles at least are written with AI assistance in the linked article for “November Singularity” and mentions the author cannot guarantee accuracy.

  • julesrms a day ago ago

    Sorry to be cynical, a lot of smart people seem to have built this.. but I'm failing to see how it's any better than "hey claude, here's my program and a profiling tool, go do your stuff"

    • laginimaineb a day ago ago

      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).

      • julesrms a day ago ago

        If you don't have part of the source code, then presumably that's because it was compiled, and there is almost no margin left for optimisation over what a modern compiler will already have done. I've written a JIT where we squeeze out a bit of gain over static compilation by vectorising to the available SIMD size, but it's marginal in most situations.

        You say "think libc" - are you suggesting they could dynamically recompile bits of libc and do better than LLVM's link time optimiser already did it??

        What I assumed was that you'd run this thing on some test runs, as a profiler step, and create an optimised binary. But you say they expect to run your code through an LLM all the time!?

        The idea that you could run your code through an LLM (which must surely slow it down 100x at least), and then find enough missed optimisation opportunities to make up for that slowdown is nuts! (Or I've just misunderstood the whole premise!)

        Honestly, the places in programs where you can get meaningful performance gain (that isn't already handled by your compiler) is all at the high-level big-O level, and that doesn't require runtime inspection.

        • mccoyb a day ago ago

          I think you're misunderstanding the premise.

          The binary is running. Maxwell is watching it: presumably there is some cost to the watching, but the LLM is not running in the binary process. Maxwell also has dynamic information about the running environment. Maxwell can then try and superoptimize the running binary using the dynamic information it has, but to do so, it needs to create semantics-preserving patches to the running binary.

          What should be clear here: dynamic information is strictly more information than what a static AOT compiler has access to.

          So that's the problem: we're going to patch the binary while it is running, and we need the patches to preserve the semantics as expressed by the high-level program, possibly assuming that the compiler was semantics preserving, etc. I'm assuming they have custom compilers or something for all of this.

          Getting this to work probably involves creating some sort of source map, perhaps a custom linker, etc (just guessing) from high-level program to binary -- but assuming you handle all of that, then the job of Maxwell is just the job of a normal superoptimizer: propose semantics-preserving patches, see how they do, etc.

          In theory, you could propose terrible patches frequently - superoptimization normally discards these, but you with bad proposals you might spend a long time searching for good patches. But LLMs are good proposers now, so you'd probably mostly get good patches (to a limit).

          Authors, correct me if I'm wrong.

          • julesrms a day ago ago

            I fully understand the merits of AOT vs JIT, I've worked on compiler tech, built JIT engines, and done lots of high performance realtime stuff for decades.

            But if:

            - we're talking about compiled code, where the compiler has already squeezed out all the low hanging fruit in terms of performance

            - it's running some kind of external process somehow watching the data flow around in memory, and is figuring out what code is doing what. This is at best incredibly expensive, even if happening in parallel

            ..then the chances of actually finding useful micro-optimisations that are also safe to patch while running without changing the memory layout and messing up.. is surely pretty close to zero.

            I can only assume that it's not actually native code, and they've built some kind of python JIT engine which is finding efficient replacements for chunks of common python, where it starts off so slow that even the massive amount of effort required manages to pay off in a long enough run.

            • mccoyb a day ago ago

              Right, makes sense — yes, all good questions that I’d also like to understand the answers to.

  • sfink a day ago ago

    Heh, such pushback here. The writeup seems to have gotten under people's skin.

    It's refreshing to read human prose about something like this. There's so much you can get about the author's state of mind -- pride at what they've accomplished and how they like to conceptualize it, traces of how they learned things and what those things mean to them... for me, it's a reminder of what we've lost in giving over so much of our writing to AI.

    But it's understandable that the writeup would trigger defensiveness. It claims a lot of originality and novelty that seem overreaching. AIUI, it's an optimizing JIT with a superoptimizer and a shared cache, with the search procedure guided by AI. And the equivalence model that the superoptimizer is based on includes all of Python and can handle both CPU and GPU code. It's quite impressive, really.

    It's hard to tell what of it is new. Superoptimizers are not, JITs are not, caching JIT code is not, using machine learning to speculate or search is not. Constraining an LLM to produce correct output is no newer than forcing semantically valid JSON output. (You could think them as different type systems.) Different JITs have handled different kinds and amounts of runtime information -- tracing JITs, runtime type inference like SpiderMonkey used to use, speculative compilation and invalidation (global or just in time like inline caches)....

    But none of that takes away from Maxwell. There isn't really enough information to compare it to other systems. Random example: many JITs work really hard to balance compilation time with execution time, and the post doesn't talk about that. Is it only for long-running code? Does it reach a steady state, and if so how much overhead is there at that time? What does it make slower or bigger?

    At any rate, it seems like there's a lot of interesting work in Maxwell, and it's worth checking out.

  • brainless a day ago ago

    Forgive the skepticism: Is this a harness that sits beside a language runtime, looks at traces/logs and uses an LLM to optimize code for given hardware?

    It looks interesting but I am really unable to see what is so different from a couple days of prompts and digging into a software to optimize it using LLMs.

  • enduku a day ago ago

    Cool. superoptimizing-jit ideas are exciting to me. Auto parallelism, swapping faster code/algos based on data distribution, autovectorization etc. Several years ago I had worked on an idiom based optimiser for assembly (https://github.com/xtellect/osm) and I hoped to extend it to binaries like what this team did. Couldn't find time to work on it further, but what this team achieved looks admirable. Congrats

  • claytonjy a day ago ago

    Suppose I have hundreds or thousands of containers from the same python image running in production, and want Maxwell to speed them up.

    How many Maxwells do I need? Maxwell isn’t free; when is it worth it vs when are the gains not enough to justify? How well can we estimate that up front?

    Does Maxwell only look at one container, or each of them individually? Do they all get the same patches or are they all treated independently?

    Does the profiling or patching cause temporary delays? If so how much, how might it compare to a GC pause or similar?

  • nickdothutton a day ago ago

    Sounds very interesting, I've occasionally wondered what it would be like to have a profiler "in the loop" which could direct improvements. Not everything can be known at compile-time, and even one run can differ greatly from another (ETL vs normal interactive use, or day-to-day load).

  • gus_massa a day ago ago

    I don't understand how it works. Is it a tracing JIT? https://en.wikipedia.org/wiki/Tracing_just-in-time_compilati...

  • Ohentis 2 days ago ago

    How is the compute of the model weighed against the compute that it saves?

  • fhn 2 days ago ago

    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.

    • laginimaineb 2 days ago ago

      That gets you nowhere near the same level of acceleration.

      • tomxor a day ago ago

        For claims of up to "2x" it certainly can do, but depending on the application and hardware, just like this.

        It's not clear to me from the article if the comparison is with locally compiled binaries, that would be the fair comparison.

        I would expect this to be better all rounder in theory, but it would be interesting to see what the difference is from a locally compiled baseline, and therefore if the complexity, obscurity and cost is worth it (again probably application and hardware dependant question).

  • levineyoav 2 days ago ago

    I like how the Manifesto is written, the Turing example at the top got me thinking more holistically about different impressive computer science achievements

  • falsemyrmidon a day ago ago

    Taking my deterministic code and injecting non determinism seems like a nightmare to work with

  • gordon28 2 days ago ago

    Can I use Maxwell in my js web app? Or just Python stuff?

  • 2 days ago ago
    [deleted]
  • Dan_Elkis 2 days ago ago

    I love it, any timeline for general availability?

  • 2 days ago ago
    [deleted]
  • nadavsch 2 days ago ago

    Sounds cool, but isn't it weird that optimizations from my workload are just for me? What if they could help a another user?

    • laginimaineb 2 days ago ago

      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).

      • addaon a day ago ago

        How do you anonymize and segment the cache to make this not leak PII? This seems prone to analysis showing that users who tend to take left branches in the user lookup trie (low alphabetic user names) also tend to render trees more than desert (so re-order the switch targets to optimize cache), suggesting that “Aaron” might live in Appalachia, not Arizona.

  • 2 days ago ago
    [deleted]
  • leopoldcongo 2 days ago ago

    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.

    • nadavsch 2 days ago ago

      this sort of response is so 1935

    • unrented7977 2 days ago ago

      Sick racism, bro

      • a day ago ago
        [deleted]
    • fhn 2 days ago ago

      [flagged]

    • Dan_Elkis 2 days ago ago

      antisemitism is not cool anymore

      • Moomoomoo309 a day ago ago

        What antisemitism? Antizionism is not antisemitism, period. Do not conflate the two.

        • nerfyink a day ago ago

          It’s not anti-Zionist to make accusations about someone just because they are Israeli. That’s just being a shitty person.

      • ImPostingOnHN a day ago ago

        israel != judaism

        as a jew, I'll thank you for not conflating the two again, because claiming all jews are a part of what israel is doing is tantamount to a jewish blood libel

        it is also ignorant, like picking a random african country and suggesting it represents all black people

        • nerfyink a day ago ago

          Bro, blood libels always targeted only some Jews, but they targeted them because they were Jews.

          This guy is responding to an innocent post about a product with accusations against it for being Israeli. Do you think it’s ok to make accusations against someone just because they are Israeli?

          It might not technically be classical antisemitism, or implemented the same way, but is still bigotry of the same root.

          Would you be ok with someone making accusations against anyone who is from an African country?

          • ImPostingOnHN a day ago ago

            > blood libels always targeted only some Jews, but they targeted them because they were Jews

            Yes, just like conflating me and my judaism with israel's actions is targeting me for being jewish and attacking me.

            > Would you be ok with someone making accusations against anyone who is from an African country?

            Would you be ok with someone making accusations against anyone who is jewish? Because that is what is happening here, just like making accusations against someone for being black.

            Maybe you're upset because someone else said something else, but that doesn't excuse the post I responded to, which attempted to conflate all jews with israel, and in so doing, ascribed horrific torture, killing, and crimes against humanity to all jews. That's literally a blood libel. "We" didn't do that. All jews/semites did not do that. israel did. Don't use us jews as human shields against criticism of israel, please.

            • nerfyink a day ago ago

              Try playing out this thread with any other group:

              OP: look at this cool product I made.

              leopoldcongo: This is an African product, you can’t trust them.

              Dan_Elkis: Racism is not cool anymore.

              You: African != black. As a black person, I'll thank you for not conflating the two again, because claiming all blacks are African is tantamount to racism.

              You see what’s happening here? You are ascribing horrific accusations against every Israeli for being Israeli.

              Saying it’s ok to do this for only one group in the world, that happens to be Jewish is antisemitism. You don’t have to include every Jew in your accusations to be an antisemite. The Nazis had Kapos too.

              • ImPostingOnHN 21 hours ago ago

                Again, maybe you're upset because someone else said something else, but that doesn't excuse the post I responded to, which attempted to conflate all jews with israel, and in so doing, ascribed horrific torture, killing, and crimes against humanity to all jews. That's literally a blood libel. "We" didn't do that. All jews/semites did not do that. israel did. Don't use us jews as human shields against criticism of israel, please.

                > African != black. As a black person, I'll thank you for not conflating the two again, because claiming all blacks are African is tantamount to racism.

                Yes, precisely. You are getting it. African != black, just like israeli != jewish. Claiming all blacks are African is indeed bigoted, just like claiming all jews are israeli (as happens when someone claims a criticism strictly of israel is "anti-semetic). Don't make either conflation, it is ignorant and disrespectful.

                • nerfyink 21 hours ago ago

                  > which attempted to conflate all jews with israel

                  That is not what it did.

                  If the Jews of Italy are accused of being baby-killers, and the Jews of France say we are not baby-killers, the accusation against the Italian Jews is still antisemitism, and it’s not antisemitic to call it antisemitism.

  • 2 days ago ago
    [deleted]
  • Skwid 2 days ago ago

    [flagged]

  • IAmRinSlow 2 days ago ago

    Is it 100% deterministic?

    • laginimaineb 2 days ago ago

      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.

      • ch_sm 2 days ago ago

        How does it prove the performance improvement? Does it A/B test in place on a production app?

  • MilkingCowboy49 a day ago ago

    [dead]

  • ben_mussay 2 days ago ago

    The manifesto is so cool!

  • 1Ecz3 2 days ago ago

    very cool