制約プログラミングに関する卒業論文

概要

情報理工学の学部生として取り組んだ研究は、実際的な問いから始まっている——シミュレータが起こりうる条件を大量に抱え込んだとき、もはや起こりえない条件を考え直すのを、どうすればやめさせられるか。値が変化していく向きを手がかりに、不要になった条件を探索から取り除く手法をHydLa向けに設計し、実装して評価した。ベンチマークとして用いたモデルでは、シミュレーション全体の所要時間がおよそ半分に減った。

この研究は、いまの私のデザイン哲学の最初の土台にあたる。複雑な結果は、必ずしも直接指定しなくてよい——規則と優先度と境界を注意深く定義した空間から、立ち上がってくることがある。制約プログラミングが教えてくれたのはそれだった。その考え方が、AIの時代に制約からデザインするという私の姿勢、すなわち生成システムが自由に振る舞える条件をデザインするという姿勢につながっている。

要旨

HydLaは、ハイブリッドシステム——連続的な変化と離散的な事象が互いに影響し合うシステム——のためのモデリング言語である。制約に基づく設計により、そうしたシステムを簡潔に記述し、高い精度でシミュレートできる。その代償として、モデルが大きくなると、すでに無関係になった条件規則までシミュレータが延々と検査し続けることになる。

本研究は、そのガード付き制約を実行中に削減することを提案した。単調な振る舞い——値が一方向に動き続けること——を認識できれば、シミュレータは特定のガードが将来にわたって真になりえないと判定し、安全に検査をやめられる。同じ形のガードを持つ対象が多数含まれるモデルで特に効果が大きく、実測した実行時間は元の約半分まで下がった。

1. はじめに

ハイブリッドシステムは、連続的な振る舞いと離散的な事象を併せ持つ。跳ねるボールが単純な例だ。空中にあるあいだは位置と速度が連続的に変化するが、面に当たった瞬間に離散的な事象が生じ、進む向きが変わる。サーモスタット、自動車、ロボットは、いずれも同じ混ざり方を、より重大な形で内側に抱えている。

HydLaでは、こうしたシステムを一本の手続きとして書き下すのではなく、数学的・論理的な制約として記述できる。シミュレータのHyLaGIは丸め誤差のない記号計算を行え、値の定まらないパラメータも扱える。ただし、この記述力の高さは規模の問題を生む。特定の条件下でのみ有効になる規則が数多く含まれるモデルでは、シミュレータはそのそれぞれについて「次に起こるのはこれか」を繰り返し問わなければならない。

2. シミュレーションにおけるガード付き制約

ガード付き制約とは、ガード条件が満たされたときにだけ有効になる規則である。上のベンチマークでは、面の区画ごとに固有の規則がある——ボールの高さが0に達したとき、その水平位置がその区画の内側にあれば、跳ね返りの規則が適用される。したがって面を細かく分割すれば、シミュレータが調べるべきガードもそれだけ増える。

実験では区画数を10から200まで変化させた。元のシミュレータは、およそその数の二乗に比例して遅くなった。これは作り物の例にとどまる話ではない。規模の大きなモデルでは、多数の物体、接触の領域、起こりうる事象が、まさにこのガード付きの形で表される。

3. ボトルネックの所在

プロファイリングにより、この遅さがシミュレータ全体に均等に散らばっているのではないことがわかった。面の区画を100個にしたとき、実測した実行時間の96%がFindMinTime——次に起こりうる最も早い事象を探す処理——に費やされていた。そこで、候補となる制約すべてのガードが繰り返し評価されていた。

この結果は、最適化の的を具体的にした。シミュレートされる振る舞いをまったく変えないまま、FindMinTimeが考慮しなければならないガードの数を減らすことである。

4. ガード付き制約の削減

階段を跳ねながら下っていくボールを思い描いてほしい。ボールがある段を通り過ぎ、そのまま前へ進み続けるなら、その段はもうボールに影響しえない。図を見た人間は、ボールの後ろにある段をただちに無視する。元のアルゴリズムは、その一つ一つを検査し続けていた。

難しいのは、取り除いたガードが後になって必要にならないことを示す側だ。いま偽だからという理由だけで取り除けば、それが再び真になったとき、誤った結果を黙って返しかねない。そこで提案手法は単調性を使う——ある変数が、ある時間区間にわたって増加し続ける、あるいは減少し続けると保証できるかどうかである。

4.1 一様な単調性への対応

一つ目の対応は、変数がシミュレーション全体を通じて一方向に動く場合にあてはまる。面を分割したモデルでは、ボールの水平位置はつねに増加する。ある区画を越えて進んでしまえば、その区画の条件は二度と満たされない。この性質はモデル検査の技術によってシミュレーション前に確かめられるので、実行が進むにつれて不要になったガードを、安全に取り除いていける。

4.2 交替する単調性への対応

現実のシステムの多くは、いつまでも一方向に動くわけではない。変数は増加し、向きを変え、そして減少しうる。そこで論文は二つ目の対応を示した。まず向きを仮定し、その仮定をアサーションで監視し、向きが変わった時点から削減の処理をやり直す。一つの単調な区間のために取り除いたガードは、次の区間が始まるときに戻される。

5. 実験結果

一様な単調性への対応を実装し、面を分割したモデルで評価した。元のアルゴリズムも提案手法も、区画数が増えれば所要時間は伸びる。ただし提案手法のほうが、一貫して仕事量が少なかった。当てはめた曲線を比べると、最高次の係数は1.1463から0.6083へ下がり、このベンチマークではシミュレーション全体の所要時間がおよそ半分になった。

これは、あらゆるHydLaのモデルが二倍速くなるという主張ではない。示しているのは、この手法が効く場所である——ガードを持つ対象が多く、変化の向きが証明でき、実行中にガードが恒久的に無関係になっていくようなモデルだ。

6. 結論と今後の課題

この研究が示したのは、低水準の計算を速くすることだけでなく、モデルについての知識がシミュレーションを効率化しうるということである。単調性を使って、どの可能性がすでに起こりえなくなったかを認識することで、HyLaGIは結果を変えずに、有効な制約の集合を小さくできる。

実装して確かめたのは、一様な単調性の側である。論文は今後の課題として二つの方向を残した。交替する振る舞いに対するアサーションに基づく手法の評価と、単調性以外の不変な性質を使って、安全に取り除ける制約をさらに見つけ出すことである。