There is interesting research in having LLMs cull the search space (for instance, asking the llm to provide which instructions are needed to complete the spec and provide an implementation) and then using more traditional techniques like ilp (or other symbolic means) to find the final program that corresponds to the spec. That way the result meets the spec but converges much (much!) faster than the traditional way for far complexer cases. Sometimes the llm gets it right in one shot (and the engine just verifies it is correct), sometimes it will never get it correct but ilp will finish the job just fine.