I want to see an LLM combined with correctness preserving transforms.

So for example, if you refactor a program, make the LLM do anything but keep the logic of the program intact.