Solving Chess Kickstarter

[hgm]

Note that it is not Intel that determines the progress of semiconductor technology, other than through being customers that contribute to the demand. They are dependent on what wafer steppers they can buy. If there aren't any 10-nm machines for sale, there isn't anything they can do about it.

[bob]

I think clearly less than 1% of the positions are reachable assuming perfect play by one side.

It is far and far less than 1%! But don't you realise that "all positions" or "1% of all positons" makes no practical difference at all, since both numbers are way way way beyond what is possible?

With minimax you'd have to search say 30^120 positions.
With alpha-beta AND always selecting the best move first it is "just" in the order of 30^60 positions.
The difference is immense.
Still, 30^60 is way too much, and most of those 60-move lines would still need considerable effort to "solve". And transpositions aren't going to help too much here, as there really aren't many transpositions in chess that bring unrelated lines back together. Not that you could have a transposition table that could store all those positions... (and just imagine the massive graph history interaction problems that would arise when trying to prove chess a draw).

1.e4 Nf6 2.Qh5 is losing for white and I feel 100% sure about it.
No need to analyze to be sure that 2...Nxh5 is a winning for black.

You are not talking about solving chess here.

But anyway, if you're talking about proving that white can win or at least draw, you can indeed alpha-beta prune 2.Qh5, and this is accounted for in the 30^60 number.

If you want to prove chess is a draw, you can probably alpha-beta prune 1...Nf6. Again, this is accounted for in the 30^60 number. But here you can already make a mistake. Maybe 1...e5 or so turns out to be losing and then you have to do another 30^60 tree for 1...Nf6 or some other move. The 30^60 assumes you can just pick a "best" move in each node, whch in practice is again completely impossible. So 30^60 is an unreachable lower bound.

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

[syzygy]

1.e4 Nf6 2.Qh5 is losing for white and I feel 100% sure about it.
No need to analyze to be sure that 2...Nxh5 is a winning for black.

You are not talking about solving chess here.

But anyway, if you're talking about proving that white can win or at least draw, you can indeed alpha-beta prune 2.Qh5, and this is accounted for in the 30^60 number.

If you want to prove chess is a draw, you can probably alpha-beta prune 1...Nf6. Again, this is accounted for in the 30^60 number. But here you can already make a mistake. Maybe 1...e5 or so turns out to be losing and then you have to do another 30^60 tree for 1...Nf6 or some other move. The 30^60 assumes you can just pick a "best" move in each node, whch in practice is again completely impossible. So 30^60 is an unreachable lower bound.

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

Note: if you're talking about proving that white can win or at least draw

The only thing that needs to be CERTAIN is the correctness of an eventual proof. There is no need to exhaustively try all of white moves.

Should I ever attempt to prove that white has at least a draw and fail in this attempt without considering 2.Qh5, then I will happily give up saying "I failed in my attempt to prove that white has at least a draw".

Obviously this would not allow to draw the conclusion that white is lost, but I was not talking about attempting to prove that white is lost in the opening position.

The point was and is that even if the prover program could select white's very best move in every position, a very low estimate for the size of the verification tree would still be 30^60 which is simply infeasibly big.

[bob]

1.e4 Nf6 2.Qh5 is losing for white and I feel 100% sure about it.
No need to analyze to be sure that 2...Nxh5 is a winning for black.

You are not talking about solving chess here.

But anyway, if you're talking about proving that white can win or at least draw, you can indeed alpha-beta prune 2.Qh5, and this is accounted for in the 30^60 number.

If you want to prove chess is a draw, you can probably alpha-beta prune 1...Nf6. Again, this is accounted for in the 30^60 number. But here you can already make a mistake. Maybe 1...e5 or so turns out to be losing and then you have to do another 30^60 tree for 1...Nf6 or some other move. The 30^60 assumes you can just pick a "best" move in each node, whch in practice is again completely impossible. So 30^60 is an unreachable lower bound.

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

Note: if you're talking about proving that white can win or at least draw

The only thing that needs to be CERTAIN is the correctness of an eventual proof. There is no need to exhaustively try all of white moves.

Should I ever attempt to prove that white has at least a draw and fail in this attempt without considering 2.Qh5, then I will happily give up saying "I failed in my attempt to prove that white has at least a draw".

Obviously this would not allow to draw the conclusion that white is lost, but I was not talking about attempting to prove that white is lost in the opening position.

The point was and is that even if the prover program could select white's very best move in every position, a very low estimate for the size of the verification tree would still be 30^60 which is simply infeasibly big.

You may or many not have to exhaustively try all white moves. What if the first N lead to a draw at best, and one remains (Qh5 perhaps). That has to be searched, or this is not a proof of anything other than "white has at least a draw." I'd personally want to know if white has a win.

You could make that same "I failed to ..." without trying a single move, obviously. Not very informative or useful.

[mvk]

I'm announcing a kickstarter project to jump over the moon. I need $2000 for the first step: selecting the color of the required trampoline. People have tried without trampoline and failed, therefore I believe that a trampoline is needed.

I'm happy to announce that my kickstarter project has gained a lot of support shortly after announcing it last month. Well, with one modification: the aim is to reach the ISS by 2020. Keep donating!

[duncan]

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

would it be the same with white opening position without a queen. that you cannot be CERTAIN white cannot win. ?

[bob]

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

would it be the same with white opening position without a queen. that you cannot be CERTAIN white cannot win. ?

Yes. Until it is proven with an exhaustive search.

[mvk]

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

would it be the same with white opening position without a queen. that you cannot be CERTAIN white cannot win. ?

Yes. Until it is proven with an exhaustive search.

Why would you settle with that, a single run? Hardware glitches and programming errors will be easily overlooked, and cast a nagging doubt on the correctness of the result. At least mathematicians would (or should) ask for two exhaustive searches, each independently implemented and executed. Or better yet, twice executed with the same configuration, but accompanied with mathemathical proofs of program, OS and CPU correctness.

Lacking that, the general chess population will settle centuries earlier with a heuristic answer, one of the type coined by Chessbase here in their famous April Fool's joke on this topic:

FF: So this means that the result is not 100% certain, it is just a hypothesis.

VR: That is technically correct, similar to the assertion that a position where one side is more than two pieces down, without any compensation, is considered lost, even if you cannot calculate it to a forced mate against any defence. Sure, there theoretically might be a way to save the game, but if Rybka is displaying +5.12 or more the outcome is 99.99999999% secure. That is approximately the confidence number we give to our King's Gambit results: 99.99999999%. It might be that there is a flaw somewhere, but if there is it will not be discovered in the course of this universe – that would require more computational power than could ever be provided. And of course it is possible, and in fact very, very likely, that there is no flaw.

This shows that in recreational computing such as computer chess, a heuristic answer will suffice: When the proof level is in somewhere in these regions, nobody will bother with an exhaustive search anymore but move on.

[bob]

Are you guys CERTAIN that after Nxh5 white can't win? Got a proof tree to support that? There are LOTS of queen sacs that do win, so how can one just dismiss this one outright? Certainly not in any sort of theoretically sound way, other than searching to a loss.

would it be the same with white opening position without a queen. that you cannot be CERTAIN white cannot win. ?

Yes. Until it is proven with an exhaustive search.

Why would you settle with that, a single run? Hardware glitches and programming errors will be easily overlooked, and cast a nagging doubt on the correctness of the result. At least mathematicians would (or should) ask for two exhaustive searches, each independently implemented and executed. Or better yet, twice executed with the same configuration, but accompanied with mathemathical proofs of program, OS and CPU correctness.

Lacking that, the general chess population will settle centuries earlier with a heuristic answer, one of the type coined by Chessbase here in their famous April Fool's joke on this topic:

FF: So this means that the result is not 100% certain, it is just a hypothesis.

VR: That is technically correct, similar to the assertion that a position where one side is more than two pieces down, without any compensation, is considered lost, even if you cannot calculate it to a forced mate against any defence. Sure, there theoretically might be a way to save the game, but if Rybka is displaying +5.12 or more the outcome is 99.99999999% secure. That is approximately the confidence number we give to our King's Gambit results: 99.99999999%. It might be that there is a flaw somewhere, but if there is it will not be discovered in the course of this universe – that would require more computational power than could ever be provided. And of course it is possible, and in fact very, very likely, that there is no flaw.

This shows that in recreational computing such as computer chess, a heuristic answer will suffice: When the proof level is in somewhere in these regions, nobody will bother with an exhaustive search anymore but move on.

The keyword here was "proof". "proof" doesn't mean 99.9% certain. it means 100.000% Schaeffer didn't prove anything about checkers heuristically, he searched from front to back and back to front to prove beyond any doubt at all what happens.

I remember some "heuristic ideas" back in the 70's that Ken Thompson blew out of the water with his KQKR endgame database. One "well-known" rule given by many GM players was "rook has to stay close to the king." False of course. As an exhaustive search/proof shows.

[mvk]

The keyword here was "proof". "proof" doesn't mean 99.9% certain. it means 100.000%

What you refer to is generally called a "mathematical proof".

Second, 99.9% is too low indeed (and so is 100.000% for that matter), and that level is not what we're talking about. The heuristic failures you refer to don't have the confidence levels referred to either, so we can dismiss those example on those grounds.