4 ms·

Program Synthesis and Large Language Models

74 points by ChristofferSN 2y ago

jiangyaokai 2y ago
I have always believed difficulty is inherent to the problem. Regardless of whether that solver is a machine or a living organism. Maybe I am tainted in the same way since I studied complexity theory.
deleted 2y ago
[deleted]
bjornsing 2y ago
I’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.
- danenania 2y ago
  This kind of begs the question though in the “there’s nothing new under the sun” sense. Maybe your particular task is novel, but are its component parts and algorithms novel? In some cases, perhaps some of them are, but I think that’s more the exception than the rule. LLMs aren’t just tape recorders. They can mix and match and adapt. What percentage of the code you write do you think is truly original?
  - shadowerm 2y ago
    I just don't know if this is true. The music programming language Csound is a good test. There is not a huge amount of csound code online, but what is online is going to work. The models are just terrible with csound. They can not mix and match at all. They can't abstract at all. An even better test is to have the LLM try to make a piece of music in a certain style in csound. That is when you can see that the model is not abstracting the concepts at all. Zero. none. nada. Of course, it gives the probablistic next token prediction but because none of this is in the training data, the most probable output is basically noise/nonsense. In general, I think we highly underestimate how hard it is to come up with things that are not in the training data.
deleted 2y ago
[deleted]
golly_ned 2y ago
This 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.
- jebarker 2y ago
  > 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.
  - simonw 2y ago
    If you expect to be able to prompt a chatbot and then not TEST that the code it wrote for you works, you're going to have a bad time. If you're willing to put in that QA work yourself the productivity boost you can get them from is immense. And honestly, working with the best human programmer in the world won't guarantee that the software they produce is the exact software that you wanted. Details are always lost in the communication between the person who wants the software and the person who builds it What matters most is the dialog and speed of iteration that you can achieve to converge on the right product.
    - jebarker 2y ago
deleted 2y ago
[deleted]
mondrian 2y ago
Tl;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.
- deleted 2y ago
  [deleted]
lmeyerov 2y ago
It'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.
- jebarker 2y ago
  Do you have any links for Prof Song talking or writing about this? Sounds interesting
  - lmeyerov 2y ago
    Her keynote at last year's https://www.louie.ai/gen-ai-graph-the-planet/ https://www.louie.ai/gen-ai-graph-the-planet/ explicitly ended on this Basically the way forward she's most excited about wrt AI x Security as a way avoid devolving into AIs fighting AIs at runtime by instead moving to enfusing authoring time with formal methods. I think her references were to earlier verified C compiler extension frameworks such as by George Necula's various projects. Interestingly, hints of LLMs-for-automating-proofs are in her older papers, e.g., https://arxiv.org/pdf/1806.00608 https://arxiv.org/pdf/1806.00608 . Even Terance Tao is leaning in here now: https://www.youtube.com/watch?v=AayZuuDDKP0 https://www.youtube.com/watch?v=AayZuuDDKP0
- qsort 2y ago
  I don't think this is in direct contradiction with the article. This was written in response to ideas like: (a) the machine is so powerful that you can just tell it what to do and it does it with no supervision or (b) we can ditch programming languages and just use English as the "source of truth", like you would read, modify and check in the source code rather than compiled object code. (a) is very much yet to be seen, and (b) is just monumentally stupid. Productive uses of LLMs for code are either as a super-autocomplete or as a pair programmer, which doesn't make programming languages obsolete, much less computer science education as a whole. This is even called out in TFA: '''Even if chatbots should become a useful tool for programmers, their existence cannot mean the end of programming. It may well be the case that this combination of a built-in repository of code examples and the ability to easily retrieve code examples based on it can be used for generating ideas and for forms of “pair programming” as recently studied by Bird et al.2 But this is not program synthesis, rather it gives software using LLMs the role of more modest and possibly useful tools. We are now seeing a flurry of interest in combining traditional approaches to program analysis with LLMs, and if anything, this points to the limitations inherent in both approaches.3,8'''
md_rumpf 2y ago
Well... How do humans synthesizs programs then? We don't do exponential search over some symbols. We "somehow know" which branches get us closer to a program and which don't. It's foolish to believe it is impossible to teach an AI to "somehow know" this, too. Also: For some reason the bar is always higher for AI. Next to no human code is verifiably correct. And the actually verified-to-be-correct code is an even smaller subset.
childintime 2y ago
The argument goes like this: a car will never be able to do all the things a horse can do. Seems to me the car is the AI and the horse is the human.
- robertlagrant 2y ago
  Seems more like AI is like a Roomba and a person using a vacuum cleaner is like a human. Roomba can do the easy bits that are well-defined.

74 points by ChristofferSN 2y ago

I have always believed difficulty is inherent to the problem. Regardless of whether that solver is a machine or a living organism. Maybe I am tainted in the same way since I studied complexity theory.

deleted 2y ago

[deleted]

bjornsing 2y ago

I’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.

danenania 2y ago
This kind of begs the question though in the “there’s nothing new under the sun” sense. Maybe your particular task is novel, but are its component parts and algorithms novel? In some cases, perhaps some of them are, but I think that’s more the exception than the rule. LLMs aren’t just tape recorders. They can mix and match and adapt. What percentage of the code you write do you think is truly original?
- shadowerm 2y ago
  I just don't know if this is true. The music programming language Csound is a good test. There is not a huge amount of csound code online, but what is online is going to work. The models are just terrible with csound. They can not mix and match at all. They can't abstract at all. An even better test is to have the LLM try to make a piece of music in a certain style in csound. That is when you can see that the model is not abstracting the concepts at all. Zero. none. nada. Of course, it gives the probablistic next token prediction but because none of this is in the training data, the most probable output is basically noise/nonsense. In general, I think we highly underestimate how hard it is to come up with things that are not in the training data.

deleted 2y ago

[deleted]

golly_ned 2y ago

This 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.

jebarker 2y ago
> 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.
- simonw 2y ago
  If you expect to be able to prompt a chatbot and then not TEST that the code it wrote for you works, you're going to have a bad time. If you're willing to put in that QA work yourself the productivity boost you can get them from is immense. And honestly, working with the best human programmer in the world won't guarantee that the software they produce is the exact software that you wanted. Details are always lost in the communication between the person who wants the software and the person who builds it What matters most is the dialog and speed of iteration that you can achieve to converge on the right product.
  - jebarker 2y ago

deleted 2y ago

[deleted]

mondrian 2y ago

Tl;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.

deleted 2y ago
[deleted]

lmeyerov 2y ago

It'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.

jebarker 2y ago
Do you have any links for Prof Song talking or writing about this? Sounds interesting
- lmeyerov 2y ago
  Her keynote at last year's https://www.louie.ai/gen-ai-graph-the-planet/ https://www.louie.ai/gen-ai-graph-the-planet/ explicitly ended on this Basically the way forward she's most excited about wrt AI x Security as a way avoid devolving into AIs fighting AIs at runtime by instead moving to enfusing authoring time with formal methods. I think her references were to earlier verified C compiler extension frameworks such as by George Necula's various projects. Interestingly, hints of LLMs-for-automating-proofs are in her older papers, e.g., https://arxiv.org/pdf/1806.00608 https://arxiv.org/pdf/1806.00608 . Even Terance Tao is leaning in here now: https://www.youtube.com/watch?v=AayZuuDDKP0 https://www.youtube.com/watch?v=AayZuuDDKP0
qsort 2y ago
I don't think this is in direct contradiction with the article. This was written in response to ideas like: (a) the machine is so powerful that you can just tell it what to do and it does it with no supervision or (b) we can ditch programming languages and just use English as the "source of truth", like you would read, modify and check in the source code rather than compiled object code. (a) is very much yet to be seen, and (b) is just monumentally stupid. Productive uses of LLMs for code are either as a super-autocomplete or as a pair programmer, which doesn't make programming languages obsolete, much less computer science education as a whole. This is even called out in TFA: '''Even if chatbots should become a useful tool for programmers, their existence cannot mean the end of programming. It may well be the case that this combination of a built-in repository of code examples and the ability to easily retrieve code examples based on it can be used for generating ideas and for forms of “pair programming” as recently studied by Bird et al.2 But this is not program synthesis, rather it gives software using LLMs the role of more modest and possibly useful tools. We are now seeing a flurry of interest in combining traditional approaches to program analysis with LLMs, and if anything, this points to the limitations inherent in both approaches.3,8'''

md_rumpf 2y ago

Well... How do humans synthesizs programs then? We don't do exponential search over some symbols. We "somehow know" which branches get us closer to a program and which don't. It's foolish to believe it is impossible to teach an AI to "somehow know" this, too. Also: For some reason the bar is always higher for AI. Next to no human code is verifiably correct. And the actually verified-to-be-correct code is an even smaller subset.

childintime 2y ago

The argument goes like this: a car will never be able to do all the things a horse can do. Seems to me the car is the AI and the horse is the human.

robertlagrant 2y ago
Seems more like AI is like a Roomba and a person using a vacuum cleaner is like a human. Roomba can do the easy bits that are well-defined.