Animation, Verification and Visualisation of Prolog Transition Systems with ProB

あなたは、バグが隠れているかもしれないコンピュータ・コードという「犯罪」を解決しようとしている探偵だと想像してください。コンピュータサイエンスの世界では、これを「形式検証（formal verification）」と呼びます。これは、プログラムがどのように振る舞うべきかという完璧な数学的地図を構築し、プログラムが道に迷ったりクラッシュしたりしないよう、あらゆるステップをチェックするようなものです。通常、これには専門家にしか読めない複雑な数学が伴います。しかし、もしその退屈な数学を、生き生きとしたビデオゲームに変えることができたらどうでしょう？それが、プログラミング言語「Prolog」の魔法です。Prologは、標準的な命令ではなく、論理パズルとして考える言語です。このPrologに「PROB」と呼ばれるツールを組み合わせると、「モデルチェッカー」が出来上がります。これは、あなたの論理パズルが展開される様子を見守り、間違いを特定し、さらに物事がどこでうまくいかなくなったのかを正確に把握するために、物語を一歩ずつ進めていくことができる、非常に賢いロボットです。

この論文は、そのロボットに大幅なアップグレードを与えることについて書かれています。著者であるハインリッヒ・ハイネ大学デュッセルドルフの研究チームは、既存のツールであるPROB（すでにPrologを話せるツール）を取り上げ、そこに全く新しい一連の「スーパーパワー」を追加しました。これは、白黒のスケッチブックを、高精細でインタラクティブな映画スタジオへと変えるようなものです。彼らは、何が起きているかを可視化する方法を容易にし、戦略をテストするために数秒間で数千のゲームをシミュレートする方法を追加し、さらにはアクションを一時停止してコンピュータに特定の指示を与え、その反応を観察できるシステムを作り上げました。彼らはこれらの新機能を、クラシックなゲームである「コネクト・フォー（四目並べ）」を論理パズルへと作り変えることでテストし、異なるコンピュータの「脳」同士を戦わせて、どちらが勝つかを検証しました。その結果、このツールキットは、複雑なコンピュータの論理をチェックすることを、宿題をする作業ではなく、ゲームをプレイすることのように感じさせてくれます。

「生きた」論理マップの魔法

その核心において、この論文は、Prolog（「もし〜ならば、〜である」というリストのように見える言語）で書かれた一連のルールを、どのように「遷移システム（transition system）」に変換するかを説明しています。ボードゲームを想像してください。そこでは、すべてのマス目が「状態」（例：「歩行者信号が赤」）であり、すべての動きが「遷移」（例：「青に切り替わる」）です。かつて、PROBはこれらのルールを読み込み、ボタンをクリックすることで一つのマスから次のマスへ移動し、その経路を示すことができました。しかし、それは少し使いにくいものでした。

著者たちは、この体験を大幅に洗練させました。まず、ビジュアルを格段に向上させました。以前は「状態：赤」といったテキストのリストが表示されるだけでしたが、現在は実際の絵を描画できるツールを統合しています。例えば、交通信号をモデル化している場合、ツールは画面上に実際に光る赤い円を表示できます。チェスのゲームをモデル化している場合は、駒が正確な位置にあるチェス盤を表示できます。さらに素晴らしいことに、インタラクティブな可視化を追加しました。画像内の駒を右クリックすると、実際のビデオゲームのように、実行可能なすべての合法的な動きを表示できます。また、これらの視覚的なストーリーをHTMLファイルとして書き出す機能も作成したため、特別なソフトウェアをインストールしていなくても、誰とでもこの論理パズルの「映画」を共有することができます。

「一時停止と問いかけ」機能

最もエキサイティングな新機能の一つは、「記号的遷移（symbolic transitions）」と呼ばれるものです。あなたがコンピュータとゲームをしている場面を想像してください。コンピュータが、次にあなたがどのような動きをしたいのか分からず、行き詰まってしまったとします。以前は、コンピュータは単に推測するか、停止してしまう可能性がありました。しかし現在、このツールは一時停止して、「ねえ、この部分については人間が決める必要があります！」と伝えることができます。ツールは、あなたが特定の値（例えば「ナイトをF3に動かす」など）を入力するのを待ち、それから物語を再開します。これは、コンピュータが自力で予測できない選択を人間が行う必要がある、複雑な定理の証明のような高度な論理のテストにおいて、非常に重要なことです。

また、「トレース・リプレイ（trace replay）」も改善しました。これは「セーブ機能」のようなものです。もし、問題解決に至る完璧な一連の動きを見つけたなら、それを保存できます。後でそのセーブファイルをロードすれば、ツールは全く同じ動きをステップバイステップで再現します。これは、今日バグを修正したとしても、明日になって誤って別の箇所を壊していないかを保証するために極めて重要です。新しいバージョンは、どの状態にいたかを正確に記憶するスマートな形式（JSON）でこれらのリプレイを保存するため、リプレイは常に完璧になります。

「百万ゲーム」シミュレーター

おそらく最も強力な追加機能は、「モンテカルロ・シミュレーション」を実行できる能力です。これは、「何が起こるかを見るために、ゲームを100万回プレイしてみよう」という高度な方法です。著者たちは、PROBを「SIMB」と呼ばれるシミュレーターに接続しました。単に一つのゲームを観察する代わりに、コンピュータにコネクト・フォーを1万回連続でプレイさせ、異なる戦略を戦わせることができます。

彼らはこれを用いて、コネクト・フォーに対する3つの異なる「脳」をテストしました。

1. ランダム（Random）: 何も考えずに動きを選ぶプレイヤー。
2. ミニマックス（Minimax）: 最善の経路を見つけるために数手先を読む、古典的なAI。
3. MCTS（モンテカルロ木探索）: 意思決定のために多くの可能な未来をシミュレートする、より賢いAI。

結果は非常に興味深いものでした。ランダムプレイヤーがミニマックスプレイヤーと戦った場合、ランダムプレイヤーが先手を取ると約55.7%の確率で勝利しましたが、ミニマックスが先手を取るとその数字は7.3%にまで低下しました。しかし、ミニマックスがMCTSと戦った場合、MCTSプレイヤーが圧倒し、約**99%**のゲームで勝利しました。著者らは、彼らのミニマックスプレイヤーはわずか2手先しか見ていない（浅い探索）ため、少し弱いプレイヤーであったと指摘しており、それがMCTSに対してこれほどまでに敗北した理由であると説明しています。

また、彼らはこれらのゲームにどれくらいの時間がかかったかも測定しました。ランダムとミニマックスのプレイヤーは高速で、1万ゲームを20分足らずで終了しました。しかし、MCTSプレイヤーは、膨大な思考を行っているため、同じ数のゲームを実行するのに数時間を要しました。興味深いことに、MCTSプレイヤーはランダムプレイヤーを倒すのに平均9.7手しか必要としなかったのに対し、ミニマックスは18.0手を必要としました。

なぜこれが重要なのか

これは単にゲームをプレイすることだけではありません。著者らは、これらのツールが教育に最適であることを示しています。例えば、プログラミングを学んでいる学生を想像してください。単にテキストの画面を見つめるのではなく、自分のコードが視覚的なアニメーションとして動き出す様子を見ることができるのです。もしミスをすれば、「交通信号」が赤に変わったり、「チェスの駒」が消えたりする様子が見えるため、何が間違っていたのかを理解するのが非常に容易になります。

また、この論文は、このシステムが「インタプリタ（解釈器）」の構築にも適していることを強調しています。インタプリタとは、あるプログラミング言語が別の言語と話すことを可能にする翻訳者のようなものです。PROBの新機能を使うことで、学生や研究者は他の言語（JavaやWebAssemblyなど）の翻訳器を簡単に構築し、それをビジュアライザー上で実行させることで、即座にテストすることができます。

結局のところ、著者らはコンピュータサイエンスのすべてを解決したと主張しているわけではありません。彼らは、これらの論理ツールをより視覚的、インタラクティブ、かつ大規模なシミュレーションが可能なものにすることで、バグをより早く発見し、学生をより良く教え、複雑なシステムをより深く理解できることを示唆しています。彼らは、将来的にこれらのツールが強化学習を用いてAIエージェントを訓練するために使用され、コンピュータが人間と同じように試行錯誤を通じてゲーム（あるいは論理パズル）をプレイすることを学習できる未来についても示唆しています。しかし、現時点での主な勝利は、論理証明という乾燥した抽象的な世界を、ルールを「見て、触れて、遊べる」遊び場へと変えたことにあるのです。