3 ms·

The first question is not the question I'd like answered. What I want to know is this: > Why does the computer have to work within a CONSISTENT formal system F

by moefh 2y ago

The first question is not the question I'd like answered. What I want to know is this: > Why does the computer have to work within a CONSISTENT formal system F? Humans are allowed to make mistakes (i.e., be inconsistent). If we don't give the computer the same benefit, you don't need Godel's theorem to show that the human is more capable than the computer: it is so by construction.

deleted 2y ago
[deleted]
enugu 2y ago
Take a group of humans who each make observations and deductions, possibly faulty. Then, they do extensive checking of their conclusions by interacting with humans and computer proof assistants etc. Let us name this process as HC. A program which can simulate individual humans should also be able to simulate HC - ie. generate proofs which are accepted by HC. --- Penrose's conclusion in the book is more weak - that a knowably correct process cannot simulate humans. We now have LLMs which hallucinate etc that are not knowably correct. But, after reasoning based methods, they can try to check their output and arrive at better conclusions, as is happening currently in popular models. This is fine, and is allowed by Penrose's argument. The argument is applied to the 'generate, check, correct' process as a whole.
- moefh 2y ago
  I don't have a problem with that. (I don't see how that relates to Godel's theorem, tough. If that's the current position held by Penrose, I don't disagree with him. But seeing the post's video makes me believe Penrose still stands behind the original argument involving Godel's theorem, so I don't know what to say...)
  - enugu 2y ago
    That a knowably correct program cant simulate human reasoning is basically Godel's theorem. One can use a diagonalization argument similar to Godel's proof for programs which try to deciding which Turing machines halt. Given a program P which is partially applicable, but always correct, we can use diagonalization to construct P' a more widely applicable and correct program ie. P' can say that some Turing machine will not halt while P is undecided. P'. So, this doesn't involve any logic or formal systems, but it is more general - Godel's result is a special case as the fact that a Turing machine halts can be encoded as a theorem and provability in a formal system can be encoded as a Turing machine. Penrose indeed, believes both in the stronger claim - a program can't simulate humans and the weaker claim, a knowably correct program can't simulate humans. The weaker claim being unassailable firstly shows that most of the usual objections are not valid and secondly, it is hard to split the difference ie. to generate the output of HC using a program which is not knowably correct. A program whose binary is uninterpretably but by magic only generates true theorems. Current AI systems including LLMs don't even come close.

by moefh 2y ago

deleted 2y ago

[deleted]

enugu 2y ago

Take a group of humans who each make observations and deductions, possibly faulty. Then, they do extensive checking of their conclusions by interacting with humans and computer proof assistants etc. Let us name this process as HC. A program which can simulate individual humans should also be able to simulate HC - ie. generate proofs which are accepted by HC. --- Penrose's conclusion in the book is more weak - that a knowably correct process cannot simulate humans. We now have LLMs which hallucinate etc that are not knowably correct. But, after reasoning based methods, they can try to check their output and arrive at better conclusions, as is happening currently in popular models. This is fine, and is allowed by Penrose's argument. The argument is applied to the 'generate, check, correct' process as a whole.

moefh 2y ago
I don't have a problem with that. (I don't see how that relates to Godel's theorem, tough. If that's the current position held by Penrose, I don't disagree with him. But seeing the post's video makes me believe Penrose still stands behind the original argument involving Godel's theorem, so I don't know what to say...)
- enugu 2y ago
  That a knowably correct program cant simulate human reasoning is basically Godel's theorem. One can use a diagonalization argument similar to Godel's proof for programs which try to deciding which Turing machines halt. Given a program P which is partially applicable, but always correct, we can use diagonalization to construct P' a more widely applicable and correct program ie. P' can say that some Turing machine will not halt while P is undecided. P'. So, this doesn't involve any logic or formal systems, but it is more general - Godel's result is a special case as the fact that a Turing machine halts can be encoded as a theorem and provability in a formal system can be encoded as a Turing machine. Penrose indeed, believes both in the stronger claim - a program can't simulate humans and the weaker claim, a knowably correct program can't simulate humans. The weaker claim being unassailable firstly shows that most of the usual objections are not valid and secondly, it is hard to split the difference ie. to generate the output of HC using a program which is not knowably correct. A program whose binary is uninterpretably but by magic only generates true theorems. Current AI systems including LLMs don't even come close.