that seems reasonable, as it is the lowest common denominator for interoperability
what would be unfortunate is if it was in some format that couldn't be used by most other systems without extra work, and if the user wasn't able to use their own property to export their own passwords in a different format.
Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove. Otherwise, what happens if the LLM includes an underhanded addition to the lean code which leads it to output a false positive?
> Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove.
Yes:
> The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say)
However, it is much easier to manually check whether the statement of the conjecture was formalized correctly than to manually check the whole proof.
People also need to be cautious with potential adversarial proofs. Like don't decide to give money on a sure-bet thing, just because they have a Lean proof. Not saying that these AI labs would do this.
They used words to mean what the words mean. What specific issue do you take with that?
"prompt", as in prompting an AI, has the same definition as "prompt", as in prompting a person. They mean the same thing, that's why the term was applied to AI after already applying people.
*Jingle-jangle fallacies are erroneous assumptions that either two different things are the same because they bear the same name (jingle fallacy); or two identical or almost identical things are different because they are labeled differently (jangle fallacy).[1][2][3] The term was coined by Truman Lee Kelley in his 1927 book Interpretation of educational measurements.[4] In research, a jangle fallacy is the inference that two measures (e.g., tests, scales) with different names measure different constructs. By comparison, a jingle fallacy is the assumption that two measures which are called by the same name capture the same construct.[5][6][7]
You are simply incorrect. It is not a fallacy of that type, or any other type, because the words do, in fact, mean the same thing, as multiple people have pointed out here. Whether referring to chatbots or people, "prompt" means "to move to action".
If you have some reliable source supporting your unilateral claims that "prompt" does not mean this, please share. Otherwise, the consensus seems to be contrary to your claims.
Why do I need a source? An LLM prompt does not "move to action", because an LLM does not act. People act, animals act, software doesn't act. Acting implies volition and volition implies cognition and if you think that LLMs have those things then you're the one who should provide a source for your claim.
How about an LLM connected to a robotic arm. What then?
As for cognition - can you prove that you possess it, to an external observer? Could you, confined to a box through which you can only communicate through textual messages, prove that you are thinking, and not just responding through a mechanistic process?
Absolutely you do. I can’t prove that I have cognition. I merely have the impression that I do, and we accept as a general axiom that others do too - but it is not provable. You are examining a system from within the confines of that system.
And you’re seriously going with “don’t ask inconvenient questions” as an argument?
>> And you’re seriously going with “don’t ask inconvenient questions” as an argument?
Where did I say that?
The conversation you seem to want to have doesn't seem to have any obvious use and you seem to want to debate a point I never made. I don't seem to be needed here so I will now bow out of the conversation.
That commenter was already obnoxious under this thread, and today they are relitigating Searle-Turing via Hofstadter GEB slop, so they are also an ignoramus.
Because your entire post is a personal, philosophic opinion on what words should mean, and how if someone disagrees with this personal opinion of 1/7,000,000,000 of people, then they are wrong. Every single one of these claims is unsupported and contradicted by reliable sources like a dictionary:
> An LLM prompt does not "move to action"
> an LLM does not act
> software doesn't act
> Acting implies volition
The only way such opinions could viably be considered "true" is if you convinced a majority of people to agree with you on the changes, which you decidedly have not.
Until you do, we can go by the existing definitions: "prompt" means "to move to action", "act" means "the doing of a thing" (note the absence of "volition" or "cognition" in the actual definition), and by all reasonable accounts, LLMs "do things".
I mean, just take a step back and dispassionately look at your ridiculous claim that nobody prompts LLMs (because you now claim only a human can be prompted, because only living creatures can do a thing). Do you really think you can gain consensus from folks on that claim?
There are many differences between LLMs and people, but this is not one of them, according to all reliable sources I've found so far. Feel free to share the reliable sources which led you to your personal conclusion here.
I'm not going articulate the answer but I will say whatever beef you have with the other commenter (or me), just copy this thread into ChatGPT and it will tell you why you are more in the wrong.
> There is a caveat that they "can't rule out" the possibility that Tristan's Codex data could have been part of the training set of the new model, though it is described as "unlikely"
This is the lynchpin behind everything, and I would describe it as "likely". Since I am not employed by any party to this dispute, my 1 opinion is more trustworthy than OpenAI blog poster's 1 opinion.
Like everyone else in the world is an NPC whose perspective can be ignored or overruled by this one dude.
reply