5 ms·

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

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.
  - deleted 2y ago
    [deleted]
  - YeGoblynQueenne 2y ago
    >> I don't feel like you're reading what I'm writing. I can assure you that I am. >> I do not use LLMs to augment my verification work, because our team do not verify things to gain belief of sufficient correctness. I don't understand where the "verification" part came into the discussion. Who said anything about using LLMs "to augment my verification work"? Are you perhaps confusing "program verification" with "program synthesis"? [edit: yes, reading your comment above https://news.ycombinator.com/item?id=42426184 https://news.ycombinator.com/item?id=42426184 it seems you are. Read on please, those are not the same thing] Program verification means you already have a program, and some specification it must satisfy, and you chack whether the program satisfies the specification. "Program synthesis" means you don't have a program, only a specification, and you generate a program that satisfies the specification. These are two different tasks, although related, and most program synthesisers will verify the correctness of candidate programs. But they're two different tasks- and btw neither can be done by LLMs. The article above is discussing the computational hardness of generating correct program code with LLMs, i.e of program synthesis, not of verification. So could you explain what you mean, please? You referred to verification, formal methods, etc before. What do you mean? Also, could you avoid expressions like "weasel words" and so on? That's just adding noise. I can tell you're feeling hard done by, although I have no idea why and by whom, and I'm sure I have no relation to them so please tone it down and let's have an adult conversation.
    - lmeyerov 2y ago
      The presumption of the article is that software correctness is the same the formal methods (which I lump mainstream classical program synthesis correctness into) is the same as some symbolic software satisfying some strong logical predicate, which, especially in general conditions, is pspace complete. And my repeat response is no, software correctness, e.g., formal software acceptance criteria, is typically something different: "Just" testing. RE:Hardness, it comes from the verification step of most classical synthesizers that use iterative search-based solvers. If verification was 'easy', the problem goes away. Verifiers say 'yes', 'no', and crucially, provide hints for 'try this next'. RE:LLM's can't do. As in my other thread, if still working here, I'd be very much working on the combination of the two, such as where I pointed at below on work by Dawn Song and Terence Tao. (And some of our customer work on security policies and graph query synthesis may still lead us here.) There's a funny irony to statements like "LLMs can't prove..." in that the last decade's program synthesizers popularly rely on, in practice, the impressive engineering tricks that go on inside SMT solvers to hit relevant scale. RE:Weasel words, that is pretty core to my criticism. By pointing out some programs are currently tricky, and especially under classical problem framings such as the above, I see a pattern of pedantic argumentation that the article is representative of. It hinges on a misunderstanding or misrepresentation of the task of writing acceptable software. I can't use the word "correct" here because of it.

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.
- deleted 2y ago
  [deleted]
- YeGoblynQueenne 2y ago
  >> I don't feel like you're reading what I'm writing. I can assure you that I am. >> I do not use LLMs to augment my verification work, because our team do not verify things to gain belief of sufficient correctness. I don't understand where the "verification" part came into the discussion. Who said anything about using LLMs "to augment my verification work"? Are you perhaps confusing "program verification" with "program synthesis"? [edit: yes, reading your comment above https://news.ycombinator.com/item?id=42426184 https://news.ycombinator.com/item?id=42426184 it seems you are. Read on please, those are not the same thing] Program verification means you already have a program, and some specification it must satisfy, and you chack whether the program satisfies the specification. "Program synthesis" means you don't have a program, only a specification, and you generate a program that satisfies the specification. These are two different tasks, although related, and most program synthesisers will verify the correctness of candidate programs. But they're two different tasks- and btw neither can be done by LLMs. The article above is discussing the computational hardness of generating correct program code with LLMs, i.e of program synthesis, not of verification. So could you explain what you mean, please? You referred to verification, formal methods, etc before. What do you mean? Also, could you avoid expressions like "weasel words" and so on? That's just adding noise. I can tell you're feeling hard done by, although I have no idea why and by whom, and I'm sure I have no relation to them so please tone it down and let's have an adult conversation.
  - lmeyerov 2y ago
    The presumption of the article is that software correctness is the same the formal methods (which I lump mainstream classical program synthesis correctness into) is the same as some symbolic software satisfying some strong logical predicate, which, especially in general conditions, is pspace complete. And my repeat response is no, software correctness, e.g., formal software acceptance criteria, is typically something different: "Just" testing. RE:Hardness, it comes from the verification step of most classical synthesizers that use iterative search-based solvers. If verification was 'easy', the problem goes away. Verifiers say 'yes', 'no', and crucially, provide hints for 'try this next'. RE:LLM's can't do. As in my other thread, if still working here, I'd be very much working on the combination of the two, such as where I pointed at below on work by Dawn Song and Terence Tao. (And some of our customer work on security policies and graph query synthesis may still lead us here.) There's a funny irony to statements like "LLMs can't prove..." in that the last decade's program synthesizers popularly rely on, in practice, the impressive engineering tricks that go on inside SMT solvers to hit relevant scale. RE:Weasel words, that is pretty core to my criticism. By pointing out some programs are currently tricky, and especially under classical problem framings such as the above, I see a pattern of pedantic argumentation that the article is representative of. It hinges on a misunderstanding or misrepresentation of the task of writing acceptable software. I can't use the word "correct" here because of it.