I published a theorem proving when you can trust a chess…
0 reactions
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.
#games
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.
#games
| 1,000 mlx | |
| 1 | |
| 0 |