Verifiability of endgame tablebases

[Sven]

The claim of a mate in 3 would be "confirmed" although it is wrong.

Ok, but I had already written that the proof tree for proving "mate in at most N" will not work for proving that the position is not mate in less than N. ("Again, this does not prove that no shorter mate exists.")

For that, you need to work the other way around. Find for every move by the winning side one countermove that sufficiently delays the mate (or even draws or wins the game). Same principle.

You can also do both at once, very much like how a principal variation search works. The PV will be what joins the two trees.

If I have that EGT which is faulty as described by me above, but I don't know it in advance, I read the claim that the given position is "mate in 3" while in reality it is "mate in 2". So the first proof tree is built to prove the "mate in at most 3" and it does not fail. If I understand you correctly the second proof tree would be built in order to prove that none of the other moves for the winning side results in a faster mate, right? So you try all white moves, including 1.Qg2. The latter will result in a mate in 2 so we are done, EGT fault detected. But the algorithm implies to also check all other non-optimal moves which is a lot of work.

I think I now understand how the proof tree building works from your viewpoint. How do you handle the effort resulting from trying all non-optimal moves for the winning side?

[syzygy]

If I understand you correctly the second proof tree would be built in order to prove that none of the other moves for the winning side results in a faster mate, right?

The second proof tree is built in order to prove that the winning side cannot force a faster mate than mate in 3. This is equivalent to saying that the losing side has a forced way of still being alive after 2 moves. How the losing side should play is what you learn by probing the TB.

I think I now understand how the proof tree building works from your viewpoint. How do you handle the effort resulting from trying all non-optimal moves for the winning side?

For the first tree you have to look at all moves by the losing side and at only one move per position by the winning side. So about d^(N/2) nodes where N is the number of ply.

For the second tree you have to look at all moves by the winning side and at only one move per position by the losing side. So again about d^(N/2) nodes.

If you verify this carefully, you will probably get that the exponent N/2 is once rounded up and once rounded down and that you can subtract 1 somehere. Adding the two together gets you the size of the minimal alpha-beta tree:
http://www-public.tem-tsp.eu/~gibson/Te ... oore75.pdf
See page 14.

Interestingly, Knuth explains that the size of the minimal tree is d^(N/2) (the exponent either rounded up or down) if the value of the game (= root position) is +INF or -INF. Of course when we are distinguishing "mate-in-2" from "mate-in-3", we are not in a +INF or -INF situation. But if you're only interested in the position being won or not, then you only need one proof tree. Same if you're only interested in proving "score at least v" instead of "score equals v".

[Sven]

Ok, that sounds reasonable for me, thank you for explaining. So my distinction into methods a) and b) was not perfectly applicable since for both proof trees we can be selective for one side and must be exhaustive for the other, just as in a regular mate search. Initially I thought that we would need to build a tree by being exhaustive for both sides in order to detect a possible EGT inconsistency.