4 ms·
Next step is to add verification for optimized code from the LLM with an SMT solver (like Z3) to remove "hallucinations". If the input and output code can be ve
by haltist 3y ago
Next step is to add verification for optimized code from the LLM with an SMT solver (like Z3) to remove "hallucinations". If the input and output code can be verified to be equivalent then this would be a great addition to an optimization pipeline. Once that's done the same can be applied to intermediate representations of GPU kernels in a recursive loop of AI optimizing AI code for faster execution times.
- deleted 3y ago[deleted]
- deleted 3y ago[deleted]
- boomanaiden154 3y agoThere'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 https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf
- haltist 3y agoInteresting. AI code has no loops so the problem they mention in the beginning about unrolling loops to a certain depth is a non-issue.