Verifiability of endgame tablebases

[hgm]

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

But of course in general mates don't take 545 moves. Whether forward search could find a mate in 545 depends on the number of men involved, and the size and quality of your hash table. Just like whether you are able to build an EGT by retrograde analysis depends on the number of men and the memory sizeof the machine.

[Sven]

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

But of course in general mates don't take 545 moves. Whether forward search could find a mate in 545 depends on the number of men involved, and the size and quality of your hash table. Just like whether you are able to build an EGT by retrograde analysis depends on the number of men and the memory sizeof the machine.

The OP was talking about mating sequences claimed by some EGT. There we typically have very deep mates. Mate in 545 was just the current example. "In general" you can forget about verifying a deep EGT mate using today's chess engines, no matter how strong your hardware and settings are. Even if the engine is able to find a mate in, say, 100 plies, you can't be sure whether this is actually the shortest path to mate due to heavy pruning stuff etc. which is the only way to get to that depth at all. So this is no "verification".

[hgm]

Well, it depends on the number of men. If that is low enough that the hash table can contain the entire table, and the table records two-sided bounds, the number of transposition cutoffs becomes so large that you can do it. But it is certainly a lot less efficient method than retrograde.

(In fact you don't need to be able to store the entire table, but just a winning line and the refutation trees sprouting from it, which for a given position might be much smaller.)

[syzygy]

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.

It is not very clear to me what you are allowed to do to verify the claim (probe the same tablebase?) and whether you trust what the tablebase returns.

Let's say you have access to the tablebase, but you don't trust it completely. You are given a position. You probe the tablebase and get mate-in-N. Now you want to know whether this is correct.

As already stated, you could run the position in a chess engine and see if it confirms the mate-in-N. If an engine confirms mate-in-N, then you can be reasonably sure that it is a mate in at most N moves (if the program is not buggy and you're not hit by unfortunate hash colissions). If an engine says mate-in-N that does normally not mean, however, that no shorter forced mate exists. The engine might have found the longer mate earlier and/or may somehow prune the shorter mate so it won't find it (or only much later).

If you have access to the tablebase, you can probe it to construct a "proof tree" for the mate. First determine the winning move (or one of the moves) that leads to the shortest mate. Play that winning move and play out all possible countermoves. For the resulting positions you probe again to find the best winning move. And so on. With a mate-in-545 the tree would grow extremely large (identifying transpositions to the same board positions could help a bit), but for shorter mates this is certainly doable. After at most N iterations all the branches of the tree should have ended in mate or the tablebase is wrong. Again, this does not prove that no shorter mate exists.

To prove that no shorter mate exists, you have to work the other way around: prove that the opponent can survive at least N-1 moves without getting mated. So now you have to construct a tree by playing out all moves of the winning side from the alleged "mate-in-N" position and then probe the tablebase by finding for each child position the "best" countermove (e.g. a winning or drawing one, or one that postpones the mate the longest). You continue this until you have constructed a tree of depth 2*N-1. If no branch ends in mate, you have the mathematical proof that the original position is at best a mate-in-N. If some of the branches do end in mate, the tablebase is corrupt.

The two proof trees together prove that the position is mate-in-N independent of the correctness of the tablebase. The tablebase was used only to construct the trees. If the tablebase is correct, the construction will have been successful.

This second part in principle could also be done by running an engine, but you would have to modify the engine a bit.

[syzygy]

You can construct the two proof trees as a single tree, basically by doing an alpha-beta search starting from the original position and using the tablebase to find the (or an) optimal first move.

Starting from the original position, the list of all selected optimal first moves will be the principal variation. The rest of the tree proves that each of these moves is in fact optimal (from the point of view of the side playing it).

[Sven]

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.

It is not very clear to me what you are allowed to do to verify the claim (probe the same tablebase?) and whether you trust what the tablebase returns.

Let's say you have access to the tablebase, but you don't trust it completely. You are given a position. You probe the tablebase and get mate-in-N. Now you want to know whether this is correct.

As already stated, you could run the position in a chess engine and see if it confirms the mate-in-N. If an engine confirms mate-in-N, then you can be reasonably sure that it is a mate in at most N moves (if the program is not buggy and you're not hit by unfortunate hash colissions). If an engine says mate-in-N that does normally not mean, however, that no shorter forced mate exists. The engine might have found the longer mate earlier and/or may somehow prune the shorter mate so it won't find it (or only much later).

If you have access to the tablebase, you can probe it to construct a "proof tree" for the mate. First determine the winning move (or one of the moves) that leads to the shortest mate. Play that winning move and play out all possible countermoves. For the resulting positions you probe again to find the best winning move. And so on. With a mate-in-545 the tree would grow extremely large (identifying transpositions to the same board positions could help a bit), but for shorter mates this is certainly doable. After at most N iterations all the branches of the tree should have ended in mate or the tablebase is wrong. Again, this does not prove that no shorter mate exists.

To prove that no shorter mate exists, you have to work the other way around: prove that the opponent can survive at least N-1 moves without getting mated. So now you have to construct a tree by playing out all moves of the winning side from the alleged "mate-in-N" position and then probe the tablebase by finding for each child position the "best" countermove (e.g. a winning or drawing one, or one that postpones the mate the longest). You continue this until you have constructed a tree of depth 2*N-1. If no branch ends in mate, you have the mathematical proof that the original position is at best a mate-in-N. If some of the branches do end in mate, the tablebase is corrupt.

The two proof trees together prove that the position is mate-in-N independent of the correctness of the tablebase. The tablebase was used only to construct the trees. If the tablebase is correct, the construction will have been successful.

This second part in principle could also be done by running an engine, but you would have to modify the engine a bit.

A proof tree can be used to verify a given mating sequence by probing a tablebase that you trust. You can't prove anything based on an incorrect, or at least "untrusted", tablebase. You may increase the likelihood that the given sequence is optimal by constructing a "proof tree" but I hope you agree that this is still no proof in a "formal" sense. Of course for a "formal" proof we would also need a proof that our move generator is correct but this is another topic ...

[syzygy]

A proof tree can be used to verify a given mating sequence by probing a tablebase that you trust. You can't prove anything based on an incorrect, or at least "untrusted", tablebase.

Certainly you can!

The resulting proof tree itself is the proof. If the tablebase is corrupt, then its construction might fail. But if it works, the proof tree itself gives you a recipe for reaching mate in at most N against any opposition.

The proof tree is the formal mathematical proof, not for the correctness of the tablebase as a whole, but for the correctnes of the statement "mate in at most N".

If you run a very simple alpha-beta search on a mate-in-N position (that takes account of distance to terminal node), you will after some time get the result "mate in N". An untrusted tablebase may be used as an oracle to determine at every node the first move to be searched. If the tablebase is correct, you will have perfect move ordering and a much faster search.

If you trust the tablebase, you only need to probe the position. If it says mate-in-N, then that can be trusted and you're done.

[hgm]

Indeed. Note that this is just a limited application of the general method for proving that the entire EGT is correct, limited to the positions you need to be correct to prove the given position: every mated-in-N must have all daughters mate-in-N or faster, and every mate-in-N must have a mated-in-(N-1) as its fastest daughter. (And the mated-in-0 positions must indeed be mates.)

I don't know about this particular mate in 545, but often the proof tree is not as big as it would seem, because deviations by the losing side just cause a faster path to the same position on the PV that leads to the mate. E.g. when you are driving the King towards the right corner in KBNK.

[syzygy]

I have actually considered the problem of possibly not entirely correct tablebases in the context of solving suicide/losing chess. I have generated all 6-piece tables (which are quite many!) but have made no attempt to verify their correctness other than convincing myself that the generator is correct (a complete verification would be very time consuming as the tables are heavily compressed with much easy-to-recompute information removed).

The main goal of this exercise is to show that suicide chess is a win for white essentially by running a proof-number search from the starting position which reaches into the tablebases. The proof-number search would generate a proof-tree, but only up to the TB positions as terminal nodes.

Now how could such a proof ever be trusted if we're not sure that the tablebases have no flipped bits? The answer was given above: we simply use the TBs to expand the TB-terminal positions of the proof tree into "real" terminal positions. Once that is done, the proof stands on its own and the reliability of the TBs becomes irrelevant.

(I have not actually been working much on the proof-number search part, though. And Mark Watkins is already very far in completing a proof, but if at some point he really gets stuck maybe my tables will be able to help.)

[Sven]

When constructing a proof tree, what would you do when encountering a mate-in-N position, after having checked that the EGT actually flags at least one successor as mated-in-(N-1) and all other successors as mated-in-(N-1) or longer: would you
a) check for all successors whether their EGT value is correct, or
b) check just the (first) one successor that you find being flagged as mated-in-(N-1)?

I assume you would have to do a) since in case of b) you might miss to find an EGT error if one of the unchecked successors has a wrong EGT value and the true value is a shorter mate. But doing a) would mean to expand all non-optimal move sequences, therefore considering also all kinds of repetitions or playing close to the 50-moves rule. How do you think this kind of examination would ever terminate?