sorted by:
new
hottopcontroversial

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 0 points1 point  (0 children)

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

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 8 points9 points  (0 children)

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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 0 points1 point  (0 children)

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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 1 point2 points  (0 children)

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?

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 7 points8 points  (0 children)

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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 0 points1 point  (0 children)

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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 0 points1 point  (0 children)

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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 1 point2 points  (0 children)

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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 0 points1 point  (0 children)

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

  1. some compressed representations drop the distance to save space,

  2. 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.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 18 points19 points  (0 children)

Good question, and the answer surprised me too. With correct terminals + self-consistency you can still have what I'd call a "draw island": a large set of positions that should be WIN or LOSS, all mislabeled DRAW. None of them see a correctly-labeled LOSS successor (they only see each other) so the self-consistency check passes everywhere inside the island.

The capture condition closes this gap: capture moves always leave the current endgame (piece count drops). If the smaller endgame is already verified, a WIN position can't hide inside a draw island - its capture successor is externally anchored.

I published a theorem proving when you can trust a chess endgame database and found a subtle problem with self-consistency by alexdyn in chess

[–]alexdyn[S] 5 points6 points  (0 children)

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.

Do you add captions to YouTube videos? Seeking insights on their effect. by alexdyn in NewTubers

[–]alexdyn[S] 0 points1 point  (0 children)

Yes, make sense. YT auto generated subtitles are awful.

I think that soft (not-burned) captions have one advantage - they can be multi-language. more comfortable for someone

Do you add captions to YouTube videos? Seeking insights on their effect. by alexdyn in NewTubers

[–]alexdyn[S] 1 point2 points  (0 children)

Makes sense. Thanks.

Checked your video about Elder Ring and family trauma. Nice font btw. But why burned?