4 ms·

The thing is, all these stacks are built by people and verified against specifications. When they failed to perform the way they should, we fixed them. Plus, a

The thing is, all these stacks are built by people and verified against specifications. When they failed to perform the way they should, we fixed them. Plus, all the parts are deterministic in this stack. Their behavior is fixed for a given input, and all the parts are interpretable, readable, verifiable and observable. LLMs are none of that. They are stochastic probability machines, which are nondeterministic. We can't guarantee their output's correctness, and we can't fix them to guarantee correct output. They are built on tons of (unethically sourced) data, which has no correctness and quality guarantees. Some people will love LLMs, and/or see programming as a task/burden they have to complete. Some of us love programming for the sake of it, and earn money by doing it that way, too. So putting LLMs to the same bucket with a deterministic, task specific programming tool is both wrong, and disservice to both. I'm also strongly against LLMs, not because of the tech, but because of how they are trained and how their shortcomings are hid and they're put forward as the "oh the savior of the woeful masses, and the silver bullet of all thy problems", and it's neither of them. LLMs are just glorified tech demos which shows what stochastic parrots can pose as accomplishing when you feed the whole world to them.

red75prime 2y ago
> We can't guarantee their output's correctness We can (for programming, at least): run the output thru theorem prover, ensure that proof is constructive, the Curry-Howard correspondence guarantees that you can turn the output into a correct program. It doesn't guarantee that formal properties of the program correspond to the informal problem statement. But even people occasionally make such errors (a provably correct program doesn't do what we wanted it to do). > and we can't fix them to guarantee correct output Same thing with other systems capable of programming. That is people. You just can't make a system that guarantees correct transformation from an informal problem statement into a formally correct implementation. "Informal" implies that there's wiggle room for interpretation. No, it doesn't mean that current LLMs are ready to replace programmers, it also doesn't mean that ML models of 2030s will not be able to.
- bamboozled 2y ago
  This doesn’t mean the LLM is deterministic. It means it can spoof the right answer give enough time.
  - red75prime 2y ago
    Indeterminism is not always bad. A probabilistic Turing machine is more powerful than a Turing machine, for example (BPP complexity class is a superset of P).
    - bamboozled 2y ago
      Yeah, didn't mean to imply something was bad or good here, just that it's not a purely deterministic thing.
- QuantumGood 2y ago
  Curry–Howard correspondence = direct relationship between computer programs and mathematical proofs
- YeGoblynQueenne 2y ago
  >> We can (for programming, at least): run the output thru theorem prover, ensure that proof is constructive, the Curry-Howard correspondence guarantees that you can turn the output into a correct program. It doesn't guarantee that formal properties of the program correspond to the informal problem statement. But even people occasionally make such errors (a provably correct program doesn't do what we wanted it to do). That sounds very ambitious. Automated theorem provers are real sticklers for complete specifications in a formal language and can't parse natural language at all, but when you generate code with an LLM all you have in terms of a specification is a natural language prompt (that's your "informal problem statement"). In that case what exactly is the prover going to prove? Not the natural language prompt it can't parse! The best you can do if you start with a natural language specification, like an LLM prompt, is to verify that the generated program compiles, i.e. that it is correct syntactically. As to semantic correctness, there, you're on your own. Edit: I'm not really sure whether you're talking about syntactic or semantic correctness after all. Which one do you mean? >> You just can't make a system that guarantees correct transformation from an informal problem statement into a formally correct implementation. "Informal" implies that there's wiggle room for interpretation. Note that in program synthesis we usually make a distinction between complete and incomplete specifications ("problem statements") not formal and informal. An incomplete specification may still be given in a formal language. And, for the record, yes, you can make a system that guarantees that an output program is formally consistent with an incomplete specification. There exist systems like that already. You can find a bit about this online if you search for "inductive program synthesis" but the subject is spread over a wide literature spanning many fields so it's not easy to get a clear idea about it. But, in general, it works and there are approaches that give you strong theoretical guarantees of semantic correctness.
skybrian 2y ago
Yep. LLM’s don’t guarantee any interesting mathematical properties. That’s up to you. This why you should write good tests, review the code, and don’t approve anything you don’t understand. It’s not a reason to reject pretty good autocomplete, though.
malux85 2y ago
> "oh the savior of the woeful masses, and the silver bullet of all thy problems" Who said that? Everyone I've talked to warns about their shortcomings (including their creators) and even the platform where I use them has a warning plastered right under the input box saying "ChatGPT can make mistakes. Check important info."
jinen83 2y ago
I would argue thats an LLM spec --> Generate probabilistic output with a degree of confidence on the output nearing p(1). IMHO End users are supposed to not take the output of these machines as is but rather iterate on top and finish their task in lesser time.

red75prime 2y ago

> We can't guarantee their output's correctness We can (for programming, at least): run the output thru theorem prover, ensure that proof is constructive, the Curry-Howard correspondence guarantees that you can turn the output into a correct program. It doesn't guarantee that formal properties of the program correspond to the informal problem statement. But even people occasionally make such errors (a provably correct program doesn't do what we wanted it to do). > and we can't fix them to guarantee correct output Same thing with other systems capable of programming. That is people. You just can't make a system that guarantees correct transformation from an informal problem statement into a formally correct implementation. "Informal" implies that there's wiggle room for interpretation. No, it doesn't mean that current LLMs are ready to replace programmers, it also doesn't mean that ML models of 2030s will not be able to.

bamboozled 2y ago
This doesn’t mean the LLM is deterministic. It means it can spoof the right answer give enough time.
- red75prime 2y ago
  Indeterminism is not always bad. A probabilistic Turing machine is more powerful than a Turing machine, for example (BPP complexity class is a superset of P).
  - bamboozled 2y ago
    Yeah, didn't mean to imply something was bad or good here, just that it's not a purely deterministic thing.
QuantumGood 2y ago
Curry–Howard correspondence = direct relationship between computer programs and mathematical proofs
YeGoblynQueenne 2y ago
>> We can (for programming, at least): run the output thru theorem prover, ensure that proof is constructive, the Curry-Howard correspondence guarantees that you can turn the output into a correct program. It doesn't guarantee that formal properties of the program correspond to the informal problem statement. But even people occasionally make such errors (a provably correct program doesn't do what we wanted it to do). That sounds very ambitious. Automated theorem provers are real sticklers for complete specifications in a formal language and can't parse natural language at all, but when you generate code with an LLM all you have in terms of a specification is a natural language prompt (that's your "informal problem statement"). In that case what exactly is the prover going to prove? Not the natural language prompt it can't parse! The best you can do if you start with a natural language specification, like an LLM prompt, is to verify that the generated program compiles, i.e. that it is correct syntactically. As to semantic correctness, there, you're on your own. Edit: I'm not really sure whether you're talking about syntactic or semantic correctness after all. Which one do you mean? >> You just can't make a system that guarantees correct transformation from an informal problem statement into a formally correct implementation. "Informal" implies that there's wiggle room for interpretation. Note that in program synthesis we usually make a distinction between complete and incomplete specifications ("problem statements") not formal and informal. An incomplete specification may still be given in a formal language. And, for the record, yes, you can make a system that guarantees that an output program is formally consistent with an incomplete specification. There exist systems like that already. You can find a bit about this online if you search for "inductive program synthesis" but the subject is spread over a wide literature spanning many fields so it's not easy to get a clear idea about it. But, in general, it works and there are approaches that give you strong theoretical guarantees of semantic correctness.

skybrian 2y ago

Yep. LLM’s don’t guarantee any interesting mathematical properties. That’s up to you. This why you should write good tests, review the code, and don’t approve anything you don’t understand. It’s not a reason to reject pretty good autocomplete, though.

malux85 2y ago

> "oh the savior of the woeful masses, and the silver bullet of all thy problems" Who said that? Everyone I've talked to warns about their shortcomings (including their creators) and even the platform where I use them has a warning plastered right under the input box saying "ChatGPT can make mistakes. Check important info."

jinen83 2y ago

I would argue thats an LLM spec --> Generate probabilistic output with a degree of confidence on the output nearing p(1). IMHO End users are supposed to not take the output of these machines as is but rather iterate on top and finish their task in lesser time.