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!"
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.