[boomanaiden154]

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.

[hughleat]

Yep, we tried it :-) These were exactly the problems we had with it.