Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Program Synthesis and Large Language Models

cacm.acm.org

Post reply on HN
Print view View original

21–30 of 35 posts

Re: Program Synthesis and Large Language Models

#21

Post by lmeyerov »

YeGoblynQueenne wrote: post #18
lmeyerov wrote: post #9

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 untyp…

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.

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.

Re: Program Synthesis and Large Language Models

#22

Post by md_rumpf »

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.

Re: Program Synthesis and Large Language Models

#23

Post by lmeyerov »

jebarker wrote: post #10
lmeyerov wrote: post #9

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 untyp…

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

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

Re: Program Synthesis and Large Language Models

#25

Post by YeGoblynQueenne »

lmeyerov wrote: post #21
YeGoblynQueenne wrote: post #18

Earlier quoted context omitted.

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.

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.

There is nothing academic about this. Program synthesis is hard for a very practical reason, the same very practical reason that you can't just brute-force your way through to an encrypted message: computational complexity is a bitch.

I appreciate that we have bigger computers now and more data and we can train large language models but for somet things it doesn't matter how big your computer and how deep your model, there are things you just can't do. E.g. when was the last time you asked an LLM to decrypt an encrypted message for you and it did it correctly? I don't mean ROT 13 btw.

Re: Program Synthesis and Large Language Models

#26

Post by robertlagrant »

childintime wrote: post #24

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.

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.

Re: Program Synthesis and Large Language Models

#27

Post by robertlagrant »

simonw wrote: post #13
jebarker wrote: post #7

Earlier quoted context omitted.

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

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…

> If you're willing to put in that QA work yourself the productivity boost you can get them from is immense.

Isn't that work more than half the work of programming? I seem to find myself spending much more time on test code than on application code.

Re: Program Synthesis and Large Language Models

#28

Post by YeGoblynQueenne »

lmeyerov wrote: post #9

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 untyp…

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

Re: Program Synthesis and Large Language Models

#29

Post by YeGoblynQueenne »

simonw wrote: post #13
jebarker wrote: post #7

Earlier quoted context omitted.

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

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…

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

Then what do you need the chatbot for? I have to do that with my own code all the time anyway. What's the benefit?

Re: Program Synthesis and Large Language Models

#30

Post by lmeyerov »

YeGoblynQueenne wrote: post #25
lmeyerov wrote: post #21

Earlier quoted context omitted.

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.

There is nothing academic about this. Program synthesis is hard for a very practical reason, the same very practical reason that you can't just brute-force your way through to an encrypted message: computational complexity is a bitch. I appreciate that we have bigger computers now and more data and we can train large language models but for somet things it doesn't matter how big your computer and how deep your model,…

I don't feel like you're reading what I'm writing.

I regularly use LLMs to work with security protocols and encrypted data, which are wrapped in APIs, and write new GPU code. Likewise, I regularly use LLMs to more quickly write large test suites.

I do not use LLMs to augment my verification work, because our team do not verify things to gain belief of sufficient correctness. Likewise, I do not try to bruteforce decrypt things, though I am surprisingly more lax on how we do things because of the headroom from GPUs.

The problem is repeat use of weasel words like 'correctness' and even here, your 'some things', that are doing a lot of work. That some tasks are hard, especially with poor environmental assumptions, does not mean they matter to most people who need to write most programs. There is a hard question here of whether most people needing to make programs need to care about these.

Post reply on HN