Verification of High-Order Control Barrier Functions by Computing Class K Functions

あなたは、街中を駆け抜ける配送ドローンの艦隊をプログラミングしていると想像してください。ドローンには素早さと効率の良さが求められますが、何よりも重要なのは、建物や他のドローン、あるいは人々に決して衝突しないことです。ロボティクスやエンジニアリングの世界において、これは「安全性」という名の聖杯です。科学者たちは、制御バリア関数（CBF）と呼ばれる数学的ツールを使用して、ロボットの周囲に目に見えない「力場」を作ります。この力場は、ロボットのコンピュータに対して、「この方向に進めば安全だが、あちらへ行けば危険だ」と教えてくれるのです。

しかし、厄介な問題があります。時として、ロボットの物理特性は複雑になります。ブレーキを踏んでから停止するまでに数秒かかったり、停止するために旋回が必要だったりすることがあります。ここで「高次（High-Order）」CBFが登場します。これらは、こうした遅延や複雑な動きを考慮した、より洗練されたバージョンの力場です。しかし問題は、この力場を機能させるために、エンジニアは安全ルールの厳格さを定義する「クラスK関数」と呼ばれる特定の数学的な曲線を選ばなければならないということです。間違った曲線を選ぶことは、速度制限の設定ミスのようなものです。制限が高すぎれば衝突し、低すぎればロボットが身動き取れなくなってしまいます。長い間、エンジニアはこれらの数値を推測して、もしもの時に命や高価な機器が失われるリスクを承知で、うまくいくことを願いながら設定してきました。

「Computing Class K Functions for Verification of High-Order Control Barrier Functions」と題されたこの論文は、その「推測するゲーム」に正面から取り組んでいます。著者であるエリー・ポンドとマシュー・T・ヘイルは、ロボットがガレージを出る前に、その安全ルールが実際に機能することを数学的に証明する新しい方法を提案しています。単に曲線を推測するのではなく、彼らは「平方和（Sum-of-Squares/SOS）プログラミング」という強力な数学的手法を用いて、完璧な安全曲線を自動的に計算します。これは、設計図を描くだけでなく、レンガを一つ積み上げる前に、建物が崩壊しないことを証明するために千回のコンピュータ・シミュレーションを実行する熟練の建築家のようなものです。

この論文は、もし彼らの数学的なレシピが解を見つけ出したならば、ロボットがどのように動き、どのような障害物に直面しようとも、安全であることが保証されることを示しています。彼らは、ユニサイクルのようなロボットが7つの異なる安全ゾーン（例えば、7つの異なる円を回避し、かつボックス内に留まること）をナビゲートするシミュレーションを用いて、このアイデアをテストしました。コンピュータは、7つのゾーンすべてに対して必要な安全曲線を一度に生成することに成功し、ロボットは安全ルールを一度も破ることなくシミュレーションの中を駆け抜けました。これはコンピュータ上のシミュレーションであり、実際の街路を走る実機のロボットではありませんでしたが、背後にある数学は堅実であり、複数のルールを同時に遵守しなければならない複雑なシステムに対して、信頼できる検証方法を提供しています。

目に見えない力場

なぜこれがこれほど重要なのかを理解するために、この論文が使用しているツールを見てみましょう。ロボットを高速道路を走る車だと想像してください。標準的な安全ルールは「車線を守れ」というものです。数学的には、これは単純な直線です。しかし、もし車が重く、停止するのに時間がかかる場合はどうでしょう？ 単純な直線では不十分です。「端に近づいたら、後で滑り出さないように『今すぐ』減速しなければならない」というルールが必要です。これが**高次制御バリア関数（HOCBF）**が行うことです。これは、ロボットの慣性や反応にかかる時間を考慮して、先読みを行う安全ルールです。

しかし、この「先読み」ルールを機能させるためには、エンジニアは「クラスK関数」として知られる特定の形状を選択しなければなりません。煙探知機の感度を設定することを想像してみてください。感度を高く設定しすぎると、トーストを焼いているだけでアラームが鳴ります（ロボットが不必要に停止します）。逆に感度を低くしすぎると、家が燃え上がるまで作動しません（ロボットが衝突します）。長い間、エンジニアはこれらの「感度のつまみ」を手動で選ぶ必要があり、多くの場合、推測と試行錯誤に頼っていました。もし推測を誤れば、ロボットが身動き取れなくなるか、あるいは最悪の場合、コンピュータが経路を見つけられずクラッシュしてしまうこともありました。

安全のための「魔法の計算機」

この論文の著者たちは、推測する代わりに、完璧な「つまみ」を計算する数学的なトリックが使えることに気づきました。彼らは平方和（Sum-of-Squares/SOS）プログラミングと呼ばれる手法を使用しました。SOSプログラミングは、ある形状が常に「正（安全）」か、あるいは「負（危険）」かをチェックする、非常に賢い計算機のようなものだと考えることができます。

この論文の主な発見は、この計算機を使用して、複数の安全ルールを持つロボットのための適切なクラスK関数を見つけ出すステップ・バイ・ステップのレシピ（アルゴリズム）です。そのプロセスは以下の通りです：

1. 問題点: 彼らは、同時に従うべき7つの異なる安全ルール（HOCBF）を持つロボットを扱いました。各ルールには、解くべき未知の「感度のつまみ」（クラスK関数）が存在します。合計で14個の未知の関数（7つのルールそれぞれに対して2つずつ）があります。
2. 解決策: 彼らは一連の数学的問題を構築しました。まず、最初の層の安全性を解き、次にその結果を使って次の層を解く、という手順を踏みます。これは、最初のブロックが安定していることが証明されるまで、二番目のブロックを置くことができないブロックの塔を積み上げるようなものです。
3. 結果: コンピュータは、14個の未知の関数のすべてに対して、値を算出することに成功しました。

シミュレーション・テスト

彼らの魔法のレシピが実際に機能するかを確認するため、シミュレーションを実施しました。彼らはユニサイクルのような見た目をした仮想のロボット（位置、速度、角度を持つ）を作成しました。そして、以下の7つの異なる安全ゾーンを備えた遊び場を設定しました：

• 3つのゾーンは、ロボットが回避すべき目に見えない円のようなものです。
• 4つのゾーンは、ロボットが中に留まっていなければならない部屋の壁です。

さらに、目標も追加しました。ロボットは特定の場所に移動して停止する必要があります（これは「制御リアプノフ関数（CLF）」と呼ばれ、ロボットを目的地へと引き寄せる磁石のような役割を果たします）。

コンピュータは数学的レシピを実行し、安全曲線を生成しました。その後、ロボットを走行させました。論文の図に示されている結果は、成功でした。ロボットは様々な場所から出発して走行しましたが、毎回必ず、安全ゾーン（7つのルールすべてが重なる領域）の中に留まりました。図中の赤い点線は境界を示しており、ロボットの経路がそれらを越えることは一度もありませんでした。

これが意味すること（および意味しないこと）

この論文は、もし数学的問題に解が存在すれば、ロボットが安全であることが保証されることを証明しています。それは「安全の証明書」です。コンピュータが「はい、曲線を見つけました」と言えば、安全設定の不備によってロボットが衝突することはないと断言できます。

しかし、留意すべき重要な制限がいくつかあります。この論文は、システムが多項式（特定の種類の滑らかな曲線）として記述できる場合にのみ、この手法が機能することを明記しています。現実世界のシステムの多くはこの方法で近似可能ですが、これは数学的な要件です。また、ここで示された結果はシミュレーションです。ロボットはコンピュータ画面上にしか存在しません。著者らは、実機のロボットや実際の街路でこれをテストしたわけではありません。

さらに、論文では、数学が複雑になりすぎて解けなくなる場合があることも指摘しています。コンピュータが解を見つけられない場合、それは必ずしもロボットが安全であり得ないことを意味するのではなく、単に彼らが用いた特定の数学的ツールが、その特定の課題に対して十分に強力ではなかっただけかもしれません。そのような場合には、数学的なアプローチを調整する（例えば、曲線をより単純にするなど）ことで、再試行することを提案しています。

シミュレーションにおいて、コンピュータが7つのルールすべてを統合して検証にかかった時間は、約1,053秒（約17分）でした。これは、数学的な負荷は高いものの、実行可能であることを示しています。著者らは、安全ルールを追加するにつれて、問題を解くのにかかる時間が直線的に増加することを発見しました。これは、将来のより複雑なロボットに向けた良い兆候です。

結論

この論文は、新しいロボットや新しい運転方法を発明したわけではありません。代わりに、ロボットの安全を守るための**「数学のチェック方法」**を新たに発明したのです。以前は、エンジニアは安全設定が正しいことを「願う」しかありませんでした。しかし今や、彼らには、たとえロボットが7つの異なる安全ルールを同時に処理しなければならない状況であっても、「はい、これらの設定はロボットを安全に保ちます」と数学的に証明できるツールがあります。これは、推測と試行錯誤のゲームを、証明と確信のゲームへと変え、将来のより安全で信頼性の高い自律型機械への道を切り拓くものです。