あなたは、チェスの駒が動くたびにルールが変わるような、あるいはドライバーの気分によって信号が変わる都市のような、カオスなシステムの未来を予測しようとしていると想像してください。コンピュータサイエンスの世界では、これは**確率的モデル検査（probabilistic model checking）**と呼ばれます。これは、システムにランダム性や偶然性が満ちている場合でも、特定の目標（例えば「すべての教授が会議を終える」など）に到達する確率がどの程度であるかを数学的に証明する方法です。問題は、システムに人数やパーツが増えるにつれて、起こりうるシナリオの数が爆発的に増加することです。それは、砂浜が成長し続けている中で、その砂粒を一つひとつ数えようとするようなものです。数学的な負荷が非常に重くなり、最速のスーパーコンピュータであっても、答えを出す前にメモリ不足や時間切れに陥ってしまいます。

長年、これらを解決するための最良のツールは、あらゆる行き止まりを描いた詳細な手書きの地図を見て迷路を進むようなものでした。これらのツールは、迷路に空きスペースが多い場合（疎なダイナミクス：sparse dynamics）には優れていますが、経路がぎっしりと詰まっている場合（密なダイナミクス：dense dynamics）には苦戦します。それらは、現代のビデオゲームやAIのエンジンである、最新のグラフィックスカード（GPU）に見られる超高速・並列処理に適さない、旧来の手法に依存しています。

そこで、ウォータールー大学の研究者によって開発されたTessaという新しいアプローチが登場しました。Tessaは、あらゆる可能性の地図を描こうとする代わりに、システム全体を、数学で**テンソル（tensor）**と呼ばれる巨大な多次元データブロックとして扱うことに決めました。テンソルを、退屈なスプレッドシートではなく、一度に押しつぶしたり、伸ばしたり、回転させたりできる数字のハイパーキューブ（超立方体）だと考えてください。この問題を、現代のグラフィックスカードが完璧に理解できる言語へと翻訳することで、Tessaは極めて複雑で大規模なシステムを、従来のツールよりもわずかな時間で計算することができます。

研究者たちは、これがうまくいくことを単に推測したのではなく、数学的に妥当であることを証明し、それをテストするためのツールを構築しました。Tessaを、いくつかのトリッキーで混雑したシナリオ（17個のプロセッサや10個のキューを含むモデルなど）で既存の最先端ツールと比較したところ、Tessaは100倍以上高速でした。500ステップのホライゾン（展望期間）を含む特定のテストでは、300倍以上高速でした。この論文は、問題の表現方法を「疎な地図」から「密で並列処理可能なデータブロック」へとシフトさせることで、以前は検証不可能だった規模のシステムを検証する能力を解き放てることを示しています。これはすべてを解決する魔法の杖ではありません（密なシステムには最適ですが、疎なシステムには向きません）。しかし、以前は手の届かなかった問題を解決するための、全く新しい遊び場を切り開くものです。

Tessaの物語：カオスをダンスに変える

Tessaがいかにしてこの魔法のようなトリックを実現しているのか、詳しく見ていきましょう。想像してみてください。あなたは、N人の教授がスマートフォンでアンケートを完了させようとしている様子を見守っています。各教授は、「離席中（電話を無視している）」、「記入中（アンケートを見ている）」、「完了（提出済み）」の3つの状態のいずれかにあります。毎秒、教授はメールに気づいたり、気が散ったり、あるいはようやく送信ボタンを押したりします。厄介なのは、誰でもいつでも中断される可能性があるということです。

全員が一定時間内に完了する確率を算出するために、従来のツールはすべての状態の組み合わせをリストアップしようとします。もし教授が10人いれば、$3^{10}$（59,049）通りの組み合わせがあります。20人になれば、30億通りを超えます。従来のツールは、これらの組み合わせを巨大で疎なリスト（空白のページがほとんどある辞書のようなもの）として保存しようとします。これは小規模なグループには機能しますが、グループが大きくなり、相互作用が複雑（密）になると、リストが大きすぎてメモリに収まらなくなり、コンピュータは窒息してしまいます。

Tessaの洞察：ハイパーキューブ
Tessaはこの問題を異なる視点で捉えます。リストとしてではなく、教授たちの状態を密なテンソル、つまり多次元の格子として捉えるのです。教授が10人いる場合、Tessaは59,049個のアイテムを持つリストを作るのではなく、各辺に3つのスロットを持つ10次元のキューブを作成します。それは、3層ではなく10層のレイヤーを持つルービックキューブのようなものです。

なぜこれが素晴らしいのでしょうか？ それは、現代のグラフィックスカード（GPU）がこれらのキューブを扱うように作られているからです。GPUは、数百万の数値に対して同時に同じ数学的操作を行うように設計されています。Tessaは、教授たちのルール（マルコフ連鎖の「もし〜ならば」のロジック）を、このキューブのための指示セットへと翻訳します。迷路を一段階ずつ進む代わりに、TessaはGPUに対して「キューブ全体を一気に押しつぶせ」と命じるのです。

「コンパイラ」の魔法
論文では、TessaがJAXと呼ばれるツールと、XLAと呼ばれるコンパイラを使用していることが強調されています。JAXを、教授たちのルールをGPUが流暢に話す言語に変換する翻訳者だと考えてください。XLAは、GPUが最も効率的に音楽を奏でられるよう指示を出す指揮者です。XLAは多くの小さなステップを一つの大きな滑らかな動きへと融合させ、GPUが停止と開始を繰り返して時間を無駄にしないようにします。これがTessaが非常に高速である理由です。ハードウェアと戦うのをやめ、ハードウェアとダンスを始めるのです。

結果：時間を加速させる
研究者たちは、文献にある3つの有名な「困難な」問題に対してTessaをテストしました。

1. キュー（待ち行列）: 10組の異なる行列を想像してください。Tessaは、次点のツールよりも100倍以上高速でした。
2. ウェザー・ファクトリー（天候工場）: 天候に基づいて工場が稼働とストライキを切り替えるモデルです。ここでも、Tessaは100倍以上高速でした。
3. ハーマンのプロトコル: プロセッサがリーダーの合意形成を図る古典的な問題です。ここでは、500ステップ先を見据えた場合、Tessaは競合と比較して300倍以上高速でした。

論文は、その限界についても非常に明確に述べています。Tessaはあらゆる問題に対する銀の弾丸ではありません。システムが非常に疎（接続が少なく、空きスペースが多い）である場合、古いツールの方がメモリ消費が少ないため、依然として優れている可能性があります。Tessaが輝くのは、システムが「密」なとき、つまりすべてがすべてと繋がっており、膨大な可能性のネットワークを生み出しているときです。

単なる検証を超えて：完璧な設定を見つける
Tessaができるもう一つの素晴らしいことがあります。問題を滑らかな数学的関数（テンソルプログラム）に変換するため、勾配降下法（gradient descent）を使用できます。これは、AIが猫を認識したり車を運転したりするために使用されるのと同じ数学です。これは、Tessaが単にシステムが機能するかどうかをチェックするだけでなく、システムを機能させるための「完璧な設定」を探索できることを意味します。

論文の中で、彼らはこれを「クヌース・ヤオのダイスローラー（Knuth-Yao die roller）」問題の解決に使用しました。彼らは、コンピュータが公平なサイコロを振るようにするために、2つのコインのバイアス（値 $p$ と $q$）の最適な値を求めたかったのです。Tessaは、コインのバイアスを「調整できるつまみ」として扱いました。Tessaは、つまみを回すことが結果にどのように影響するかを計算し、その後、エラーを最小化するために自動的にそれらを調整しました。そして、わずか数秒で完璧な値（$p=0.5$ および $q=0.5$）を見つけ出し、Tessaが検証だけでなく最適化にも使用できることを示しました。

結論
この論文は、問題を表現する方法を「疎なリスト」から「密なテンソル」へと変えることで、現代のハードウェアの強大なパワーを解き放てることを証明しています。これは、「砂粒を一つひとつ数える」ことから、「ブルドーザーを使ってビーチ全体を一度に動かす」ことへの転換です。これは状態爆発の問題（状態の数は依然として指数関数的に増加する）を解決するものではありませんが、解決可能な範囲を大幅に押し広げ、以前は検証不可能だったシステムの検証を可能にします。著者たちは、自分たちの数学的根拠（妥当性を証明した）と結果（実際のベンチマークで測定した）に自信を持っており、コンピュータサイエンティストの道具箱に強力な新しいツールを提供しています。