Re:Large Language Models for Compiler Optimization
by SiempreViernes on Monday September 18, 2023 @06:50AM
(#37554539)
What do you do when you check the proof and discover it is false? Just ask again for a proof or discard the emitted instructions?
Re:Large Language Models for Compiler Optimization
by eru on Monday September 18, 2023 @08:44AM
(#37555380)
Depends on your use case, I guess?
Re:Large Language Models for Compiler Optimization
by hoosieree on Monday September 18, 2023 @09:45AM
(#37556041)
This is the right way to interact with LLMs in general. Ask for what you want, but independently verify the result. Don't be like that lawyer "...but I asked ChatGPT if it was telling the truth, and it said yes!"
Re:Large Language Models for Compiler Optimization
by eru on Tuesday September 19, 2023 @02:22AM
(#37566238)
What you describe is useful, but it's not really what my comment described.
My comment was describing the wacky idea of asking the model to come up with a formal, machine-checkable mathematical proof of correctness, too. That's hard in general.
The idea in the article of just letting the model pick between different, already proven-correct, optimization passes is much saner most of the time.
You could still do that, you'd just also need to ask the model for a proof. (But I guess that's much harder than heuristically picking which passes to apply.)