Verifiability of endgame tablebases

[Joan Charmant]

Hi,

Let's imagine that someone has computed a specific endgame tablebase and makes a claim regarding a position with a forced mate in M moves. (For example the mate in 545 in 7-man KRBN-KQN).

We are given the starting position.

- Is there any way to independently verify the claim without having to access or rely on the endgame tablebase itself? (and without generating a new one).
- Is there any way to verify the claim with only partial access to the tablebase? (or by only building a partial one?)

Finding counter examples to the claim, White could have mated more quickly (maybe ending in a different mating position), or Black could have delayed the mate longer, seems very difficult without having access to the entire set of positions.

[Sven]

I would say: no, you always need some reference tablebase. You can easily verify trivial things like legality, checkmate, or forced mate in few plies with a normal chess engine. But as soon as it comes to very long mating sequences where the optimal distance to mate can't be found by a normal mate search of a chess engine you need to apply "tablebase algorithms" for verification. As far as I know most people writing a tablebase generator also write a verification tool to check their own TB. But if you aim at an independent verification, therefore neither trusting the original TB nor its (possible existing) verification tool, then a reference TB would be needed.

I don't know what you mean by "only partial access to the tablebase" so I can't answer that part.

[Joan Charmant]

I meant a tablebase where only some of the positions have associated information.

By verification tool do you mean something that would take each position, play each legal move forward and verify that the resulting position is either at the same distance or one ply removed from the mate in either direction but never two plies closer or further away? (And maybe similarly for all legal unmoves)

[Sven]

I meant a tablebase where only some of the positions have associated information.

For instance, if this "partial TB" would contain complete information for all successors of those positions occurring on the given line then you could verify the claim.

By verification tool do you mean something that would take each position, play each legal move forward and verify that the resulting position is either at the same distance or one ply removed from the mate in either direction but never two plies closer or further away? (And maybe similarly for all legal unmoves)

I don't know how exactly a TB verification tool would be written most efficiently. But yes, something in that direction.

- A position is won in N plies (optimal DTM, ignoring repetitions and 50-moves rule here) if there is one legal move that leads to a position being lost for the opponent in N-1 plies, and none of the other legal moves leads to a position being lost for the opponent in N-3 plies or less.

- A position is lost in N plies if there is one legal move leading to a position that is won for the opponent in N-1 plies and all other legal moves lead to a position that is won for the opponent in at most N-1 plies.

- And the obvious stuff for N=0 (checkmated) and draw.

There may be different algorithms to verify these properties for all positions in a TB. Running the verification will certainly take some time, though.

[hgm]

The nomal way to verify EGT is to check that every lost-in-N position has only legal moves to won-in-N or better positions, and that every won-in-N position has at least one move to a lost-in-(N-1) position. And that the lost-in-0 positions are indeed checkmates, and that there are no checkmates amongst the undecided positions.

You can directly verify an individual won position by having an engine search on it until it finds the mate.

[Joan Charmant]

You can directly verify an individual won position by having an engine search on it until it finds the mate.

But if the engine plays sub-optimal move for the loosing color it will flag the position thinking that it found a shorter mate?

[hgm]

Engines are not supposed to play sub-optimal moves. The PV is defined as the sequence of moves where each side plays all their best moves, and the reported score (distance to mate) is based on that PV.

[Joan Charmant]

Yes of course, but I was thinking that maybe during the course of the 545 moves mate, there might be points where Black have several options that look similarly good if the engine is only looking at a depth of say, 128, but it later turns out that one option was the only way to stay on the longest mate route.

I don't know if that's the case, or if there are many short variations of equal length that actually end back up in the main sequence.

[Sven]

Engines are not supposed to play sub-optimal moves. The PV is defined as the sequence of moves where each side plays all their best moves, and the reported score (distance to mate) is based on that PV.

Which in general won't work, unfortunately, for a mate in 545 ...

[hgm]

Engines judge moves only by the evaluation at the leaves. Of course you must search deep enough to make sure you can see every faster mate than the one reported. But if a mate is reported it means that every possible combination of moves has been searched, and be found to be answerable by the winning side with a move that forced mate. Even if there was only a single sequence of moves against which mate could not be forced, the root would not get a mate score. In particular, the search cannot have failed to consider any moves of the losing side. It could have cut off some moves of the winning side, which would force the mate faster. But this would report a DTM larger than the true one. Never smaller.