💻 computer science

An ASP-based approach to Solving General Stochastic Two-Player Games

本論文は、不確実性を伴う二人対戦型ターン制一般ゲーム記述言語（GDL）ゲームを解決するための最初の ASP ベースのアプローチとして、確率的回答集合プログラミング（SQASP）を導入し、小規模な確率的ゲームにおける前方探索との競争力および終局評価における可能性を実証する。

原著者： Yifan He, Michael Thielscher

公開日 2026-05-25

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Yifan He, Michael Thielscher

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

コンピュータにボードゲームの遊び方を教えることを想像してみてください。通常、これらのゲームはチェスのように、あなたが手を打ち、相手も手を打ち、盤面が予測可能な形で変化するものです。しかし、もしそのゲームに「ワイルドカード」が関与していたらどうでしょうか？あなたが手を打った後、魔法のサイコロの転がりがその手が有効かどうかを決定したり、あるいは第三の目に見えないプレイヤー（彼を「ランダム」と呼びましょう）が歯車に楔を打ち込んだりする可能性があったらどうでしょうか？

この論文は、こうした厄介で予測不能なゲームをコンピュータに解かせることについて扱っています。著者の黄一凡（Yifan He）とマイケル・ティエルシャー（Michael Thielscher）は、運が関与する状況において最善の戦略を導き出すための新しい数学的ツールキットを構築しました。

以下に、彼らのアプローチを簡単な比喩を用いて解説します。

1. 問題点：「ランダム」なプレイヤー

標準的なゲーム理論において、コンピュータは賢い相手に対する完璧な手を計算するのが得意です。しかし、ランダム性（サイコロを振ったりカードを引いたりすることなど）を加えると、数学は複雑になります。

従来の方法: 以前のコンピュータプログラムは、二人の賢いプレイヤーがいるゲーム（チェスなど）か、一人のプレイヤーとランダムな要素があるゲーム（ソリティアなど）のどちらかを処理できました。しかし、二人の賢いプレイヤーとランダムな要素を同時に扱うゲームは処理できませんでした。
目標: 著者たちは「一般確率的二人零和ゲーム」を解きたがっていました。これは、あなたが X を置こうとするたびに、そのマスが 30% の確率で O に変わったり、50% の確率でその手が完全にブロックされたりするような、三目並べのようなゲームだと考えてください。

2. 新しいツール：SQASP（「魔法の設計図」）

著者たちは**確率的回答集合プログラミング（Stochastic Answer Set Programming、SQASP）**と呼ばれる新しい言語を発明しました。

比喩: あなたが家を設計する建築家だと想像してください。あなたは設計図（ゲームのルール）を持っています。過去には、二人の特定の種類の建設業者のための家しか設計できませんでした。一人は天才的な戦略家（相手）、もう一人は厳格なルールに従うロボットです。
革新: SQASP は、天才的な戦略家、ロボット、そしてギャンブラーがすべて協力して作業する建設現場を記述できる新しいタイプの設計図のようなものです。
- 天才（プレイヤー X）は勝ちたいと考えています。
- 相手（プレイヤー O）はプレイヤー X を止めたいと考えています。
- ギャンブラー（ランダム）は次に何が起こるかを決定するためにコインを投げます。
SQASP を通じて、コンピュータは次のように問いかけることができます。「相手が私を止めるために完璧に動き、ギャンブラーがやりたい放題をする場合、私が勝つ最高に高い確率は何か？」

3. 翻訳機：設計図をパズルに変える

コンピュータは「設計図」を話しません。彼らは「論理パズル」を話します。

プロセス: 著者たちは翻訳機（sqasp2xssat というツール）を構築しました。これは彼らの凝った SQASP 設計図を取り込み、**拡張確率的充足可能性（Extended Stochastic Satisfiability、XSSAT）**と呼ばれる巨大な論理パズルに変換します。
隠喩: SQASP をケーキの複雑なレシピだと考えてください。翻訳機は、そのレシピを巨大で多層構造の数独パズルに変える機械です。パズルが解かれると、その答えはゲームに勝つ正確な確率を教えてくれます。
ソルバー: 彼らは既存のソルバー（SharpSSAT）を使って、この数独を解きました。ソルバーが「はい、このパズルは解けます」と言えば、それはプレイヤーに勝利戦略があることを意味します。もし 67% の確率を計算すれば、それが最良の結果となります。

4. 「量化子シフト」のトリック

この論文では、**量化子シフト（Quantifier Shifting）**と呼ばれる特定の最適化技術もテストされました。

比喩: あなたがトーナメントを運営していると想像してください。
- 方法 A（ベースライン）: すべてのプレイヤーの手をリストアップし、次にその手が合法かどうかをチェックし、その後ゲームが終了したかどうかをチェックします。
- 方法 B（シフト）: 手をリストアップする前に、その手が合法かどうかをチェックします。違法な手を計画する時間を無駄にしないため、これはより速く見えるように思えます。
結果: 二人の賢いプレイヤーがいるゲーム（決定論的ゲーム）では、この「シフト」のトリックは劇的な速度向上をもたらします。しかし、著者たちは「ギャンブラー」がいるゲーム（確率的ゲーム）では、このトリックがほとんど違いをもたらさなかったことを発見しました。
なぜか？: 彼らが使用したソルバー（SharpSSAT）は非常に賢いです。それは「ユニット伝播（unit propagation）」と呼ばれる組み込みの「探偵」を持っており、指示の順序に関係なく、違法な手を独自に突き止めます。したがって、この特定のソルバーにとっては、凝った並べ替えは不要でした。

5. 結果：性能はどうだったか

チームは、三目並べ、コネクト4、ニムといった古典的なゲームの変種に、このシステムをテストしました。ただし、「ランダム」なプレイヤーが追加されたバージョンです。

性能: 新しい手法は、コンピュータが頭の中で何百万回もゲームをシミュレーションして結果を見るような、標準的な「前方探索」法と競争力のある性能を示しました。
欠点: 小さな盤面（3x3 や 4x4 など）では非常にうまく機能しました。しかし、ゲームが大きくなりすぎると（ニムで 100 個の石の山など）、論理パズルがコンピュータが合理的な時間で解ける規模を超えてしまいました。
教訓: この手法は終盤の評価に優れています。ゲームがほぼ終了した段階で、このシステムは汎用ゲームプレイ AI に、「もしこの手を打てば、99% の確率で勝てるよ」と伝えることができ、最終的な決定を助けます。

まとめ

著者たちは、運と戦略が衝突するゲームを数学的に記述する新しい方法を作成しました。彼らはこれらの記述を、コンピュータが解いて「最良の勝率」を見つけることができる論理パズルに変換しました。あらゆるゲームサイズに対する万能薬ではありませんが、論理プログラミングを用いて複雑で不確実なゲームを解くことができることを証明し、混沌とした世界においてコンピュータが未来をより良く考えるための手段を提供しました。

彼らが主張しなかったこと:

彼らは、ボード全体が見えないゲーム（ポーカーやクリエグ・三目並べなど）にこれが機能すると主張していません。彼らは明確に、この手法は全員がボード全体を見るゲーム（完全情報ゲーム）向けであると述べています。
彼らは、これが直ちにすべての他の AI 手法を置き換えるとは主張していません。特に終盤戦などの特定のシナリオにおける代替手段であると指摘しています。

技術的概要：確率的な二人対戦ゲームを解くための ASP ベースのアプローチ

問題定義

一般ゲームプレイ（GGP）システムは、ルールを事前に知らずに、実行時の記述に基づいて戦略的ゲームをプレイすることを目指しています。ゲーム記述言語（GDL）とその拡張である GDL-II は、そのようなゲームを指定するための標準的な形式言語であり、GDL-II はランダム性（確率性）と部分観測性をサポートしています。回答集合プログラミング（ASP）は、決定論的な一人および二人の GDL ゲームを解くために成功裏に適用されてきましたが、既存の ASP フレームワークには、敵対的（ミニマックス）な振る舞いと確率的な振る舞いを同時に表現する能力が欠けています。その結果、不確実性を伴う二人対戦のターン制 GDL ゲームを ASP ベースの手法で解くという点にギャップが存在します。

手法

著者らは、新しい言語と翻訳ベースのソルバーを導入することで、二人対戦の確率的 GDL ゲームを解くための新規アプローチを提案します。

1. 確率的量化回答集合プログラミング（SQASP）

ASP と確率的ゲーム解決の間のギャップを埋めるため、本論文は確率量化子を追加した QASP（Quantified ASP）を拡張した言語SQASPを導入します。

構文: SQASP プログラムは $Q_1.x_1 \dots Q_n.x_n \ P$ の形式をとります。ここで $P$ は通常の論理プログラムであり、量化子 $Q_i$ は存在量化（ $\exists$ ）、全称量化（ $\forall$ ）、または確率量化（ $\mathcal{R}_{p}$ ）のいずれかです。
意味論: SQASP プログラムを満たす最大確率は、再帰的に定義されます。確率量化子 $\mathcal{R}_{p}$ は、変数が真となる確率 $p$ を割り当て、部分式のプロバビリティに基づいて期待値を計算します。
翻訳: 著者らは、SQASP プログラムを**拡張確率的充足可能性（XSSAT）**式に変換するツール sqasp2xssat を実装しました。XSSAT は、確率量化子を追加した量化ブール式（QBF）を拡張したものです。この翻訳は、既存のツール（lp2sat など）を活用して、論理プログラム $P$ を、そのモデルが $P$ の安定モデルに対応する CNF 式 $\psi$ に変換するものです。

2. GDL ゲームの SQASP への符号化

中心的な貢献は、プレイヤー $x$ が $n$ 手以内で勝利する最大確率 $P_x^w(S_0, n)$ に等しい最大充足可能性確率を持つ SQASP プログラム $\Psi$ を構築することです。この符号化は、主に 2 つのフェーズで進行します。

協調的ベースライン: まず、すべてのプレイヤー（対戦相手 $o$ およびランダムプレイヤー $r$ を含む）が $x$ の勝利に至る終了状態へ到達するために協調すると仮定して、論理プログラム $P_c$ を構築します。これにより、有効なゲームの進行、 $n$ 手以内の終了、および目標状態の達成が保証されます。
敵対的および確率的モデリング: 次に、プログラムを拡張して、対戦相手および環境の特定の振る舞いを捉えます。
- 敵対的プレイヤー（ $o$ ）: 決定変数（dec_o）に対する全称量化（ $\forall$ ）を用いてモデル化されます。これにより、ソルバーは対戦相手が $x$ の勝利確率を最小化する最悪のシナリオを考慮することを強制されます。この符号化では、ルール数を削減するために行動の対数表現が使用されます。
- 確率的プレイヤー（ $r$ ）: 確率量化子（ $\mathcal{R}_{1/i}$ ）を用いてモデル化されます。この符号化により、ゲームが終了していない場合、ランダムプレイヤーが利用可能な合法手から均等に 1 つの合法行動を選択することが保証されます。これは、合法行動を数え上げ、決定変数（dec_r）に確率制約を適用することで達成されます。

3. 量化戦略

本論文は、生成された XSSAT 式に対する 2 つの量化戦略を検討します。

ベースライン手法（ $Q_b$ ）: 選択原子（legal、terminal など）以外のすべての原子は、選択原子の厳密な時間的順序に従って、最も内側の存在量化ブロックに配置されます。
依存関係ベースの手法（ $Q_d$ ）: 決定論的ゲームの技術に着想を得たこの手法は、非選択原子を、依存する選択原子の直後に、量化子接頭辞の中でできるだけ早く出現するようにシフトさせます。これは、does に対して分岐する前に legal などの値を固定することで、探索空間を削減することを目的としています。

主要な貢献

確率的 GDL 向けの最初の ASP ベースソルバー: 本論文は、二人対戦、確率的、ターン制の GDL ゲームを ASP を用いて解く最初の手法を提示します。
SQASP 言語: 敵対的推論と確率的推論を論理プログラミングの枠組み内で統合する、確率的量化回答集合プログラミングの導入。
翻訳ベースのソルバー: SQASP プログラムを XSSAT 式に変換する sqasp2xssat の開発。これにより、既存の XSSAT ソルバー（特に SharpSSAT）をゲーム解決に利用できるようになります。
理論的正当性: 著者らは、GDL ゲームにおける最大勝利確率と、生成された SQASP/XSSAT 式の最大充足可能性確率との等価性を確立する形式的証明（定理 2 および 3）を提供します。

実験結果

著者らは、Tic-Tac-Toe、Connect-4、Nim の確率的変種において自らのアプローチを評価し、SQASP ベースの手法（ $Q_b$ および $Q_d$ 量化の両方を使用）を、前方探索 Expected Minimax（EMM）ソルバーと比較しました。

パフォーマンス: ASP ベースのアプローチは、小規模な確率的ゲームにおいて前方探索と競合する性能を示します。多くのケース（例：Tic-Tac-Toe、Connect-3）において、ASP ソルバーは EMM と同等の勝利確率を計算し、しばしば同程度の時間内に完了します。
量化子のシフト: 驚くべきことに、SharpSSAT ソルバーを使用する場合、依存関係ベースの量化（ $Q_d$ ）はベースライン（ $Q_b$ ）に対して顕著な性能向上をもたらさなかったことです。著者らは、これを SharpSSAT の内部ユニット伝播メカニズムに起因すると帰結しています。このメカニズムは、量化子の順序に関係なく原子（legal など）の値を導出できるため、明示的なシフトの必要性を実質的に緩和していると考えられます。
スケーラビリティの限界: このアプローチは、大きな山を持つ確率的 Nim のような、より大きな状態空間には苦戦します。生成される XSSAT 式は 100 万節を超えるなど巨大になり、現在のソルバーでは効率的に処理できません。一方、EMM は動的計画法と転置表により良好にスケーリングします。

意義と主張

本論文は、提案された ASP ベースのアプローチが、一般ゲームプレイシステムにおける終盤評価のための実用的な代替手段を提供すると主張しています。決定論的ゲームにおける ASP の成功した応用を確率的領域へ拡張することで、論理プログラミングが不確実性と敵対的推論を効果的に処理できることを実証しています。

著者らは控えめに、このアプローチがすべてのケース（特に非常に大きな状態空間を持つゲームや、Nim のような特定の構造を持つゲーム）において前方探索を凌駕するわけではないと指摘しつつも、決定論的ゲームに関する以前の結果を確率的なものへ成功裡に一般化していることを強調しています。彼らは、部分観測性（例：ポーカー、Krieg-Tic-Tac-Toe）への拡張を将来の重要な研究方向として特定し、現在の手法が完全情報ゲームに限定されていることを認めています。