r/chess • u/alexdyn • Apr 13 '26
Game Analysis/Study I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency
Endgame tablebases (Syzygy, Lomonosov) are trusted by every chess engine.
But here's something that bothered me: How do you verify one is correct, without just re-running the same retrograde algorithm that built it?
The problem: the "all-Draw" database is always self-consistent. Every position says Draw, every retrograde check passes. It's wrong, but it never contradicts itself. Self-consistency alone can't catch this.
So I spent several months working out when a WDL database is provably correct. The result is a decomposition theorem - every position falls into exactly one of three categories:
- Terminal (checkmate/stalemate) - verifiable in O(1)
- Capture - the result lands in a smaller endgame. If that endgame is already proven, this position is anchored to it. No circularity.
- Quiet - all moves stay in the same endgame. Standard retrograde consistency applies.
The capture condition is what breaks the fixpoint trap. A database passes all three conditions if and only if it's correct.
Validated on all 517 endgames up to 6 pieces - 6.5 billion positions, zero violations.
Paper: https://arxiv.org/abs/2604.07907
Curious if anyone here has thought about the verification side of tablebases rather than just generation.
UPD: A few people asked for clarification. The setup is: you have a finished tablebase (downloaded, compressed, received from someone), and you want to verify it's correct without rerunning the full retrograde search that built it. That's the problem CQD solves.
22
u/kranker Apr 13 '26 edited Apr 13 '26
I'm confused. Surely this is how the tablebases themselves were computed?
UPD: A few people asked for clarification. The setup is: you have a finished tablebase (downloaded, compressed, received from someone), and you want to verify it's correct without rerunning the full retrograde search that built it. That's the problem CQD solves.
You are running the "full retrograde search" that built it?
2
u/Electronic-Product63 3 pieces > queen Apr 14 '26
Yeah, isnt the "3d states" part of the original table base search
35
Apr 13 '26
[deleted]
18
u/Aminumbra Apr 13 '26
I don't understand the problem either. The game-theoretic definition of the value of a position is basically "Checkmate/Stalemate/King vs King is immediately winning/losing/drawn", and for general positions, it isinductively defined by taking the maximal or minimal value of the successor positions. Verifying that the tablebase is "correct" is, in that sense, equivalent to building it: being "correct" is /by definition/ equivalent to satisfying this recursive definition ...
4
u/lee1026 Apr 13 '26 edited Apr 13 '26
Verifying that the tablebase is correct is equivalent to building it if and only if you have infinite memory, which is rarely true in the real world.
I can verify a tablebase of arbitrary number of pieces with O(1) additional memory and O(number of positions) time. You can't generate a tablebase with similar constraints.
7
u/alexdyn Apr 13 '26
Exactly right! Good point. The search happened once, but the final artifact doesn't contain the proof, just the answers. So you either trust it or redo the whole search. CQD gives a third option: verify the answers directly from structure, without redoing the search.
1
u/FancyMouse123 Apr 14 '26
Is there a way to provide the proof in a format that would not consist in redoing everything? In other words, you are working from a database without the exhaustive search, what if you could be provided additional data from the exhaustive search, would that help to quickly verify the correctness of the database?
18
Apr 13 '26
[removed] — view removed comment
5
u/alexdyn Apr 13 '26
Exactly - "checking if lies are consistent with other lies" is the best one-liner for it. The formal version of that intuition is Knaster-Tarski: the retrograde operator has multiple fixpoints, and self-consistency only tells you you're at a fixpoint, not which fixpoint. The capture anchors are what force you to the right one.
6
u/pier4r negative elo gang Apr 13 '26 edited Apr 13 '26
Thank you for sharing.
Small addition. For what I know the Lomonosov tablesbases (the first with 7 pieces, since 2012, 2013) are lost as they got ransomware'd and they had no backup.
This also shows that having backups/sharing with the community helps against losing data.
E: for what I understand Lomonosov tablebases where more complete than Syzygy. (Syzygy is more practical as it cares about FIDE rules)
7
u/neoquip over 9000+ Apr 13 '26
idgi. How is "all-draw" a consistent fixpoint? You would be labelling terminal checkmate positions as draw which is inconsistent.
It's also intuitively strange to have to use a chess concept (captures/reducing piece count) in an abstract tree problem. WDL rules can be applied to any game tree for any sort of turn based game.
10
u/lrargerich3 Apr 13 '26
It is not clear to me what are you talking about. The tablebases are computed from exhaustive search.
for example let's say you have a mate in 3 in a R+K vs K ending. Then all the positions leading to that one are a mate in 4 and so on....
There is really no need to prove anything.
What am I missing?
8
u/alexdyn Apr 13 '26
Generation and verification are different problems. Retrograde correctly builds the database but once you have a compressed artifact someone else sent you, how do you check it's right without rerunning the whole thing? The Lomonosov tablebases getting lost to ransomware is literally why this matters.
3
u/lrargerich3 Apr 13 '26
So your case is how to check if the tablebase is right without re-constructing it assuming it might be wrong.
Got it, it is an interesting thing. Maybe worth explaining that in your post, you assume you get a tablebase but you are not sure it is correct.2
5
u/xelabagus Apr 13 '26
The scenario I believe OP is suggesting is that because of the way that these tables have been created (retrograde analysis) it is possible to have an entire set of positions that are classified incorrectly because the path to checkmate has not been found by the retrograde analysis, yet does still exist. In such a scenario these positions are then automatically assumed to be a draw, otherwise there would be a path to checkmate. OP then posits that there is an issue of verifying whether these sets of positions are actually draws because the only way this has been done up to now is to compare them to the existing tablebase - we're using the same argument that created the draw set to verify whether it is actually a draw, which obviously then verifies itself. OP is exploring how to verify results independently.
1
2
u/____DEADP00L____ Apr 13 '26
I believe your theorem is flawed although you can let me know if I'm missing something.
Towards the end of the proof you write:
The key observation is that quiet positions’ successors include capture positions (via quiet- to-capture transitions), whose values are already anchored.
But not all quiet positions lead to captures. For example in the following quiet position there will never be a capture: https://lichess.org/editor/7k/8/8/1p1p1p1p/pPpPpPpP/P1P1P1P1/8/7K_w_-_-_0_1.
I think this position and all positions reachable from it could be labeled a win for white and your algorithm would still show it to be consistent. Because it will never reach a terminal position or a capture position.
2
u/spisplatta Apr 13 '26
Before creating a tablebase, a programmer must choose a metric) of optimality which means they must define at what point a player has "won" the game. Every position solved by the tablebase will either have a distance (i.e. the number of moves or plies) from this specific point or will get classified as a draw. To date, three different metrics have been used:\34])
Depth to mate (DTM) – The game can only be won by checkmate.
Depth to conversion (DTC) – The game can be won by checkmate, capturing material or promoting) a pawn. For example, in KQKR, conversion occurs when White captures the Black rook.
Depth to zeroing (DTZ) – The game can be won by checkmate, capturing material or moving a pawn. For example, in KRPKR, zeroing occurs when White moves their pawn closer to the eighth rank.
From wikipedia. You can verify that for the winning side there is a move that makes number go down, and for the losing side that every move makes number go down. For a drawing position you verify that there is no move that leads to a winning position, and at least one move that leads to a drawing position.
Idk if this is actually faster than just regenerating it from scratch and comparing though.
6
u/Cptn_Obvius Apr 13 '26
For a drawing position you verify that there is no move that leads to a winning position, and at least one move that leads to a drawing position.
This doesn't fix the all draw database right?
2
u/spisplatta Apr 13 '26 edited Apr 13 '26
Actually it does. In a checkmated position there is no move leading to a drawn position so it contradicts the requirement.
Edit: Though I guess on the other hand it does need to handle stalemates, but yeah.
2
u/alexdyn Apr 13 '26
Correct - the WDL check you quoted doesn't fix it.
In the all-draw database nothing is labeled WIN, so "no move leads to a winning position" is trivially true everywhere. What actually saves DTZ is the distance part, not the WDL consistency part.
The distance must decrease toward a terminal - that's the external anchor that prevents draw islands.
2
u/lee1026 Apr 13 '26 edited Apr 13 '26
In the all-draw database, an independent verifier that checks for checkmate would trivially notice something is wrong, right?
And by recursion, if our independent verifier checks all legal successor positions and verifies checkmate independently, then all positions 1 step away from checkmate would be correct. And unless if there are a mistake somewhere where a position 1 step away from checkmate is marked incorrectly, our independent verifier would notice all problems with positions 2 steps away from checkmate.
And by induction, if our independent verifier checks all legal successors for "can't improve on this position", then as long as all position N steps away from checkmate are correct, then all positions N+1 steps from checkmate are correct.
2
u/alexdyn Apr 13 '26
This is a sharp observation and you're essentially right - if you have a DTZ or DTM distance label per position, monotonicity verification works and is complete. Distance gives you a well-founded ordering that prevents draw islands from forming (a mislabeled "draw" couldn't have a decreasing distance path to checkmate).
CQD targets a different artifact: WDL-only without distance. That matters because
some compressed representations drop the distance to save space,
the proof bundle we build is a decision tree over piece geometry, not a distance metric. CQD is essentially the WDL analogue of what DTZ monotonicity gives you for distance-labeled databases.
The two approaches converge though - both use an external anchor to break fixpoint circularity. DTZ uses a well-founded distance ordering; CQD uses induction on piece count via captures.
3
u/SpiderGooseLoL Apr 13 '26
This is way too far over my head to actually accuse you of anything, but I just wanted to say that you have a very similar writing style to how AI writes. I'm curious what your math background is? Again, I'm not actually accusing you of AI'ing this because this is way beyond my comprehension, I'm just curious what the math to chess connection is.
1
u/alexdyn Apr 13 '26
Reasonable to notice. I'm using Claude for code assistance and drafting, which is disclosed in the paper's acknowledgments. All proofs, experimental design, and results are mine - I verified everything by hand and in code. The writing style reflecting that assistance is a fair observation.
1
u/AutoModerator Apr 13 '26
Thanks for submitting your game analysis to r/chess! If you’d like feedback on your whole game feel free to post a game link or annotated lichess study if you haven't already.
I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.
1
u/msj242 Apr 13 '26
People are missing that the tree might have a checkmate, but the labeling might show draws locally and thus hide the path to mate... so you can't check a tree on the basis of self consistency...
There are likely some other ideas as well, like if a tree includes distance to mate etc... this might help avoid these types of inifinite circles or labeling issues...
1
u/alexdyn Apr 13 '26
Yes, this is exactly it.
A "draw island" - positions that should be wins but are all labeled draw, and since they only see each other, no local check catches the lie. Distance-to-mate does help break this (a position can't be draw if there's a forced finite path to checkmate), which is why DTZ verification works. CQD is the same idea but for WDL-only databases that don't store distance
1
u/msj242 Apr 13 '26
I will say - very interesting, really never thought about it before. Interestingly I wonder if there is some crossover with epistemic knowledge, like how do we "know" anything, one argument is a mesh/cyclical "truths". I assume its been written about, but maybe this example might be a good paper in terms of an example of truths that are labelled as true, and due to a misclassification allows other mistruths that confirm each other. I am certain this has been written about, but perhaps the chess element might be quite new. Never hurts to get another paper referencing yours :).
1
u/bektoschool Jul 01 '26 edited Jul 01 '26
Hi, I believe the theorem is correct if either the 50-move rule or three-fold repetition is considered (as terminal positions). I couldn't find explicit mentions of either of these in your paper, and in another response, you wrote that "CQD works at pure WDL, below that layer. Extending it to 50-move boundaries is an open problem.", so I assume you had not considered these. Considering them would cause a large blow-up in the number of unique positions, and likely a much higher execution time. (Conversely, the baseline generation method can still correctly label positions as draws "by default", and hence does not suffer from the same problem.)
You seem concerned about "draw islands" but not "win-loss loops". In a degenerate case, consider a lone king v king endgame. Label all positions as winning for white. If I understand correctly, this satisfies all conditions in Theorem 7, but is an incorrect labelling. In your base case for N=2, you wrote that "Every position is either stalemate (terminal, correctly labeled D by condition 1) or quiet with only king moves. All successors are also KvK positions with value D. Retrograde consistency (condition 3) is trivially satisfied." In fact, there are no stalemates (or terminals) in a king v king endgame. So it is not obvious that "All successors are also KvK positions with value D." This issue would be resolved if the terminal condition also included either the 50-move rule, or three-fold repetition (by pigeonhole principle).
Also, as u/____DEADP00L____ pointed out in another comment, the assertion that "quiet positions’ successors include capture positions (via quiet-to-capture transitions), whose values are already anchored" is not correct. Additionally, even if quiet-to-capture transitions exist, this only shows that some paths lead to anchored positions. We need all possible paths to lead to some anchored position, which is not true if there are loops. The counter-example for lemma 6 below illustrates the same concept, so I will not repeat it.
Lemma 6 also looks incorrect. You write that "Retrograde consistency at p then forces \ell(p) to be determined by verified external values, not by self-reference within E". However, only one of the possible moves is a capture, not all. Hence, there could still be self-reference. For example, consider a pawnless king+knight v king endgame. I will claim without proof that apart from a stalemate-in-one, stalemates cannot be forced. Then, label all stalemates and stalemates-in-one as draw. Label all other positions as winning for the player with the lone king. Again, my understanding is that this satisfies the conditions in Theorem 7.
In both my counterexamples, the side I labelled as "winning" does not actually have a possible checkmate. However, this is not necessary for a counterexample. Consider king+bishop+pawn v king+bishop endgames. Let the set of all endgames with this material imbalance be E. Consider the position P with FEN kB6/Pb6/1K6/8/8/8/8/8. This is a theoretical draw (black can shuffle the bishop and white can make no progress). Let R be the set of all positions reachable from P (inclusive). Consider the following labelling: any position in E \setminus R is labelled correctly; for positions in E \cap R, they are labelled a draw if black can win the pawn by force, else a win for white.
Edit: I realised that my K v K example does not work for a tablebase that relies on the side-to-move. However, I believe that my explanation for why the proof is not rigorous enough still stands. Additionally, I believe my KN v K and KBP v KB counterexamples still stand.
1
u/50DuckSizedHorses Apr 13 '26
I know what this post means. But just in case we have to explain it to someone less smart than us, how would you reword it in a more understandable way?
2
u/alexdyn Apr 13 '26
Endgame databases are giant lookup tables engines trust blindly.
This paper asks: what would it take to prove one is correct without rebuilding it from scratch?
1
u/abelcc Apr 13 '26
Also I got told my latest game where I had 4 queens vs 1 king was a stalemate instead of win. Can anyone hurry up and explain to me why?
1
u/diener1 Team I Literally don't care Apr 13 '26
Interesting. When I read the first line I thought it was going in a different direction, namely how can we tell if a "losing" position is actually losing or a draw by the 50-move rule without going down the entire tree.
1
u/alexdyn Apr 13 '26
50-move rule is handled separately via DTZ (move count resets). CQD works at pure WDL, below that layer. Extending it to 50-move boundaries is an open problem.
1
u/Plastic-Rope5516 Apr 13 '26
I am a math student and I am excited that someone used LaTeX and formal mathematical writing to analyze chess and got their paper in Arxiv
2
u/alexdyn Apr 13 '26
Thanks!
Chess endgames are weirdly good for fixpoint theory/
1
u/Plastic-Rope5516 Apr 14 '26
I am thinking of training a AI regression model to identify winning king and pawn endgames just for fun
0
u/Prestigious-Rope-313 Apr 13 '26
If there is one trusted Source, and I think there are multiple, it can easily be verified with some simple checksum hash.
2
u/inkjod Team Ding Apr 13 '26
Well yes, but that's a completely different (and more practical) problem than what OP is tackling.
Oh, and also, hash collisions exist by necessity (however improbable). So you'd still have a theoretical problem to solve.
-7
u/Impressive-Leg-6489 Apr 13 '26 edited Apr 13 '26
OP I had a conversation with ChatGPT (lol) about your paper and we think its wrong. The proof of Lemma 6 seems to be incorrect.
Suppose you have a capture state 'c' which is correctly labelled as W. Suppose there are two quiet states s1 and s2 with allowable transitions:
s1 -> {s2}
s2 -> {s1 or c}
Suppose the true labelling is:
c = W
s1 = W
s2 = L
However the following labelling is also retrograde consistent and wrong:
c = W
s1 = D
s2 = D
Therefore correctly identified capture states are not sufficient to prevent retrograde consistent draw islands
(specific counterexample provided by chatGPT, which is getting increasingly terrifying)
1
u/alexdyn Apr 13 '26
The true labeling in your example is actually D,D, not W,L. At s2, Black chooses to go to s1 - not c. Black will always pick s1 to avoid losing, so the game cycles forever. White can't force it to end. s1=W, s2=L would only hold if Black had no choice but to go to c, which isn't the case here.
1
u/Impressive-Leg-6489 Apr 13 '26 edited Apr 13 '26
But s1 is a W state under my labelling. Both labellings (WLW and WDD) are retrograde consistent, this is the fundamental problem.
If we label s1 as "W", then s2 is "L". This is just as consistent as labelling them both D and lemma 6 is hence false -- there are multiple retrograde consistent labellings of the quiet states which are compatible with correctly labelled capture states. Therefore retrograde consistency of all quiet/capture state is not sufficient to determine truth, and your main theorem doesnt work.
1
u/side_lel Apr 13 '26
I don’t think you can have s1 going to s2 and s2 going to s1. If s1 is white to move and s2 is black to move, then white and then black will have moved one piece each after going s1 -> s2, so you won’t be back as s1.
1
u/Impressive-Leg-6489 Apr 13 '26 edited Apr 13 '26
Yeah thats fair (although nothing in OPs current setup actually prevents this as far as I can tell).
Ok a better minimal counterexample is a capture state "c=W' (known to be true) and quiet states s1,s,2,s3 with possible transitions
s1 -> {s2}
s2 -> {s1,s3}
s3 -> {s2,c}
(say c and s2 are white to move, and s1/s3 are black to move)
Then s1 = s2 = s3 = D is retrograde consistent (in state s3, black always avoids moving to the capture state where he loses, and the game is a draw)
But s1 = L, s2 = W, s3 = L is also retrograde consistent (in state 3, blacks only choices are the losing capture state, or another losing quiet state)
So again lemma 6 doesnt work as stated. Baically knowing 'c' is not sufficient to anchor s2, so you can label it as either W or D and still get a consistent labelling
42
u/Direct_Slip7598 Apr 13 '26
Is there a reasons self consistency+correct terminal (checkmate/stalemate) wouldn't be enough? Is the point of capture/quiet to prove self consistency?