4 ms·

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 & verifiab

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'''
- lmeyerov 2y 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.
YeGoblynQueenne 2y 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.
- lmeyerov 2y 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.
  - YeGoblynQueenne 2y ago
    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.
    - lmeyerov 2y ago
      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.
sublinear 2y 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!
- lmeyerov 2y 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
YeGoblynQueenne 2y 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).

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

lmeyerov 2y 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.

YeGoblynQueenne 2y 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.

lmeyerov 2y 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.
- YeGoblynQueenne 2y ago
  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.
  - lmeyerov 2y ago
    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.

sublinear 2y 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!

lmeyerov 2y 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

YeGoblynQueenne 2y 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).