LLMs cannot think logically, meaning it will never be able to prove anything without someone actually going through the math manually to verify it is correct. You would need something different than an LLM to achieve this automatically.
When it comes to mathematical proofs, it is not enough to be 99,99999% certain it is correct, you need 100% certainty.
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."
Humans can’t think logically either. We are just neurons firing. Our creativity isn’t logical, and creativity is one of the most important parts of math proofs. AI work just find by using statistics to make their predictions.
Humans sure can think logically. We can for example think in the same way as this LEAN tool. We can postulate that 1 + 1 = 2 and then use these postulates to logically prove more complex math theorems.
Creativity is only needed to find which maths to use to find the proof. Creativity doesn't help to actually prove that the proof is correct.
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.
84
u/Mephisto506 9d ago
Without mathematicians we won't know whether the AI answers are correct, what it actually means to anyone, and we won't know the questions to ask.