Learning GR(1) Specifications from Traces

ロボットにどのように振る舞うべきかを教えようとしていると想像してください。しかし、ルールが何であるかを知らないため、ルールを書き記すことができません。代わりに、ロボットを記録しているビデオカメラがあります。あなたは、カメラに対して、ロボットが素晴らしい仕事をしたクリップ（「良い」トレース）の集まりと、ロボットが衝突したり奇妙な動きをしたりしたクリップ（「悪い」トレース）の集まりを見せます。あなたの目標は、良いクリップと悪いクリップを完璧に分けるルールブックを書くことです。これが**仕様マイニング（specification mining）**の世界です。つまり、データの中から隠された法則を掘り起こす作業です。

しかし、落とし穴があります。現実世界では、自動運転車や工場のロボットのようなシステムは、単にルールに従うだけではありません。彼らは周囲の環境に反応します。もし環境（雨の降る道路や、ボタンを押す人間など）が何かを行えば、システムはそれに応答しなければなりません。これは**リアクティブ・システム（reactive system）と呼ばれます。これらのシステムを安全にするために、コンピュータ科学者はGR(1)**と呼ばれる特殊な論理を使用します。GR(1)を、厳格な契約だと考えてください。「もし環境が善良に振る舞うことを約束するなら（仮定）、システムは自分の役割を果たすことを約束する（保証）」という契約です。もしこの契約を正しく結べれば、数学的に動作が保証されたロボットを自動的に構築できます。もし間違えると、ロボットは失敗するか、あるいは最悪の場合、ロボットが作れるはずなのに、数学的には不可能であると判定されてしまいます。

問題は、正しい契約を見つけるのが難しいことです。既存のツールは、論理の言語におけるあらゆる可能な文章を調べることで、ルールを推測しようとすることがよくあります。これは、宇宙にあるすべての藁（わら）を一つずつチェックして、特定の針を探そうとするようなものです。これでは永遠に時間がかかりますし、ツールが「見た目はまともだが、実は罠のようなルール」を提示することもあります。つまり、良いクリップと悪いクリップを分けることはできても、実際のロボットが到底従うことのできないルールを提示してしまうのです。

ここで、この論文が登場します。サム・ニコラス・クテイリとそのチーム率いる研究者たちは、GR1MINEと呼ばれる新しいツールを構築しました。GR1MINEは、ランダムに推測するのではなく、あらかじめ契約の形を知っています。それは、GR(1)ルールの骨組み、すなわち「もし環境がXをするなら、システムはYをしなければならない」という構造です。ツールは、XとYが実際に何であるかを解明するだけでよいのです。

これを行うために、彼らは「SATソルバー」を用いた巧妙なトリックを使用しました。これは、超高速のパズル解決器のようなものです。あなたがレゴのお城を作ろうとしているとしますが、どのブロックを使えばよいか分かりません。そのとき、お城全体を組み立ててはテストし、また壊してやり直すということを繰り返すのではなく、GR1MINEはまずお城の「フレーム（枠組み）」を一度作ります。そして、そのフレームの中にさまざまなブロックの組み合わせを試していきます。もしある組み合わせが失敗した場合、ソルバーはその失敗の「理由」を記憶し、それを利用して、他の何千もの不適切な組み合わせを瞬時にスキップします。これは「増分解決（incremental solving）」と呼ばれます。

チームは、実世界のハードウェアやロボティクスの課題から取られた120種類の異なるパズル（ベンチマーク）を用いて、このツールをテストしました。結果は驚くべきものでした。パズルが標準的なGR(1)ルールで構成されている場合、GR1MINEは60個すべてを解きました。対照的に、従来の最高レベルのツールは、それらの半分か3分の1程度しか解けませんでした。さらに印象的なことに、特定のパズルにおいて、GR1MINEは汎用的なツールよりも30倍以上速かったのです。

しかし、本当の魔法は、パズルが完璧なGR(1)ルールではなかった場合に起こりました。元のルールが乱雑で、整然としたテンプレートに適合しない場合でも、GR1MINEは60個中38個のケースにおいて、機能する「実現可能（realizable）」なルールを見つけ出すことに成功しました。他のツールは苦戦し、見つけたルールも極めて少なく、また、それらは「実現不可能（unrealizable）」、つまり数学的にロボットが従うことが不可能なルールであることが多かったのです。

要するに、GR1MINEは単に「良いもの」と「悪いもの」を分けるルールを見つけるのではありません。ロボットが実際に生きていくためのルールを見つけるのです。GR(1)の既知の構造に従い、作業の重複を避けるためのスマートな記憶トリックを用いることで、チームは、以前よりもはるかに速く、かつ確実に、複雑で安全な契約を自動的に発見できることを示しました。彼らは単に、干し草の山の中から針を見つけたのではありません。正しい種類の針だけを引き寄せる磁石を作り上げたのです。