As this LLM operates on LLVM intermediate representation language, the result can be fed into https://alive2.llvm.org/ce/ and formally verified. For those who don't know what to print there: here is an example of C++ spaceship operator: https://alive2.llvm.org/ce/z/YJPr84 (try to replace -1 with -2 there to break). This is kind of a Swiss knife for LLVM developers, they often start optimizations with this tool.
What they missed is to mention verification (they probably don't know about alive2) and comparison with other compilers. It is very likely that LLM Compiler "learned" from GCC and with huge computational effort simply generates what GCC can do out of the box.
I'm reasonably certain the authors are aware of alive2.
The problem with using alive2 to verify LLM based compilation is that alive2 isn't really designed for that. It's an amazing tool for catching correctness issues in LLVM, but it's expensive to run and will time out reasonably often, especially on cases involving floating point. It's explicitly designed to minimize the rate of false-positive correctness issues to serve the primary purpose of alerting compiler developers to correctness issues that need to be fixed.
This is one of the oldest computer operators in the game: the arithmetic IF statement from FORTRAN.
It's useful for stable-sorting collections with a single test. Also, overloading <=> for a type, gives all comparison operators "for free": ==, !=, <, <=, >=, >
How would that apply to Fortran’s arithmetic IF statement? It goes to one label for a negative value, or to a second label for a zero, or to a third label for positive. A NaN is in none of these categories.
I mean maybe I'm missing something but it seems like it behaves exactly the same way as subtraction? At least for integers it's definitely the same, for floats I imagine it might handle equals better?
C++ has operator overloading, so you can define the spaceship for any class, and get every comparison operator from the fallback definitions, which use `<=>` in some obvious ways.
The three-way comparison operator just needs to return a ternary, and many comparisons boil down to integer subtraction. strcmp is also defined this way.
In C++20 the compiler will automatically use the spaceship operator to implement other comparisons if it is available, so it's a significant convenience.
I'm not sure it's likely that the LLM here learned from gcc. The size optimization work here is focused on learning phase orderings for LLVM passes/the LLVM pipeline, which wouldn't be at all applicable to gcc.
Additionally, they train approximately half on assembly and half on LLVM-IR. They don't talk much about how they generate the dataset other than that they generated it from the CodeLlama dataset, but I would guess they compile as much code as they can into LLVM-IR and then just lower that into assembly, leaving gcc out of the loop completely for the vast majority of the compiler specific training.
Yep! No GCC on this one.
And yep, that's not far off how the pretraining data was gathered - but with random optimisations to give it a bit of variety.
We plan to have a peer reviewed version of the paper where we will probably have more details on that. Otherwise we can't give anymore details than in the paper or post, etc. without going through legal which takes ages.
Science is getting harder to do :-(
What they missed is to mention verification (they probably don't know about alive2) and comparison with other compilers. It is very likely that LLM Compiler "learned" from GCC and with huge computational effort simply generates what GCC can do out of the box.