[boomanaiden154]

There's already tooling available for using SMT to validate LLVM-IR transformations [1]. It's designed for zero false positives however, so some things might slip through the cracks.

Additionally, this work focuses on phase ordering, which produces correct code regardless of what the LLM puts out, assuming there aren't any bugs in the passes being used (which could crop up as random orderings aren't as well tested as the standard orderings in the commonly used pipelines).

1. https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf

[haltist]

Interesting. AI code has no loops so the problem they mention in the beginning about unrolling loops to a certain depth is a non-issue.