Given that I think that capturing the ingenuity of human mathematicians is one of the last things I’d expect to see before seeing human-level-or-smarter AI, the poor state of automated theorem proving doesn’t seem to me like much evidence on how far away GAI might be.
Why is the ingenuity of human mathematicians one of the last things that you’d expect to see before seeing human-level-or-smarter AI? My intuition is that it’s one of the earlier things that you’d expect to see. Mikhail Gromov wrote:
The mathematical ability of each person’s brain by far exceeds those of the greatest geniuses of all time. Nobody, given the input the brain starts with, could be able to arrive at such a level of abstraction, for instance, as the five-fold symmetry (for example, a starfish), which you, or rather your brain, recognizes instantaneously regardless of a particular size, shape, or color of an object.
That’s a different meaning of the term “mathematical ability”. In this context, you should read it as “calculating ability”, and computers are pretty good at that—although still not as good as our brains.
It was not intended to imply that low-level brainware is any good at abstract mathematics.
Where did you get your interpretation from, and why do you think that yours is more accurate than mine? :-)
I believe that he was referring to the brain’s pattern recognition ability rather than calculating ability. Existing supercomputers have a lot of calculating ability, but they can’t recognize five-fold symmetry regardless of a particular size, shape or color of an object.
This is interesting to me, and I had not known that such research has been done.
I’ve heard that there’s a consistent problem in machine learning of people overtraining their algorithms to particular data sets. The diversity of examples in the paper appears to be impressive, but it could be that the algorithm would break if given images that would appear to us to be qualitatively similar to the ones displayed.
I think that Gromov may not have expressed himself very clearly, and his remarks may not have been intended to be taken literally. Consider the many starfish in this picture. By looking at the photo, one can infer that any given star-fish has five-fold symmetry with high probability, even though some of the ones in the distance wouldn’t look like they had five-fold symmetry (or even look like star-fish at all) if they were viewed in isolation. I don’t think that existing AI has the capacity to make these sorts of inferences at a high level of generality.
I think #3 is the real issue. Most of the starfishes in that picture aren’t 5-fold symmetric, but a person who had never seen starfish before would first notice “those all look like variations of a general form” and then “that general form is 5-fold symmetric”. I don’t know of any learning algorithms that do this, but I also don’t know what to search for.
So you’re probably right that it’s an issue of “pattern recognition ability”, but it’s not as bad as you originally said.
Also note that the Sylow theorems are, in some sense, a pretty low bar. Compare with the Feit-Thompson Theorem, which has a proof running 250 pages, and which builds on previously known results. I have a friend who’s a finite group theorist who said that in many cases he struggled to verify the truth of individual lines of the proof.
Given that I think that capturing the ingenuity of human mathematicians is one of the last things I’d expect to see before seeing human-level-or-smarter AI,
Verifying proofs and writing programs are isomorphic. A smarter-than-human theorem prover is likely to also be a better-than-human programmer, and you can ask it to do things like find good theorem provers...
More or less what Strilanc said, and not what gjm said.
The difference between chess and math is that a superhuman-at-theorem-proving AI is a lot more useful for speeding up further AI research than a superhuman-at-chess-playing AI would be. (Not to mention the chance that being better-than-human at mathematical intuition already unlocks enough munchkinning of physics to take over the world directly.)
I’d like to make explicit the connection of this idea to hard takeoff, since it’s something I’ve thought about before but isn’t stated explicitly very often. Namely, this provides some reason to think that by the time an AGI is human-level in the things humans have evolved to do, it will be very superhuman in things that humans have more difficulty with, like math and engineering.
First of all: I hereby apologize to orthonormal if s/he felt insulted or belittled or mocked by what I wrote. That was in no way my intention.
I’m not sure “sarcasm” is quite the right term, though. I really do think that, among human beings, doing mathematics well takes exceptional brainpower, and even most very intelligent people can’t do it; I really do think that playing chess well has the same feature; and I really do think that that feature is why orthonormal expects doing mathematics well to be one of the last achievements of AI before general superhumanness.
If my last paragraph had said “I don’t think that’s very good evidence, though; you could say the same about playing chess well, and we all know what computers have done to that” then it would have been clearer and that might have been worth the loss of brevity. But I’m not sure sarcasm is the failure mode (if failure it be) here.
Following up on JoshuaZ’s comment, humans brains aren’t at all optimized for doing higher math — it’s a mystery that humans can do higher math at all. Humans optimized for things like visual processing and adapting to the cultures that they grow up in. So I would expect human-level math AI to be easier than human-level visual processing AI.
Because doing mathematics well is something that takes really exceptional brainpower and that even most very intelligent people aren’t capable of.
What do you mean by “really exceptional brainpower”? And what do you mean by “doing mathematics well” ?
What I meant was: (1) empirically it seems that very few human beings are good at proving theorems (or even following other people’s proofs), (2) being good at proving theorems seems to correlate somewhat with other things we think of as cleverness, (3) these facts are probably part of why it seems to orthonormal (and, I bet, to lots of others) as if skill in theorem-proving would be one of the hardest things for AI to achieve, but (4) #1 and #2 hold to some extent for other things, like being good at playing chess, that also used to be thought of as particularly impressive human achievements but that seem to be easier to make computers do than all sorts of things that initially seem straightforward.
All of which is rather cumbersome, which is why I put it in the elliptical way I did.
More explicitly, there are a lot of things that humans can do easily that seem to be extremely difficult for AI (vision and language are the most obvious), and there are many things that humans have trouble with that we can easily make AI do a decent job. At some level, this shouldn’t be that surprising because a lot of the things humans find really easy are things we have millions of years of evolution optimizing those procedures.
Given that I think that capturing the ingenuity of human mathematicians is one of the last things I’d expect to see before seeing human-level-or-smarter AI, the poor state of automated theorem proving doesn’t seem to me like much evidence on how far away GAI might be.
Why is the ingenuity of human mathematicians one of the last things that you’d expect to see before seeing human-level-or-smarter AI? My intuition is that it’s one of the earlier things that you’d expect to see. Mikhail Gromov wrote:
That’s a different meaning of the term “mathematical ability”. In this context, you should read it as “calculating ability”, and computers are pretty good at that—although still not as good as our brains.
It was not intended to imply that low-level brainware is any good at abstract mathematics.
Where did you get your interpretation from, and why do you think that yours is more accurate than mine? :-)
I believe that he was referring to the brain’s pattern recognition ability rather than calculating ability. Existing supercomputers have a lot of calculating ability, but they can’t recognize five-fold symmetry regardless of a particular size, shape or color of an object.
Are you sure? This sounds possible.
Possible in principle, but my understanding of the current state of AI is that computer programs are nowhere near being able to do this.
Are you saying we can’t make programs that would identify portions of an image that are highly fold fold symmetric? This seems really unlikely to me.
Some looking turns up a paper on Skewed Rotation Symmetry Group Detection which appears to do this.
This is interesting to me, and I had not known that such research has been done.
I’ve heard that there’s a consistent problem in machine learning of people overtraining their algorithms to particular data sets. The diversity of examples in the paper appears to be impressive, but it could be that the algorithm would break if given images that would appear to us to be qualitatively similar to the ones displayed.
I think that Gromov may not have expressed himself very clearly, and his remarks may not have been intended to be taken literally. Consider the many starfish in this picture. By looking at the photo, one can infer that any given star-fish has five-fold symmetry with high probability, even though some of the ones in the distance wouldn’t look like they had five-fold symmetry (or even look like star-fish at all) if they were viewed in isolation. I don’t think that existing AI has the capacity to make these sorts of inferences at a high level of generality.
I think #3 is the real issue. Most of the starfishes in that picture aren’t 5-fold symmetric, but a person who had never seen starfish before would first notice “those all look like variations of a general form” and then “that general form is 5-fold symmetric”. I don’t know of any learning algorithms that do this, but I also don’t know what to search for.
So you’re probably right that it’s an issue of “pattern recognition ability”, but it’s not as bad as you originally said.
Also note that the Sylow theorems are, in some sense, a pretty low bar. Compare with the Feit-Thompson Theorem, which has a proof running 250 pages, and which builds on previously known results. I have a friend who’s a finite group theorist who said that in many cases he struggled to verify the truth of individual lines of the proof.
Why do you think so?
Verifying proofs and writing programs are isomorphic. A smarter-than-human theorem prover is likely to also be a better-than-human programmer, and you can ask it to do things like find good theorem provers...
More or less what Strilanc said, and not what gjm said.
The difference between chess and math is that a superhuman-at-theorem-proving AI is a lot more useful for speeding up further AI research than a superhuman-at-chess-playing AI would be. (Not to mention the chance that being better-than-human at mathematical intuition already unlocks enough munchkinning of physics to take over the world directly.)
Because doing mathematics well is something that takes really exceptional brainpower and that even most very intelligent people aren’t capable of.
Just like chess.
I’d like to make explicit the connection of this idea to hard takeoff, since it’s something I’ve thought about before but isn’t stated explicitly very often. Namely, this provides some reason to think that by the time an AGI is human-level in the things humans have evolved to do, it will be very superhuman in things that humans have more difficulty with, like math and engineering.
I’m against sarcasm as a way of making an argument; it makes it less pleasant to discuss things here, and it can hide a bad argument.
First of all: I hereby apologize to orthonormal if s/he felt insulted or belittled or mocked by what I wrote. That was in no way my intention.
I’m not sure “sarcasm” is quite the right term, though. I really do think that, among human beings, doing mathematics well takes exceptional brainpower, and even most very intelligent people can’t do it; I really do think that playing chess well has the same feature; and I really do think that that feature is why orthonormal expects doing mathematics well to be one of the last achievements of AI before general superhumanness.
If my last paragraph had said “I don’t think that’s very good evidence, though; you could say the same about playing chess well, and we all know what computers have done to that” then it would have been clearer and that might have been worth the loss of brevity. But I’m not sure sarcasm is the failure mode (if failure it be) here.
Following up on JoshuaZ’s comment, humans brains aren’t at all optimized for doing higher math — it’s a mystery that humans can do higher math at all. Humans optimized for things like visual processing and adapting to the cultures that they grow up in. So I would expect human-level math AI to be easier than human-level visual processing AI.
What do you mean by “really exceptional brainpower”? And what do you mean by “doing mathematics well” ?
What I meant was: (1) empirically it seems that very few human beings are good at proving theorems (or even following other people’s proofs), (2) being good at proving theorems seems to correlate somewhat with other things we think of as cleverness, (3) these facts are probably part of why it seems to orthonormal (and, I bet, to lots of others) as if skill in theorem-proving would be one of the hardest things for AI to achieve, but (4) #1 and #2 hold to some extent for other things, like being good at playing chess, that also used to be thought of as particularly impressive human achievements but that seem to be easier to make computers do than all sorts of things that initially seem straightforward.
All of which is rather cumbersome, which is why I put it in the elliptical way I did.
Heh, I missed the irony :-)
I didn’t, but realized someone could, hence why my other comment started off with the words “more explicitly” to essentially unpack gjm’s remark.
More explicitly, there are a lot of things that humans can do easily that seem to be extremely difficult for AI (vision and language are the most obvious), and there are many things that humans have trouble with that we can easily make AI do a decent job. At some level, this shouldn’t be that surprising because a lot of the things humans find really easy are things we have millions of years of evolution optimizing those procedures.