ロボットに、ボールを空中に保持し続ける、あるいは嵐の中を車で運転するといったゲームの遊び方を教えたいと考えていると想像してください。あなたはロボットが最高の結果を出せるようにしたい一方で、壁に衝突したりボールを落としたりといった危険な行動を絶対にさせないようにする必要があります。コンピュータサイエンスの世界では、これは「シールド合成（shield synthesis）」と呼ばれます。シールドを、単なる金属の板としてではなく、ロボットのすぐ横に立つ厳格なセーフティコーチ（安全指導員）として考えてみてください。もしロボットが災難を招くような動きをしようとしたら、コーチが介入して、「ダメだよ！そんなのはやめて。代わりにこの安全な動きを試しなさい」と言います。これは、風に反応して跳ねるボールや、電気を扱う回路のように、ルールが絶えず変化する複雑なシステムにおいて非常に重要です。課題は、これらのシステムには無限の可能性があるため、あらゆる状況における「安全な動き」と「不安全な動き」の完璧なリストを書き出すことが極めて困難であることです。

ここで、論文「Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems」が登場します。デンマークの研究チームは、これらトリッキーな混合システム（速度のような滑らかで連続的な変化と、スイッチのオン・オフのような突然のデジタル的なジャンプが混ざり合っているため「ハイブリッドシステム」と呼ばれます）のための、超スマートなセーフティコーチとなる新しいツール「Uppuall Coshy」を開発しました。彼らの大きなアイデアは、まず起こりうる状況の全宇宙を、小さな箱の巨大なグリッド（格子）に分割することです。そして、何千回ものシミュレーションを実行して、どの箱が安全で、どの箱が危険であるかを判断し、許可された動きの膨大なマップを作成します。しかし、このマップはあまりにも巨大になりすぎて、保存したり使用したりすることが不可能です。そこで彼らは、「Caap」（親しみやすいロボットの名前のような響きです）と呼ばれる巧妙なアルゴリズムを考案しました。Caapは、この巨大で乱雑なマップを取り込み、簡潔な決定木へと凝縮します。これは、100ページの取扱説明書をシンプルなフローチャートに変えるようなものです。彼らはこの手法を跳ねるボールのモデルでテストし、安全性を損なうことなく、安全ルールを数千倍にまで縮小できることを発見しました。これにより、これらの安全コーチを実際のデバイスに搭載することが可能になります。

跳ねるボールとセーフティコーチの物語

私たちがよく知るキャラクター、跳ねるボールを例に、この物語の核心に触れてみましょう。ボールが上下に跳ねている様子を想像してください。人間プレイヤーは、ボールを打ち続けて動かし続けることができますが、もし強く打ちすぎたり、タイミングが悪かったりすると、ボールは空高く飛んでいってしまうか、あるいは跳ねるのを止めてしまうかもしれません。目標は、ボールが止まったりどこかへ飛んでいったりすることなく、永遠に跳ね続けさせることです。

昔は、安全に保つためにいつボールを打つべきかを正確に判断するのは悪夢のような作業でした。ボールの位置と速度は滑らかに、かつ連続的に変化するため、どの瞬間においても、ボールが存在しうる場所は無限にあります。研究者たちは、この問題を解決するために「Uppaal Coshy」というツールを使用しました。彼らはボールの世界を巨大なチェス盤のように扱いました。ボールが存在しうる空間を、何百万もの小さな長方形の箱に細かく切り分けたのです。各ボックスに対して、ツールは単純な問いを投げかけます。「もしボールがこの箱の中にいたら、どのような動きが安全か？」

これに答えるために、ツールはただ推測したわけではありません。ゲームを何度も何度も繰り返しました。ボックス内の一点を選び、ボールの跳ね方をシミュレートし、それがどこに着地するかを見守りました。もしボールが「安全な」ボックスに着地すれば、その動きは良しとされました。もし「危険な」ボックス（例えば、ボールが止まってしまうボックス）に着地すれば、その動きは禁止されました。ボールの挙動には多少のランダム性（床がデコボコしていたり、ヒットが完璧でなかったりするなど）があるため、ツールは確信を持つためにこれらのシミュレーションを何度も実行しました。さらに、ボールが跳ねすぎて「ボード」の外に出てしまう可能性も考慮しなければなりませんでした。ツールは、特別な「境界外（アウトオブバウンズ）」ゾーンを作成し、シミュレーションの結果に基づいて、ボードの外に出ることが安全であるかどうかを判断することで、これに対処しました。

巨大なマップの問題

ここで物語は行き詰まります。グリッドがあまりにも細かかったため（精度を非常に高く保つため）、ツールは膨大なルールのリストを作成してしまいました。跳ねるボールの例では、初期の安全マップには、それぞれ独自のルールを持つ143万個以上の小さなボックスが存在していました。これほど大きなリストを保存することは、バックパックの中に図書館を持ち歩こうとするようなものであり、実際のロボットが使用するには重すぎるのです。

研究者たちは興味深いことに気づきました。隣り合う多くのボックスは、全く同じルールを持っているのです。もしボールがあるボックスにいて、そこでのヒットが安全であれば、そのすぐ隣のボックスにいるボールにとっても、ヒットはおそらく安全なはずです。ですから、何百万もの細かいルールを保持する代わりに、それらをグループ化してはどうでしょうか？

入場：Caap — 魔法の圧縮機

ここで、彼らの新しいアルゴリズムである「Caap」が登場します。Caapを、巨大で乱雑なマップを見つめ、「おい、この500個のボックスはすべて『ボールを打て』と言っている。これらを一つの大きなゾーンに統合しよう」と言う魔法のエディターだと考えてください。Caapは、パターンを探し、隣接するボックスをより大きな長方形の領域へと統合していくことで、これを行います。ただし、ルールが変わらない場合に限ります。

その結果、決定木が出来上がります。フローチャートを想像してください。「ボールは高い位置にあるか？ はい。速度は速いか？ いいえ。ならば、打て。」 このツリーは、元の百万個のボックスのマップよりもはるかに小さく、読みやすいものです。テストにおいて、Caapは跳ねるボールの安全ルールを、1,430,000個の小さなセルから、わずか2,972個の領域へと縮小することに成功しました。これは驚異的な削減です！まるで1,000ページの小説を、全く同じ物語を伝える20ページのコミックに変えるようなものです。

それは本当に機能するのか？

チームは単にマップを小さくしただけではありません。それが正しく機能することも確認しました。彼らはこの新しいコンパクトなシールドを跳ねるボールのテストに使用しました。彼らは、この新しい圧縮されたセーフティコーチによって制御されたボールを用いて、10,000回のシミュレーションを実行しました。結果はどうだったでしょうか？これら10,000回の試行の中で、ボールが跳ねるのを止めたり、どこかへ飛んでいったりすることは一度もありませんでした。ルールが今やポストカードに収まるほど小さくなっていたにもかかわらず、安全性は完璧に維持されていたのです。

また、彼らはこのセーフティコーチを使って、ロボットに「より良く」動く方法を教えることもできることを示しました。まず、ロボットが効率的に（エネルギーを最小限に抑えて）ボールを打つ方法を学習させ、その間、シールドが監視役として危険なミスを防ぐようにしました。ロボットは、非常に少ない回数のヒットでボールを空中に保持することを学習しました。これは、安全性と効率性の両立が可能であることを証明しています。

なぜこれが重要なのか

この論文は、単なる跳ねるボールの話ではありません。同じ数学的原理は、電圧を一定に保つ必要がある電気回路（ブーストコンバータ）や、溢れることを避けなければならない水槽など、現実世界の様々なものに適用できます。研究者たちはこれらのモデルについてもツールをテストしましたが、あらゆるケースにおいて、Caapアルゴリズムは安全性を保ちながら、安全ルールを劇的に（時には数百万のルールを数十個にまで）縮小することに成功しました。

Uppaal Coshyの素晴らしさは、それが完全に自動化されている点にあります。数学の天才である必要はありません。システムを記述するだけで、ツールが安全ルールを導き出し、圧縮し、日常的に使用するデバイスで実行可能なコンパクトなシールドを提供してくれるのです。これは、将来のスマートなロボットや自動化システムが、スマートであるだけでなく、安全で信頼性が高く、かつ私たちが日々使うデバイス上で動作できるほど軽量であることを保証するための、大きな一歩なのです。