提出验证残局表的分解定理,确保胜平负标记准确无误。
Capture-Quiet Decomposition: A Verification Theorem for Chess Endgame Tablebases
- 将棋局分为终局、吃子和静步三类,分层验证标签正确性。
- 在517个残局共超5000万位置上验证,结果与传统方法完全一致。
- 可防止虚假解(如全平局)通过自洽性伪装,适合验证系统设计者。
我们提出捕获-静步分解(CQD),一种用于验证国际象棋残局表胜平负(WDL)标记的结构定理。该定理将每个合法局面精确划分为三类——终局、吃子或静步,并证明:一个WDL标记是正确的当且仅当:(1) 终局局面标记正确;(2) 吃子局面与更少棋子数的已验证子模型一致;(3) 静步局面在同残局内满足回溯一致性。核心洞察在于,吃子局面将标记锚定于外部验证的子模型,打破仅靠自洽性即可生成平凡解(如全平局)的循环依赖。我们在全部35个三至四子残局(4200万位置)、110个五子残局和372个六子残局(总计517个残局)上对CQD进行了全面验证,分解验证器在每种情况下产生的违规数量均与完整回溯基线完全一致。
原文摘要 · Abstract (English)
We present the Capture-Quiet Decomposition (CQD), a structural theorem for verifying Win-Draw-Loss (WDL) labelings of chess endgame tablebases. The theorem decomposes every legal position into exactly one of three categories -- terminal, capture, or quiet -- and shows that a WDL labeling is correct if and only if: (1) terminal positions are labeled correctly, (2) capture positions are consistent with verified sub-models of smaller piece count, and (3) quiet positions satisfy retrograde consistency within the same endgame. The key insight is that capture positions anchor the labeling to externally verified sub-models, breaking the circularity that allows trivial fixpoints (such as the all-draw labeling) to satisfy self-consistency alone. We validate CQD exhaustively on all 35 three- and four-piece endgames (42 million positions), all 110 five-piece endgames, and all 372 six-piece endgames -- 517 endgames in total -- with the decomposed verifier producing identical violation counts to a full retrograde baseline in every case.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。