Program Synthesis and Large Language Models
cacm.acm.org
Program Synthesis and Large Language Models
1–10 of 35 posts
Re: Program Synthesis and Large Language Models
#2[deleted]
Re: Program Synthesis and Large Language Models
#3I’m beginning to see LLMs more as a solution to the code reuse problem: they can implement anything that’s common enough to appear a number of times in their training data.
If you’re hoping they will soon implement entirely novel complex systems based on a loose specification I think you’ll be disappointed.
Re: Program Synthesis and Large Language Models
#4[deleted]
Re: Program Synthesis and Large Language Models
#5This article compares the hardness of program synthesis to the utility of chatbots to show chatbots fall short.
The difference is we don’t expect chatbots to be 100% right but we do expect program synthesis to be 100% right. For chatbots, 99% is amazing in terms of utility. That other 1% is really hard to get.
Given the limitations of English being able to robustly specify a program, thus requiring constraints for program synthesis to be formal descriptions of specifications, the author is committing a category error in comparing two incommensurable solutions to two distinct problems.
Re: Program Synthesis and Large Language Models
#6[deleted]
Re: Program Synthesis and Large Language Models
#7This article compares the hardness of program synthesis to the utility of chatbots to show chatbots fall short. The difference is we don’t expect chatbots to be 100% right but we do expect program synthesis to be 100% right. For chatbots, 99% is amazing in terms of utility. That other 1% is really hard to get. Given the limitations of English being able to robustly specify a program, thus requiring constraints for pr…
> For chatbots, 99% is amazing in terms of utility.
Is it really though? If it's 99% of generated tokens, then 1 out of 100 being wrong is not great for code generation since you're often going to generate more than that. But let's suppose it's 1 in 100 whole functions or programs that's wrong. Unless there's a way to automatically verify when a function is wrong the error rate basically makes full automation, e.g. automatically fixing GitHub issues, out of the question.
So it seems like at 99% we're left with a system that requires constant vigilance from the user to check it's work. This is a far cry from the promise of true program synthesis.
What would be amazingly useful is a 99% reliable system that can tell you when it can't answer the question correctly instead of providing a wrong answer.
Re: Program Synthesis and Large Language Models
#8Tl;dr (a) program synthesis is provably hard and (b) English is too ambiguous as a specification language. Therefore we’re nowhere close.
Ultimately not a convincing argument. We could use this same argument to argue that a human cannot write a program to spec. That may be strictly true, but not interesting.
Re: Program Synthesis and Large Language Models
#9It's frustrating whenever folks throw up proof complexity as why LLMs can't work. If most programs most people want to write can map into predictable & verifiable abstractions, or we recognize almost no software is verified to beginwith, we realize the world is already moving on irrespective of personal hobby horses here. Shocker: Much of the world we interact with every day already runs on PHP, JavaScript, and untyped Python that is not verified, not type checked, and has repos overflowing with bugs and CVEs.
Prof. Dawn Song IMO has been articulating a more productive view. LLMs are generating half the new code on github anyways, so lean in: use this as an opportunity to make it easy for new code to use formal methods where before it would have been to hard. Progress will happen either way, and at least this way we have a shot at bringing the verifiability in to more user code.
Re: Program Synthesis and Large Language Models
#10It's frustrating whenever folks throw up proof complexity as why LLMs can't work. If most programs most people want to write can map into predictable & verifiable abstractions, or we recognize almost no software is verified to beginwith, we realize the world is already moving on irrespective of personal hobby horses here. Shocker: Much of the world we interact with every day already runs on PHP, JavaScript, and untyp…
Do you have any links for Prof Song talking or writing about this? Sounds interesting