Verifiability of endgame tablebases

[hgm]

It is just like a normal search, where you use the best move indicated by the EGT as hash move (and never allow hash cutoffs). Wrong hash moves would never corrupt the search result, but just slow it down. For a correct EGT the first move would be cut move 100% of the time. With a faulty EGT the move suggested by the EGT might in reality not cause a cutoff, so that you would have to search later moves before you find the cut move.

[Sven]

It is just like a normal search, where you use the best move indicated by the EGT as hash move (and never allow hash cutoffs). Wrong hash moves would never corrupt the search result, but just slow it down. For a correct EGT the first move would be cut move 100% of the time. With a faulty EGT the move suggested by the EGT might in reality not cause a cutoff, so that you would have to search later moves before you find the cut move.

I think you did not consider the case that I described. Let's take an example position:
[D]8/8/5K2/8/7k/8/8/6Q1 w - - 0 1
This is mate in 2 if White plays Qg2, all other moves are mate in 3 or worse from white viewpoint. Now let's assume the EGT has two errors: it flags the diagram position as "mate in 3" and the position after 1.Qg2 as "mated in 3", for unknown reasons. (These are in fact two independent errors which are also inconsistent to each other!) How would you find that problem by constructing a proof tree, where the claim (based on the erroneous EGT) is that the diagram position is a mate in 3, with a PV that definitely does *not* start with the optimal move 1.Qg2 since the EGT says that other moves are better than it?

If you only check the best move indicated by EGT you will check any of the four king moves Kg6, Ke6, Kf5, Ke5 whose successors are all flagged correctly as "mated in 2". So based on the part of EGT information that you access it can happen that you "confirm" the (wrong) mate in 3. It is certainly possible that you will not find the EGT inconsistency since maybe no part of your proof tree covers any of the two positions having a wrong EGT value. (If this last assumption fails in my concrete example then it will certainly be possible to construct better examples where it works.)

It would be really surprising if proving the correctness of a claim that is based on unreliable data would be possible by directly using that data. You may be able to construct a real proof in some cases, and even in my (constructed) example above you may argue that it were impossible for your proof tree not to visit any of the problematic positions. But I hightly doubt that you can be successful with that in the general case.

[syzygy]

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 just build the tree. I don't have to verify the correctness of the tablebase.

So I do b).

If the position is mated-in-n, then I don't probe the tablebase at all, but I add to the corresponding node in the tree all the successor positions as children. These are all the countermoves by the losing side. Those positions are all supposed to be mate-in-n (or better). I will check them one by one (recursively) and again do b) on each of them.

With this tree, I can mate you in n or better if you play the losing side. When it's my move, the tree will give me one move and I will play that move.

[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 just build the tree. I don't have to verify the correctness of the tablebase.

So I do b).

If the position is mated-in-n, then I don't probe the tablebase at all, but I add to the corresponding node in the tree all the successor positions as children. These are all the countermoves by the losing side. Those positions are all supposed to be mate-in-n (or better). I will check them one by one (recursively) and again do b) on each of them.

With this tree, I can mate you in n or better if you play the losing side. When it's my move, the tree will give me one move and I will play that move.

So would you say that by doing b) you would build a valid proof tree in case of my example position of my previous post (KQK)?

[hgm]

Well, it doesn't seem there are any moves that are suggested to be better than mate in 3 by the EGT, but suppose for argument's sake that based on the disinfo you started picking Kf5 as the start of the PV (1. Kf5 Kh3 2. Kf4 Kh4 3. Qg4#) Then the proof tree would start verifying that every alterative white move sequence can be refuted by black to a slower mate. In the root it would try every move (it is a PV node), and amongst those it would find 1. Qg2. From the position that leads to, it would try the black move that the EGT says is best for black. That is 1... Kh5, as all other black moves lead to King captures, which are likely registered in the EGT as mated-in-0, while after 1. Qg2 Kh5 it is mate-in-1. From there it tries all white move, amongst which 2. Qg5#. From the position after that, it would try all black moves, and all lead to mate-in-0. It would verify that black's King can indeed be captured in such positions. So after trying all black moves, it would conclude that the position after 2. Qg5# is a mated-in-0. This makes the position after 1... Kh5 a mate-in-1-or-faster. So 1... Kh5 was (surprisingly) not enough to refute 1. Qg2. So for lack of a beta cutoff it would now also have to search alternatives to 1... Kh5, to see if these postpone the mate longer. None of those is any good, of course, as they are all illegal. So the position after 1. Qg2 is eventually scored as a mated-in-1. Which makes the start position a mate-in-2-or-less, contradicting the value of the EGT.

[Joan Charmant]

If I understand correctly Ronald de Man approach doesn't rely on the tablebase data at all, which feels better as it is deemed unreliable in the first place.

But if I'm not mistaken this would amount to traverse all the directed graph rooted at the start position… Which lead to another question I've had: would such a graph contain all the legal positions or only a subset of them? (Would we be rebuilding the entire tablebase in the process?)

Basically wondering if all legal positions in an endgame are connected together, in the sense that they can be reached from one another, or if there are islands of positions that can't be reached from other islands. (Limiting to pieces-only endgames since in the presence of pawns it's obvious that some positions can't be reached from others)

[Sven]

Oops, seems I accidentally hit 'Edit' where I thought I hit 'Reply', so I unwittingly destroyed Sven's post. Sorry about that.
H.G.

[syzygy]

So would you say that by doing b) you would build a valid proof tree in case of my example position of my previous post (KQK)?

If the tablebase has an error and I not really searching but only using the moves that the tablebase gives me, then the construction of the proof tree will fail. And I will know that, because not all branches will end in mate-in-2 or less.

Such a failed construction does not prove that the mate-in-2 is wrong (i.e. it does not prove that the position is a mate-in-3 or worse). It proves nothing, except that the tablebase is not reliable.

But if the construction does result in a proof tree, then that is a formally correct proof independent of whether the tablebase has errors or not.

[Sven]

So would you say that by doing b) you would build a valid proof tree in case of my example position of my previous post (KQK)?

If the tablebase has an error and I not really searching but only using the moves that the tablebase gives me, then the construction of the proof tree will fail. And I will know that, because not all branches will end in mate-in-2 or less.

Such a failed construction does not prove that the mate-in-2 is wrong (i.e. it does not prove that the position is a mate-in-3 or worse). It proves nothing, except that the tablebase is not reliable.

But if the construction does result in a proof tree, then that is a formally correct proof independent of whether the tablebase has errors or not.

In my example the proof tree construction based on the faulty EGT would not fail, that was my point. The claim of a mate in 3 would be "confirmed" although it is wrong.

With method a) (see HGM's post in the parallel subthread and my reply) the EGT fault would be detected but I think the effort for a) would be extraneous.

[syzygy]

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.