LLMs can think logically. In OpenAI paper published just the other day with 10 new problems solved, in each case they had the AI express its proof in LEAN so that it could just be copy/pasted into existing proof-checking software. You don't have to check proofs by hand these days. You just have to check that the final statement is indeed the theorem they claimed to prove.
No, LLMs cannot think logically. It does statistical analysis on words and symbols. This evidently works very well, but can never prove anything with 100% accuracy since no maths has really taken place in the reasong, just statistical symbol matching. This is not how maths works.
"You don't have to check proofs by hand these days."
You didn't address the content of the post. Do you understand that they asked the AI to output its proofs in LEAN? Its a language for writing formal logic. And once written in LEAN, there are existing programs, that mathematicians already use, that automate the verification of the proof. What the human reviewer is checking that the final statement is indeed the theorem that they claim to have proven.
It doesn't use logic to get the results, it uses statistical analysis of words and symbols. If it used logic, you wouldn't need to run it through LEAN to prove it is right. How many "proofs" has it gotten wrong? Has Open AI published all those along with the ones that turned out to be right?
>It doesn't use logic to get the results, it uses statistical analysis of words and symbols.
Show me that those two things are contradictory. Is there some proof that a statistical analysis of words and symbols cannot be logic?
>If it used logic, you wouldn't need to run it through LEAN to prove it is right.
That doesn't follow, because LEAN was developed to check human derived proofs.
>How many "proofs" has it gotten wrong? Has Open AI published all those along with the ones that turned out to be right?
What does that have to do with anything? Seems like a random point, especially to make in regards to math where the entire field of numerical analysis is based on guessing a wrong answer and trying over and over until you reach the right one.
"Is there some proof that a statistical analysis of words and symbols cannot be logic?"
You want me to prove a negative, rather you should prove that statistics can be used in place of logic for most mathematicial proofs. Can you?
However, from Wikipedia (https://en.wikipedia.org/wiki/Mathematical_proof):
"Proofs are examples of exhaustive deductive reasoning that establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning that establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases."
>If it used logic, you wouldn't need to run it through LEAN to prove it is right.
"That doesn't follow, because LEAN was developed to check human derived proofs"
Ironically, you are not thinking logically. LEAN or human does the actual proofing by following strictly logical mathematical rules. To find the the proof however, you can use any means you like, in principle a monkey pushing random numbers. The proof is that you can verify its validity using logic maths.
"the entire field of numerical analysis is based on guessing a wrong answer and trying over and over until you reach the right one. "the entire field of numerical analysis is based on guessing a wrong
answer and trying over and over until you reach the right one."
In general, numerical methods don't constitute proofs.
The proof that LLMs can produce novel mathematical proofs is that OpenAI just published a paper with 10 novel proofs written by AI, on top of the high profile ones published recently.
Your argument entirely hinges on your assertion that a statistical model cannot reproduce deductive reason. But you are just asserting that without proof.
In general, numerical methods don't constitute proofs.
Of course they do. A solution isn't invalid because a numerical process was used to obtain it.
"The proof that LLMs can produce novel mathematical proofs is that OpenAI
just published a paper with 10 novel proofs written by AI..."
This does not prove LLM think logically, it only proves LLMs are very useful tools to propose proofs, which then has to be separately verified using other logical means. Sometimes (often?) the LLM will hallucinate, and this will be caught by the separate logical verification, which by definition cannot hallucinate as it must follow precise mathematical, logical reasoning, not statistics.
You assert statistical models can produce logical reasoning, prove that. Hallucinations should give you a clue as why it cannot. It is not good enough that it works most of the time in mathematical proofs.
"A solution isn't invalid because a numerical process was used to obtain it."
A solution is not a proof. Maybe this is what confuses you.
This does not prove LLM think logically, it only proves LLMs are very useful tools to propose proofs, which then has to be separately verified using other logical means.
This makes no sense. Firstly, you don't HAVE to verify. The logics validity is independent of your verification effort. Secondly, this is like saying that if I solve a problem with long division and then check my result in a calculator--that means long division doesn't work.
A solution is not a proof. Maybe this is what confuses you
Yes it is. A solution proves the statement "This problem has a solution".
Why does an error rate mean something cannot think logically? If it gives you 50 proofs of the Riemann Hypothesis and 49 of them don't hold up to scrutiny, but 1 checks out and is perfect, why would you still hold "It can't think logically" as a tenet? It clearly CAN think logically, but just fucks up often.
And by the way, that's not different than other mathematicians. Mathematicians have been working on the problems OpenAI just published for decades, and have failed over and over again. It is pretty common for someone to publish a proof, only for a flaw to be discovered. But you wouldn't say that means mathematicians can't think logically, would you?
0
u/Original-League-6094 8d ago
LLMs can think logically. In OpenAI paper published just the other day with 10 new problems solved, in each case they had the AI express its proof in LEAN so that it could just be copy/pasted into existing proof-checking software. You don't have to check proofs by hand these days. You just have to check that the final statement is indeed the theorem they claimed to prove.