4 ms·
I meant how do you make sure the optimization suggested by the AI is actually valid. If you're using AI to modify bytecode for faster execution then you have to
by ainoobler 2y ago
I meant how do you make sure the optimization suggested by the AI is actually valid. If you're using AI to modify bytecode for faster execution then you have to make sure the optimized and unoptimized code are semantically equivalent. Neural networks can't do logic so how would you know the suggestions were not bogus?
- weebull 2y agoYou've asked the right question, and for those that think validation is as simpLe as "run it and see if it gets the right result", good start but instruction ordering can be critical around multi thread aware data structures. Taking a fence out, or an atomic operation might give a big performance gain. Trouble is the structure may now go wrong 1% of the time.
- aantix 2y agoA valid accompanying test would ensure this? You’d be extracting optimization candidates by running the test suite. You re-run the test suite after changes to ensure they still pass.
- ainoobler 2y agoJIT optimizers operate at runtime, there are no test suites to verify before/after. It's happening live as the code is running so if you use AI then you won't know if the optimization is actually valid or not. This is why the article is using Z3 instead of neural networks. Z3 can validate semantic equivalence, neural networks can't.
- fwip 2y agoYes, but this Z3 analysis is not done at runtime. It's done offline, based on JIT traces. A neural network could, in principal, suggest optimizations in the same way, which an expert would then review for possible inclusion into the Pypy JIT.
- ainoobler 2y agoYou'd still have to write a proof for verifying semantic equivalence before implementing the optimization so I don't see what the neural network gains you here unless it is actually supplying the proof of correctness along with the optimization.
- screcth 2y agoThe idea is that the LLM would provide "intuition" to guide the optimizer to find better optimizations, but a formal proof would be necessary to ensure that those optimizations are actually valid.
- fwip 2y agoI might be incorrect, but I don't believe that most compiler optimizations have formal proofs written out before implementation. Does Pypy do this?
- derdi 2y agoPypy doesn't do this in general. The same Z3 model that is used to find these missing optimizations is also used to verify some integer optimizations. But the point is that as long as optimization rules are hand-written, a human has thought about them and convinced themselves (maybe incorrectly) that the rules are correct. If a machine generates them without a human in the loop, some other sort of correctness argument is needed. Hence the reasonable suggestion that they should be formally verified.
- fwip 2y agoAh, yes, I meant that the LLM could output suggestions, which a human would then think about and convince themselves, and only then, implement in Pypy.
- derdi 2y agoPresumably the LLM would generate a lot of proposed rules for humans to wade through. Reviewing lots of proposed rewrites while catching all possible errors would be tedious and error-prone. We have computers to take care of this kind of work.
- lmeyerov 2y agoClose! Generate the z3 too - as the need is to verify, not test. It can be a direct translation. For all inputs, is the optimization output equivalent. (Bootstrapping a compiler prototype via LLMs is nice though.) One place LLMs get fun here is where the direct translation to z3 times out, such as bigger or more complicated programs, and so the LLM can provide intuition for pushing the solver ahead.
- SkiFire13 2y agoTests can't ensure the correctness of an algorithm, only that it gives the correct output on a specific input.
- aantix 2y agoDepends on the comprehensiveness of the test.
- SkiFire13 2y agoFor any practical input no test is gonna be comprehensive enough. Especially for something that has infinite possible inputs like programs.
- aantix 2y agoIs the scope a whole program or a specific algorithm?
- SkiFire13 2y agoEven most algorithms would allow too many inputs. Even a simple algorithm computing the addition between two 64 bit numbers allow 2^128 possible input combinations, which would take billions of years to exhaustively check in the best case.
- petschge 2y agoSure, for booleans you can just test all combinations of input arguments. In some cases you can do the same for all possible 32 bit float or int values that you have as input. But for 64 bit integers (let alone several of them) that's not feasible.
- stonemetal12 2y agoAs long as we can agree that we are testing the application logic and not the compiler or hardware, then if (a > 4) {...} else {...} can be tested with just 3, 4, 5 no need to test -430 or 5036. Known as boundary value testing, you partition all input into equivalence classes, then make sure your tests contain a sample from each class.
- gus_massa 2y agoI added a few somewhat similar optimization to Racket. The problem are the corner cases. For example (fixnums are small integer), is it valid to replace (if (fixnum? x) (fixnum? (abs x)) true) with just the constant true ? Try runing a few tests, common unit test and even random test. Did you spot the corner case? It fails only when x is the most negative fixnum, that is also a very rare case in a real program. (IIRC, the random test suit try to use more of this kind of problematic values.)
- wolf550e 2y agoregehr et al use alive2 which uses z3
- Twirrim 2y agoBut.. But.. But.... This is HN. You must use AI / LLMs for everything! /s