Colorless green DNNs sleep furiously in an unexplainable fantasy
cacm.acm.org
cacm.acm.org
On the other hand, the strong Church-Turing thesis is that nothing is more powerful than a Turing machine when it comes to solving halting problems, including humans. This is not proven or really provable but it seems more likely than not (humans certainly don't seem especially good at solving halting problems in general).
If the Church-Turing thesis is true (at least as applied to humans), discovering valid, halting programs by heuristic using a machine isn't barred by the halting problem as far as I can tell.
In other words, humans almost certainly aren't solving halting problems when they program, why should computers necessarily have to? Humans mess up and produce programs that don't halt or don't produce the output they expect all the time, but we still produce useful programs at least sometimes, even if we can't know for sure which programs are which.
I'm very surprised someone a whole essay like this and have this misconception.
I was half expecting to see "humans building something smarter than human machines violates the laws of thermodynamics" next.
Mathematicians have spilled a bunch of ink explaining why Penrose didn't understand Godel's proof.
The question of whether human perception of mathematical truth is infallible is open to philosophical debate. Penrose distinguishes between mistakes, which all mathematicians make but which in principle they can later come to recognise as mistakes, and true incorrect perception of mathematical truth, where no amount of checking, re-derivation, etc. could possibly right the incorrect perception. His view is that the latter type of error does not exist, that there is a mathematical ground truth that we can directly perceive and that is infallible, and that the mistakes made by mathematicians are of a different nature to inconsistencies in that perception of mathematical ground truth.
Penrose went too far in presenting this argument as a proof of the impossibility of strong AI based on algorithms. The point about human perception of mathematical truth can very reasonably be disputed, and is part of a much larger debate about the fundamental nature of maths that is far from settled. Personally, though, my intuition is that Penrose is right about the human perception of mathematical truth, and I therefore find the Godel-based argument persuasive. It's not a proof because it rests on an assumption that has not been proven, but I find it convincing to the extent that I tend to think that the assumption is probably true.
So the debate is a philosophical one more than it is a mathematical one, and while Penrose may be guilty of some rather bad PR, accusing him of "not understanding Godel's proof" does him a disservice.
* Yes, there's no Nobel prize in mathematics, but he is a mathematician (as well as a physicist) and he has won a Nobel prize.
> He rightly observed that Godel's incompleteness theorem requires that either human minds are capable of things algorithms are not capable of...
"Formal system of logic" maps well onto Turing machines, and Turing machines map onto "any computer system" if you are very abstract about it.
Now, people are wrong about mathematical facts, but seemingly not forever. We puzzle it over, come back to it, someone makes a breakthrough. It doesn't seem like there is a fixed blind spot where our logic breaks down.
So what are people doing that is not captured by a formal system of logic?
Options:
1. The mapping of Turing machines to computers isn't airtight - they are doing something "more" than a TM with infinite time + space is capable of
2. People are not "more than" an infinite TM either, we just romantically believe we are, and ignore our own flaws
3. People are doing something special that is not captured by our theory of computation
He proved they can be inconsistent, or incomplete. The ones that mathematicians work with are incomplete and assumed to be consistent[0], namely that there are statements which are true, but not provable, within that system. Consistent-but-incomplete systems don't have any contradictions or logical holes; they just can't determine the truth of every possible statement.
From an incomplete system you can build a "more powerful" system- one with another axiom that makes more things provable without contradicting anything in the original one.
In inconsistent systems, everything is provable, even statements' own negations, so they aren't very useful.
[0] one statement that you can't prove within a (sufficiently powerful) system is "this system is consistent."
All the limits that exist for computing machines almost certainly exist for us too; we don't need to solve the halting problem; we don't solve large NP-hard problems; etc.
Of course, if one believes there's something mystical about brains -- whether a soul or access to quantum computing -- perhaps one would disagree.
Since humans don't seem to be particularly good at solving the halting problem even for very small TMs, it doesn't seem that likely to me that we are categorically stronger at it than computers, whether our cognition is truly "computation" or not.
And of course all programs of practical significance are finite state machines (since there is only a finite number of atoms in the universe).
You and I both intuit that there are conjectures that, likely, do not have a solution. The author is proposing (and maybe rightly) that an AI as a Turing machine with this intuition would inherently (have to) be a Turing Oracle...
It's an interesting take that has some implications...
> Plus, the halting problem only says that you can't have a procedure which will be 100% right on 100% of programs about whether or not they halt.
Your missing it still...
"Given a computer program and an input, will the program terminate or will it run forever?"
We both know that the collatz conjecture likely wont ever halt. We understand that. WE are reasonable oracles. Now write me an oracle that can detect this. Dont feed a list of problems to avoid, write a program that detects these types problems and skips them... Hint, you likley cant. You could simulate one, but that would be cheating...
A real AI needs this, or needs to be able to do it, or it risks working on the collatz conjecture till the heat death of the universe, or till it consumes the universe in a paperclip style problem...
The implication is that real ai might not come out of a Turing machine ever...
The latter claim doesn't follow: programmers aren't Turing oracles either. A programming machine that can emulate whatever humans are doing when they program, would be able to program too.
Speak for yourself. I know that the Collatz Conjecture is an unsolved problem and so wouldn't make any strong statements about it.
First: most practical problems are computable, and most practical programs do not run forever. Even if an agent had to run a program to termination, it could still use the feedback gathered from running it to make modifications.
Second: an agent with a sufficiently good intermediate representation _which is computable_ doesn't need to actually execute a program to model its behavior. Humans do this all the time--we can read code and understand its approximate function as a means to edit it. I don't want to claim that LLMs have a concept of "understanding," but they definitely build an intermediate representation which, when combined with external input (e.g. having to kill a program, because it exceeded a timeout), can be used to modify the program.
Now with all of that said: I don't feel confident about whether or not AI is actually serious risk to programmers, I just don't feel as if this argument is sufficiently compelling.
As part of the argument on explainability, the author says "we have known for some time these models cannot represent or model symbolic structures". There might be some particular weird way of defining things where this is true, but it's certainly not true in the most basic reading. In fact, we have very strong theoretical results that a sufficiently wide neural network can compute any function, including those that are "symbolic". Whether they can be trained using gradient optimization to compute every function is an open problem, but the idea that there are functions they can't represent is provably false.
The third point, that LLM's aren't as step towards AGI. They again make the claim that there are functions a DNN can't compute (or approximate arbitrarily well) (see https://en.wikipedia.org/wiki/Universal_approximation_theore... for the theorem that this isn't true).
The rest of this point, and the fourth point, are basically just about how current LLM's are actually pretty dumb in a lot of situations. This is the only argument that's actually compelling to me; there's a lot of hype around LLMs and their abilities, but a lot of that might have to do with our brains being happy to paper over flaws to anthropomorphize things. And the fact that we haven't yet learned what to look for in artificial output, like we spent decades doing for other machine outputs before LLMs. Recall that when dumb pattern matching conversation bots were invented in the 60s (https://en.wikipedia.org/wiki/ELIZA), people thought they couldn't possibly be artificial and must really be human, even though they are obviously artificial by todays standards.
So, I agree that we don't know if LLM's are the first step towards AGI, and they probably aren't in a sense more than the fact that inventions tend to build on each other. But we don't have enough information to say definitively that they aren't that first step.
Things like alphafold would suggest to me that this doesn’t always hold true.
Perhaps a matter of definition but to me there does seem to be “some” problem solving ability. And once you’ve got even a little of that then it’s a scaling question and not really compatible with “ can never be automated.”
I do see a compelling argument on the limits of LLMs being probabilistic (rather than logic/symbolic), as I’ve seen on GPT/Pilot coming up with code that looks syntactically valid but calls completely made-up APIs.
Not necessarily. It could (in theory) prove through formal methods that A solves P.
>Lists a bunch of totally human failings
Great argument.
Dude, 99.999% of programming today is writing HTML.