Comment by mindwok
6 days ago
Sure,
> In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified.
"As specified" here being the key phrase. This is defined however you want, and ranges from a person saying "yep, behaves as specified", to a formal proof. Modern language language models are trained under RL for both sides of this spectrum, from "Hey man looks good", to formal theorem proving. See https://arxiv.org/html/2502.08908v1.
So I'll return to my original point: LLMs are not just generating outputs that look plausible, they are generating outputs that satisfy (or at least attempt to satisfy) lots of different objectives across a wide range of requirements. They are explicitly trained to do this.
So while you argue over the semantics of "correctness", the rest of us will be building stuff with LLMs that is actually useful and fun.
You have to actually read more than the first line of a Wikipedia article to understand it
You're using Coq and Lean?
I'm actually not convinced you read the paper. It doesn't have anything to do with your argument. Someone using LLMs with formal verification systems is wildly different than LLMs being formal verification systems.
This really can't work if you don't read your own sources
> they are generating outputs that satisfy (or at least attempt to satisfy) lots of different objectives across a wide range of requirements
No they aren't. You were lied to by the hype machine industry. Sorry.
The good news is that there's a lot of formerly intractable problems that can now be solved by generating plausible output. Programming is just not one of them.
> No they aren't. You were lied to by the hype machine industry. Sorry.
Ok. My own empirical evidence is in favour of these things being useful, and useful enough to sell their output (partly), but I'll keep in mind that I'm being lied to.
Quite a huge leap from "these things are useful" to "these things can code".
(And yes, this leap is the lie you're being sold. "LLMs are kinda useful" is not what led to the LLM trillion dollar hype bubble.)
1 reply →