Program Synthesis and Large Language Models

https://cacm.acm.org/opinion/on-program-synthesis-and-large-language-models/

by ChristofferSN • 2 years ago

74 29 2 years ago

cacm.acm.org

bjornsing• 2 years 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• 2 years 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• 2 years 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.

golly_ned• 2 years 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.

jebarker3• 2 years 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• 2 years 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.

mondrian• 2 years 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.

lmeyerov7• 2 years 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.

jebarker3• 2 years ago

Do you have any links for Prof Song talking or writing about this? Sounds interesting

lmeyerov7• 2 years ago

Her keynote at last year's 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 . Even Terance Tao is leaning in here now: https://www.youtube.com/watch?v=AayZuuDDKP0

qsort• 2 years 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

(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'''

lmeyerov7• 2 years ago

I'm mostly responding to the middle third of the article that IMO interprets the word "correct" in an academic way that, IMO, is unanchored to how, to a rounding error, software is written:

"Even simple versions of the approach are intractable in the very precise sense of computational complexity theory if we are concerned about generating code that is correct." (Then 5 paragraphs about that being pspace-complete.)

The notion of correctness used in the article is a verified property. My point is probably less than 1% of the programmers on this site have ever verified their code in that sense, especially since they left a university setting. Instead, most commercial developers write tests based on their domain knowledge as developers and some limited understanding of their company's business domain... if at all. Which LLMs can also do.

YeGoblynQueenne6• 2 years ago

The article's claim is that:

"Generating Correct Program Code Is Hard"

Emphasis mine. The claim is widely accepted and I don't understand why that has changed just because LLMs can generate program code. Note the missing word.

lmeyerov7• 2 years ago

See my above on there is an academic use of terminology here that makes any discussion here irrelevant. A big chunk of the article reduces to pedantic trolling by basing arguments on this.

sublinear• 2 years ago

There's a very hard cliff of complexity that you and your business will fall off of with this attitude, but ya don't have to take my word for it!

lmeyerov7• 2 years ago

Not sure I understand

What % of programmers in your company writes verifying coq proofs or equiv for what goes to production? Vs what % just does testing (unit, integration, etc)?

For us, as a small team, we do 7-8 figure annually for tested but unverified GPU code, and our growth plan does not involve formal verification

YeGoblynQueenne6• 2 years ago

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

Yes, see, that's exactly the motivation for program synthesis (i.e. the automatic generation of programs that are correct with respect to some specification). Human programmers are perfectly capable of producing buggy code on our own. Nobody needs a system that can automatically generate bugs for the programmer to find and fix. We want something that can help us find bugs and fix them, or generate bug-free code automatically (if you can do one, you can do the other).

That is computationally hard and that hasn't changed, just as complexity theory hasn't suddenly been rendered obsolete, because of LLMs. Every attempt to get LLMs to produce correct code so-far use an LLM as a generator and then filters its output through a classical verifier, which is subject to all the issues with complexity that arise everywhere in program synthesis (for an early exemplar of that see DeepMind's AlphaCode).

md_rumpf• 2 years 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• 2 years 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.

robertlagrant2• 2 years 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.

jiangyaokai• 2 years 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.

Program Synthesis and Large Language Models

Related Stories