Mind boggling machine learning results from AlphaZero

[PeroK]

Problem is, nobody knows how many positions humans consider, because humans cannot accurately report on both conscious and unconscious thought

To illustrate this point I remember a game when I used to play weekend chess tournaments. I was about 1800, so a decent player. I was losing to a slightly weaker opponent having blown a big advantage when, to my horror, I noticed my opponent had a checkmate in one! which, obviously he hadn't seen.

While he was thinking more and more people crowded round our board. I was praying they would all go away but my opponent never noticed. When he finally moved, not the check mate, a roar of laughter went up and I slumped back in my chair. Only then did my opponent notice the crowd!

So, what on Earth was he thinking? What moves was he looking at and why didn't he notice the mate in one?

Sometimes I think looking at the top players doesn't help understand human thought because they are so exceptional. Looking at what an average player does is perhaps more interesting.

 

[Fooality]

I keep wondering whether this technology would be applicable to solving mathematics problems, perhaps defining the game rules by some formal system. What I find hard to imagine is how to formulate the state of a partial proof in a form that can be the input of an artificial neural net.

Yeah, good question. I know mathematical proofs we're one of the first thing they tried to unleash computers on in the 50s, and they meet their first failures in making machines think. There's more to it than just formal logic it seems.

Thinking about Bridges of Königsberg problem solved by Euler. You have this question that seems to involve all this complexity, but you discard a lot of data to get down to the simplest representation, and in that context break down the notion of travel until the negative result is obvious, is proven. And it's proven to us because in that simple form we can understand it, we don't have the cognitive power to brute force it.

How does Euler's brain know to not think about the complete path, but rather just a single node (in his newly created graph theory) to find the solution for all complete paths? It's hard to imagine NN doing this without a priori knowledge that paths are composed of all the places visited, again real physical world knowledge.

 

[Hendrik Boom]

Yeah, good question. I know mathematical proofs we're one of the first thing they tried to unleash computers on in the 50s, and they meet their first failures in making machines think. There's more to it than just formal logic it seems.

Thinking about Bridges of Königsberg problem solved by Euler. You have this question that seems to involve all this complexity, but you discard a lot of data to get down to the simplest representation, and in that context break down the notion of travel until the negative result is obvious, is proven. And it's proven to us because in that simple form we can understand it, we don't have the cognitive power to brute force it.

How does Euler's brain know to not think about the complete path, but rather just a single node (in his newly created graph theory) to find the solution for all complete paths? It's hard to imagine NN doing this without a priori knowledge that paths are composed of all the places visited, again real physical world knowledge.

I'm hoping initially to be able to automate somewhat the choice of proof tactics in a proof assistant. Not have AI-generated insight.

 

[Fooality]

I'm hoping initially to be able to automate somewhat the choice of proof tactics in a proof assistant. Not have AI-generated insight.

Oh you're actually doing it? Cool good luck. If you can get the training data, I don't see why not.

 

[Hendrik Boom]

Oh you're actually doing it? Cool good luck. If you can get the training data, I don't see why not.

Sorry. I don't actually have the resources to do this. So I spend my time wondering how it might be done instead.

Training data? I thought of finding some analogue if having the machine play itself. But now that you point it out, I suppose one could use human interaction with a proof assistant as training data.