one of my students who works on program synthesis is playing around with GPT-4 which is actually kind of a great use of AI -- we have an SMT solver to check everything it emits, we would never trust it for a millisecond otherwise and also, our current synthesis strategy (enumeration) is so painfully boneheaded that even random-ass LLM magic seems like an improvement