数理

数理：大局将棋の数学

形式モデル、エンジンで計算した正確な数、そして Lean 4 による機械検証された形式化へのロードマップ。

要旨 · 1 形式モデル · 2 正確な数 · 3 状態空間 · 4 ゲーム木 · 5 移動力 · 6 階級の代数 · 7 対称性 · 8 計算量 · 9 Lean · 10 AIと解決 · 11 未解決問題 · 参考文献

草稿です。V を付けた数値はすべてゲーム自身のルールエンジンで計算したもので、 godot --headless --path . -s tests/math_stats.gd で再現できます。P は本ページで短く証明した命題、 C は文献からの引用、O は未解決または予想、L は Lean 4 で機械検証する予定の主張です。 Lean による形式化はまだ書かれていません。以下のコード片は、証明するつもりの主張であって、コンパイル済みの定理ではありません。

要旨

大局将棋は知られている中で最大の将棋で、\(36\times 36\) の盤に片側402枚、301種の駒が並びます。駒の動きには、無制限の走り、跳び、二歩動く「エリアムーブ」、 90°曲がる「鉤行」、複数の駒を一度に取る「範囲取り」が含まれます。本ページでは、局面と合法手の形式モデル、初期局面からの正確な数 （初手の合法手は \(97\)、3手後の局面は \(1{,}426{,}099\)）、状態空間の上界（\(<10^{3604}\)）、ランダムな対局で測った分岐数（\(\approx 320.6\)）、 走り駒の移動力の閉じた式、範囲取りの階級の代数を与えます。続いて、Lean 4 で形式化する予定の定理を述べ、AI を強くしてゲームを解けるところまで解くための取り組みを説明し、未解決問題を挙げます。

1. 形式モデル

1.1 盤・手番・駒

定義1（盤）。 \(N=36\) とする。盤は \(B=\{0,\dots,N-1\}^2\) であり、\(|B|=N^2=1296\)。升は \(p=(x,y)\)。手番は \(\mathsf B\)（先手、先に指す）と \(\mathsf W\)（後手）で、 \(\bar{\mathsf B}=\mathsf W\)、\(\bar{\mathsf W}=\mathsf B\) とする。先手は \(y\) が増える向きに、後手は減る向きに進む。
定義2（駒の種類）。 有限集合 \(K\) を駒の種類とし、階級 \(\rho:K\to\mathbb N\cup\{\infty\}\) と王類の集合 \(R\subseteq K\)（\(k\in R\) なら \(\rho(k)=\infty\)）を与える。 種類 \(k\) は成り \(\mathrm{pr}(k)\in K\cup\{\bot\}\) をもつことがある。データでは \(|K|=301\) V で、そのうち 209 種が初期配置に現れ、92 種は成りでのみ現れる。 王類は王と太子である。
定義3（局面）。 局面は組 \(s=(\pi,t)\) であり、\(\pi:B\to\{\varnothing\}\cup(K\times\{\mathsf B,\mathsf W\})\)、\(t\) は手番である。局面全体の集合を \(\mathcal S\) と書く。 初期局面 \(s_0\) では、各側の402枚を自陣に近い12段に置き、両軍の間に空きの段が12ある。各軍の1つの段には6枚、他の11段にはそれぞれ36枚が並ぶ（\(6+11\cdot 36=402\)）V。 初期配置での種類の個数は、1種が36枚（歩）、1種が4枚、155 種が2枚、52 種が1枚である（\(36+4+2\cdot 155+52=402\)）V。
00121224243535筋 x段 y先手（先に指す）後手空きの段 12歩（36枚）
図1. 初期局面（ゲームデータの配置表から描画）。先手（黒）は 0–11 段、後手（赤）は 24–35 段を埋め、180°回転した配置になる。薄い色の升は各側の歩36枚。両軍の間には12段の空きがある。

1.2 集合値関数としての動き

手番側と相手側の駒がある升の集合を \(\mathrm{Own}_t(\pi)\)、\(\mathrm{Opp}_t(\pi)\) と書き、方向ベクトルは動かす側に合わせて向ける（先手は \(d\mapsto d\)、後手は \(d\mapsto -d\)）。 動きは有限の経路 \(p=q_0\to q_1\to\cdots\to q_m\) と取られる升の集合 \(C\) の組である。各駒種の動きの規則は、次の要素の有限和集合である。

走り \(\mathrm{Sl}(d,\ell)\)、\(d\in\mathbb Z^2\)、\(\ell\in\{1,\dots,N-1\}\cup\{\infty\}\)： \(\{\,p+jd\ :\ 1\le j\le \ell,\ p+id\in B\ \forall i\le j,\ \pi(p+id)=\varnothing\ \forall i<j,\ p+jd\notin\mathrm{Own}_t\,\}\)。\(p+jd\) が \(\mathrm{Opp}_t\) にあればそれを取る。 （\(\ell=1\) は歩み、\(\ell=\infty\) は走り駒。）
跳び \(\mathrm{Lp}(v)\)：盤上にあり \(\mathrm{Own}_t\) にない単一の升 \(p+v\)。途中の升は無視する。
跳び越え走り \(\mathrm{JS}(d,s,\ell)\)：方向 \(d\) の最初の \(s\) 升を（何があっても）飛び越え、その先に着地するか、最大 \(\ell\) 升まで走る。走りと同様に最初の駒で止まる。
鉤行 \(\mathrm{Hk}(d)\)：\(d\) に沿って走り、途中の空き升で一度だけ90°曲がって、新しい方向へ走り続けてもよい。
エリアムーブ（獅子の仲間）：一手に最大2歩、8方向のどれにも進める。各歩で駒を取ってよく、2歩は一直線でなくてもよい。さらに、距離2の升への跳び、動かずに隣の駒を取ること、パスができる。動きは中間の升 \(q_1\) を記録する。
範囲取り \(\mathrm{RC}(d,r)\)、\(r\in\mathbb N\)：第6節を参照。

局面の合法手の集合 \(\mathrm{Mv}(s)\) は、手番側の各駒の各要素の動きの和集合である。王手の規則はなく、生成された動きがそのまま合法手である。 相手の王類をすべて取った側が勝つ。成りは規則のパラメータで、敵陣の奥11段に入ったとき（既定）、最初に取ったとき、成りなしから選ぶ。

実装では動きは三つ組 \((\text{from},\text{to},\text{via})\) である。\(\text{via}\) が異なる動きは別の動きとして数えるため、以下の数は (from,to) の組の数を上回る。

走り Sl(d, ∞)跳び Lp(v)跳び越え走り JS(d, 2, ∞)鉤行 Hk(d)↰エリアムーブ（獅子）12範囲取り RC(d, r)31215移動可取られる動く駒敵障害・味方
図2. 第1.2節の6つの動きの要素を \(9\times9\) の盤で示した模式図。走りは最初の駒で止まり、それを取れる。跳びは間の駒を無視する。跳び越え走りは2升を飛び越える。鉤行は空き升で一度曲がる。エリアムーブは最大2歩動く。範囲取りは階級の低い駒を飛び越えてすべて取る。

2. 初期局面からの正確な数

定義4（perft）。 \(\mathrm{perft}(s,0)=1\)、\(\mathrm{perft}(s,n)=\sum_{m\in\mathrm{Mv}(s)}\mathrm{perft}(s\cdot m,\,n-1)\)。
\(n\)\(\mathrm{perft}(s_0,n)\)前の値との比
197-
29,39396.8
31,426,099151.8
10^010^110^210^310^410^510^610^797n = 19,393n = 21,426,099n = 3破線：97ⁿ（毎手97通りなら）perft(s₀, n)
図3. 正確なノード数 \(\mathrm{perft}(s_0,n)\) の対数軸グラフ。破線は \(97^n\)。利きが開くにつれて、実際の数は \(n=3\) から \(97^n\) よりわずかに速く増える。

V 初手の合法手は先手に \(97\) 通りある。\(\mathrm{perft}(s_0,2)=9393\) は \(97^2=9409\) より \(16\) 小さい。後手の応手の数は先手の初手によってわずかに変わる（平均は \(9393/97\approx96.8\)）。

Lean での主張：L theorem perft_one : (moves init).card = 97。同様に perft init 2 = 9393、perft init 3 = 1426099。まず decide / native_decide で確認し、カーネルが現実的な時間で許す場合にはコンパイラを使わない証明に置き換える（第9節）。

3. 状態空間の大きさ

命題1（粗い上界）。 \(|\mathcal S|\le 2\,(1+2|K|)^{N^2}\)。\(|K|=301\)、\(N=36\) のとき \(\log_{10}|\mathcal S|<3604\)。P
証明。 各升は \(1+2|K|\) 通りの値をとり、手番は2通りある。\(\square\)
命題2（初期配置の数）。 両軍の初期配置（種類の多重集合、各402枚）を空の盤に置く方法の数は \[\frac{1296!}{(1296-804)!\;\prod_{k}\big(m_k!\big)^2}\;\approx\;10^{2181}\] である。ここで \(m_k\) は片軍における種類 \(k\) の個数。P（多項係数。指数は配置表から正確に計算した。）

どちらの数も、他のゲームでよく引用される値（Allis, 1994 の表による）：チェス \(\approx10^{46}\)、将棋 \(\approx10^{71}\)、囲碁 \(\approx10^{172}\) の局面数 C をはるかに上回る。 到達可能な局面は駒が最大804枚で、取りは不可逆であるため、はるかに良い上界があるはずだが、どのような上界でも全探索の対象にはならない天文学的な大きさである。

チェス10^46将棋10^71囲碁10^172大局将棋：初期配置の数10^2181大局将棋：上界10^3604局面数の常用対数チェス・将棋・囲碁：Allis (1994) の表より。大局将棋：本ページ第3節。
図4. 状態空間の大きさ（対数軸）。大局将棋の2本は数学的な上界（初期配置の数と命題1の粗い上界）であり、到達可能な局面の数ではない。

3.1 終盤テーブルベースは手が届く

王と他の1枚 対 王だけの配置数は \(1296\cdot1295\cdot1294\cdot 2=4,343,492,160\)（3つの異なる駒の順序付き配置に手番の2通りを掛けたもの）P。 約 \(4.3\times10^{9}\) 状態であり、このような終盤の全後退解析は現実的な計算で、すべての駒種について正確な勝ちまでの手数表が得られる。O まだ計算していない。

4. 分岐数とゲーム木の大きさ

ランダムな対局（固定シードで30局、最大120手）の局面 3,600 個で、合法手の数を測った V：

手数0–1920–3940–5960–7980–99100–119
合法手の平均203.0267.8307.4349.8382.9412.9
150250350450203.00–19267.820–39307.440–59349.860–79382.980–99412.9100–119手数合法手数の平均
図5. ランダムな対局での合法手数の平均を手数の範囲別に示す（30局、固定シード）。盤が開くにつれて増える。

全体の平均は \(\bar b\approx 320.6\)、最大は 608 である。手数とともに増えるのは、駒が取られて盤が開け、走り駒の利きが通るようになるためである。 （ランダムな指し方は強い指し方を代表しないので、\(\bar b\) は大まかな目安であり、強者の対局の推定値ではない。）

Allis にならい、ゲーム木の複雑さの推定は平均の対局の長さ \(d\) 手に対して \(\bar b^{\,d}\) とする。実際の対局の長さは不明なので、表にする：

\(d\)（手）\(\log_{10}\bar b^{\,d}\)
100251
200501
4001002
8002005
01002003004000200400600800チェス 10^123将棋 10^226囲碁 10^360対局の長さ d（手）log₁₀ b^db ≈ 320.6
図6. Allis 流の推定 \(\log_{10}\bar b^{\,d}\) を未知の対局の長さ \(d\) に対して示す。破線は、チェス・将棋・囲碁のよく引用されるゲーム木の大きさ。

比較として、Allis はチェス \(\approx10^{123}\)、将棋 \(10^{226}\)、囲碁 \(10^{360}\) を挙げている C。200手の短い対局でも、この3つをすべて超える。

5. 移動力と駒の価値

定義5。 種類 \(k\) の升 \(p\) での移動力 \(\mu(k,p)\) は、他に駒のない盤の \(p\) に \(k\) の駒が1枚だけあるときの合法手の数である。 ゲームの評価関数は \(v(k)=10+2\,\mu(k,c)\) を使う。\(c=(18,18)\) は中央付近の升で、王類には支配的な一定値を与える。

V 301 種について、最小 \(\mu=1\)、中央値 \(43\)、平均 \(70.0\)、最大 \(2,520\)。最大は Hook mover で、曲がる経路が数を増やす：\(\mu\) は動き \((\text{from},\text{to},\text{via})\) を数えるため、複数の曲がり升から届く1つの行き先は複数回数えられる。 （異なる行き先の升の数はそれより小さい。第9節 M6 を参照。）

010203040506070809010011142–3334–7308–152616–318032–639564–12718128–2554256+移動力 μ（中央からの手数）駒の種類数赤：飛車（70）を含む区間　青：角の平均（46）を含む区間
図7. 301種の駒の移動力 \(\mu\) の分布（倍々の区間；最後の区間は \(\mu\ge256\) の全種）。赤い棒は飛車の値70を、青い棒は角の平均46を含む。
命題3（飛車）。 空の \(N\times N\) の盤で、飛車はどの升からでもちょうど \(2(N-1)\) 手をもつ。したがって平均の移動力は \(N=36\) で \(2(N-1)=70\)。P
証明。 \((x,y)\) から、横には \(x+(N-1-x)\)、縦には \(y+(N-1-y)\) 升あり、合計 \((N-1)+(N-1)\)。\(\square\)
命題4（角）。 空の \(N\times N\) の盤の全升にわたる角の平均移動力は \[\bar\mu_{\mathrm{B}}(N)=\frac{2(N-1)(2N-1)}{3N},\qquad \bar\mu_{\mathrm B}(8)=8.75,\quad \bar\mu_{\mathrm B}(36)=\frac{2\cdot35\cdot71}{108}\approx 46.02.\] P
証明。 \((x,y)\) から方向 \((+1,+1)\) に届く升の数は \(\min(a,b)\)（\(a=N-1-x\)、\(b=N-1-y\)）である。他の3つの斜め方向は盤を反転すれば同じなので、 \(\bar\mu_{\mathrm B}=\tfrac{4}{N^2}\sum_{a,b=0}^{N-1}\min(a,b)\)。\(\min(a,b)=m\) となる組 \((a,b)\) の数は \((N-m)^2-(N-m-1)^2=2(N-m)-1\) なので、 \[\sum_{a,b}\min(a,b)=\sum_{m=0}^{N-1}m\,(2(N-m)-1)=(2N-1)\tfrac{N(N-1)}{2}-2\tfrac{(N-1)N(2N-1)}{6}=\tfrac{(N-1)N(2N-1)}{6}.\] これに \(4/N^2\) を掛けると \(\tfrac{2(N-1)(2N-1)}{3N}\) を得る。\(\square\)
6935角の手数平均 46.02（飛車はどの升でも70）
図8. 空の \(36\times36\) の盤の全升での角の移動力。端で最小、中央で最大で、平均はちょうど \(\frac{2(N-1)(2N-1)}{3N}\)（命題4）。

したがって、この盤でのチェスのクイーン（飛車＋角の動き）の平均移動力は \(\approx 70+46.02=116.02\) である。飛車と角の平均移動力の比は \(70/46.02\approx1.52\) で、チェスの古典的な評価 \(5:3.25\approx1.54\) に近い。 示唆的ではあるが、障害物を無視しているので、駒の価値の導出ではない。障害物の密度 \(\delta\) をランダムに与え、走りの長さが幾何分布に従うとする占有を考慮した移動力のモデルが、自然な改良である。O

6. 範囲取りと階級の代数

定義6（範囲取り）。 \(d\) を方向、\(r\in\mathbb N\) を階級とする。局面 \(\pi\) に対し、 \(J=\max\{\,j\ge 0 : \forall i\le j,\ p+id\in B \text{ かつ } (\pi(p+id)=\varnothing \text{ または } \rho(\mathrm{kind}\,\pi(p+id))<r)\,\}\) とおく。 \(\mathrm{RC}(d,r)\) は、\(p\) から \(1\le j\le J\) の空きまたは取れる升 \(p+jd\) への動きで、\(p+d,\dots,p+jd\) のうち駒のある升を味方・敵を問わずすべて取るものからなる。駒種の \(r\) をその取りの階級という。
3121524範囲取り駒（階級 r = 3）階級5 ≥ r：ここで止まるJ = 4：飛び越える升（階級 < 3）通過した駒をすべて取る：ここでは階級1・2・1の駒
図9. 階級 \(r=3\) の範囲取り。筋は階級1・2・1の駒を飛び越えてすべて取り（赤）、階級5の駒（灰色）で止まる。途中の空き升（緑）は通過するだけ。
補題1（範囲取りで取れない駒）。 \(\mathrm{RC}(d,r)\) の動きが種類 \(k\) の駒を取るなら \(\rho(k)<r\)。特に王類は \(\rho=\infty\) なので、範囲取りが王類を取ることはない。 \(\mathrm{RC}\) の動きが取る駒は高々 \(N-1=35\) 枚。P L
証明。 取られる升は \(p+id\)（\(i\le J\)）の中にあり、\(J\) の定義によりすべて \(\rho<r\) を満たす。1本の筋には高々 \(N-1\) 升しかない。\(\square\)
補題2（単調性）。 \(p,d,\pi\) を固定するとき、\(r\le r'\) ならば \(J(r)\le J(r')\) で、\(r\) のもとで飛び越える升の集合は \(r'\) のもとでのそれの先頭部分である。したがって、同じ方向をもつなら階級の高い範囲取り駒は低いものを弱い意味で支配する。P L
証明。 \(J\) を定める述語は \(r\) が大きいほど弱くなる。\(\square\)

Lean での予定の形。

-- スケッチ（まだコンパイルしていない）
inductive Side | black | white
structure Pos where
  board : Fin 36 → Fin 36 → Option (Kind × Side)
  turn  : Side

def rangeCapturePassed (π : Pos) (p : Fin 36 × Fin 36) (d : Int × Int) (r : Nat) : List (Fin 36 × Fin 36) := ...

theorem rangeCapture_rank_lt {π p d r c} (hc : c ∈ captured (rangeCapture π p d r)) :
    rank (kindAt π c) < r := by ...

theorem royal_untouchable {π p d r c} (hc : c ∈ captured (rangeCapture π p d r)) :
    ¬ isRoyal (kindAt π c) := by ...

theorem rangeCapture_card_le {π p d r} : (captured (rangeCapture π p d r)).length ≤ 35 := by ...

7. 対称性と不変量

命題5（手番の対称性）。 \(\tau(x,y)=(N-1-x,\,N-1-y)\)（180°回転）とし、これを手番を入れ替えて局面に拡張する。初期局面は \(\tau\) で不変である P （両軍は同じ配置表から生成される）。また \(\tau\) は \(s\) の合法手を \(\tau s\) の合法手へ全単射に写す（動きの規則は動かす側を基準に定義されている）。特に \(\tau\) は \(\mathrm{Mv}(s)\) を \(\mathrm{Mv}(\tau s)\) へ全単射に写すので、 \(|\mathrm{Mv}|\) は \(\tau\) で結ばれる局面で一致する。L

初期配置は左右対称ではない（12段のうち左右対称に読めるのは2段だけ）V。したがって、初期局面には利用できる鏡映対称性はない。

証明すべき不変量。 L (i) 各側の駒の数は、相手の取りによってしか減らない；(ii) 駒は履歴の中で高々1回しか成らない（成った種類は \(\mathrm{pr}=\bot\)）；(iii) 既定の規則では、駒は成りゾーンに入るか、そこで終わる動きでのみ成る；(iv) 対局は、一方に王類がなくなったときちょうど終わる；(v) \(\mathrm{Mv}(s)=\varnothing\)（動ける手がない）はありうるので、その結果を定めておく必要がある。

8. 計算量の文脈

\(n\times n\) への一般化では、チェスは EXPTIME 完全（Fraenkel & Lichtenstein, 1981）、将棋は EXPTIME 完全（Adachi, Kamekawa & Iwata, 1987）、日本ルールの囲碁も EXPTIME 完全（Robson, 1983）である C。 大局将棋は有限の1つの例なので、漸近的な計算量クラスは直接には当てはまらない。\(N\) を大きくし、配置を相応に拡大して、上記の動きの要素の固定された集まりで定義したゲームの族も EXPTIME 完全であろうと予想する。 自然な道筋は、一般化将棋の局面からの帰着である（将棋のすべての駒は大局将棋の要素だからである）。O 証明はない。

無限の対局。 実装されている規則には千日手や手数制限がないので、ゲームのグラフには閉路があり、局面の値は通常の後退解析の不動点で定義される（有限手数での勝ち・負け、それ以外は無限に続く引き分け）。 Lean で形式化するには、帰納的述語 WinIn : Nat → Pos → Side → Prop と、負けを避け続けることの余帰納的な概念が必要である。L

9. Lean 4 での機械検証された形式化のロードマップ

上のモデルを Lean 4（de Moura & Ullrich, 2021）で構築し、本ページの V と P の主張をすべてカーネルが検証した定理にし、数え上げの主張をゲームが実行するのと同じデータに結びつけたい。予定のマイルストーン：

  1. M1 データ。 301種（ベツァ記法による動きの記述）を Lean の構造体として取り込み、生成した要素の表がエンジンの使うものと等しいことを証明する。
  2. M2 局面と動き。 Pos、各要素の動きの関数（走り、跳び、跳び越え走り、鉤行、エリア、範囲取り）、moves : Pos → Finset Move を定義し、健全性（すべての動きは盤内にあり、範囲取り以外では味方を取らず、範囲取りで王類を取らない）を証明する。
  3. M3 Perft。 perft init 1 = 97、perft init 2 = 9393 を decide で；perft init 3 = 1426099 は素朴な moves からの洗練証明をもつ、検証された効率的な実装で。native_decide を使わない \(n=3\) のカーネル検証は大きな計算（葉が約 \(1.4\times10^{6}\)）で、特注の反射的証明が必要になるかもしれない。
  4. M4 不変量。 第7節の (i)–(v)。
  5. M5 階級の代数。 補題1・2、そして範囲取りが3枚以上を取れる唯一の動きの要素であるという主張。
  6. M6 閉じた式。 走り駒の平均移動力（命題3・4）を、任意の方向集合 \(D\subseteq\{-1,0,1\}^2\) へ一般化し、\(N=8\) と \(N=36\) では decide で確認する。
  7. M7 対称性。 命題5とその結果としての結果クラスへの帰結。
  8. M8 ゲーム理論。 後退帰納による結果の述語、小さな終盤ソルバー（王＋1枚 対 王）の正しさ、各駒種についてテーブルベースの値が \(4.3\times10^{9}\) の範囲で計算できるという主張。
M1 データM2 局面と合法手M3 PerftM4 不変量M5 階級代数M6 閉じた式M7 対称性M8 ゲーム理論
図10. 第9節の Lean のマイルストーン M1–M8 の依存関係。

式を超えて、Lean は資料の細かい点を浮かび上がらせるだろう。残された規則の記述が食い違う箇所（成り、鉤行、エリアムーブの端の場合）では、形式的な定義が選択を迫るので、選択はそれぞれラベル付きの規則パラメータとして公開する。

10. AI を賢くし、ゲームを解く

現在の AI。 コンピューターの相手は、キラーと履歴による手の並べ替え、最高難度での静止探索、持ち時間（ふつう 1.5 秒、むずかしい 3 秒）をもつ反復深化のアルファベータ探索である。評価は、第5節の移動力による価値 \(v(k)=10+2\mu(k,c)\) で重みづけした駒の損得に、位置の項（前進と敵の王類への圧力）を加えたものである。 強くはない：分岐数が \(\approx 320.6\)（第4節）なので、一定時間の探索が届くのは数手先にすぎない。

目標。 AI を大幅に賢くし、数学が許す限り、ゲームを解くことを目指している。Allis にならい、ゲームは、初期局面の値がわかっているとき超弱解決、初期局面からその値を達成する戦略がわかっているとき弱解決、すべての局面の値がわかっているとき強解決されたという。 ここで強解決は不可能である：第3節は状態空間を \(10^{3604}\) でしか抑えておらず、両軍の初期配置の数だけでも \(\approx10^{2181}\) である。ゲーム全体の弱解決・超弱解決も、今日の計算能力による力まかせの探索をはるかに超えている。そこで計画は段階的である：

  1. 探索の工学。 Zobrist ハッシュによる置換表、より良い手の並べ替え、ヌルムーブと後ろの手の削減、より速い合法手生成（現在の生成器は速度ではなく明快さのために書かれており、\(\mathrm{perft}(s_0,3)\) の \(1.4\times10^6\) の葉を列挙するのに約20秒かかる）。すべての最適化は、第2節の perft の基準値と照合する。
  2. 学習による評価。 手で決めた移動力の価値を、移動力モデルを事前分布とした自己対戦から学習した価値関数に置き換え、モンテカルロ木探索または方策ネットワークで、\(\approx 320.6\) 手のうち有望な数百手に探索を絞る。
  3. 序盤・中盤の知識。 自己対戦から作る定跡と、各版の前の版に対する強さの測定（そのための AI 対 AI の対戦用ハーネスはすでにある）。
  4. 終盤テーブルベース。 王＋1枚 対 王（\(4.3\times10^{9}\) 状態、第3.1節）から始め、各側2〜3枚の局面へと進める、小さな駒数の終盤の正確な後退解析。これらは強解決された部分ゲームで、探索の葉に正確な値を与える。
  5. 規則の縮小版の解決。 縮小した配置による小さな盤（たとえば \(N=8,\dots,12\)）の完全な解決。先手有利や引き分けやすさが大きさにどう依存するかを知り、ゲーム全体についての証拠とする。
  6. 検証されたソルバー。 計算がゲーム理論的な値（テーブルベースや縮小盤の解）を主張する場合、Lean で検査される証明オブジェクトで保証し（第9節 M8）、公表された結果が「プログラムがそう言った」だけにならないようにする。

大局将棋の完全な解決は、可能だとしても長いあいだ手の届かないままだと予想している。この取り組みの目的は、AI を測定可能な形で強くし、解ける断片のすべてについて正確な結果を確立し、境界がどこにあるかを正確に述べることである。O

11. 未解決問題

  1. 先手有利か。（チェスや将棋でも未解決であり、ここでは探索で決められるはずもない。）O
  2. 強者の対局での対局の長さの経験分布は。これが実際のゲーム木の大きさを決める（第4節）。
  3. 小さな駒数の到達可能な局面数の正確な値（第3.1節）と、各駒種について 王＋1枚 対 王 での最長の強制勝ち。
  4. 多重度 \(m_k\) による到達可能な局面数の厳密な組合せ論的上界。
  5. 拡大した族の計算量（第8節）。
  6. 範囲取りの将に、取りだけの手順に閉路がないことを示す美しいポテンシャル関数はあるか。取りでは駒の数が減るので自明だが、取りと取りの間の取らない手の数が有界かという、より強い問題は未解決である。

参考文献

  1. H. Adachi, H. Kamekawa and S. Iwata. Shogi on \(n\times n\) board is complete in exponential time. Trans. IEICE J70-D(10):1843–1852, 1987（日本語）。
  2. L. V. Allis. Searching for Solutions in Games and Artificial Intelligence. PhD thesis, University of Limburg, 1994.
  3. R. Betza. Chess with different armies and the “funny notation” for piece moves. Chess Variant Pages, 1996.
  4. L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. CADE-28, 2021.
  5. A. S. Fraenkel and D. Lichtenstein. Computing a perfect strategy for \(n\times n\) chess requires time exponential in \(n\). J. Combin. Theory Ser. A 31(2):199–214, 1981.
  6. G. Hodges. Ten Shogi Variants. 2002.
  7. J. M. Robson. The complexity of Go. Proc. IFIP Congress, 1983.
  8. C. E. Shannon. Programming a computer for playing chess. Philosophical Magazine 41(314):256–275, 1950.
  9. J. Tromp. Counting legal Go positions (with G. Farnebäck), 2016、およびチェスの局面数についての推定。
  10. “Taikyoku shogi”, English Wikipedia (CC BY-SA 4.0)：ここで使った駒の一覧と初期配置の出典。

エンジン、データ、V の数値を生成するスクリプトはプロジェクトのリポジトリにあり、本ページの数値は data/math_stats.json から python3 tools/build_math.py で再生成される。 誤りの指摘や Lean の開発への協力のお申し出は hello@taikyokushogi.com まで。日本語版は機械で作成しており、専門家による校正をまだ受けていない。