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

概要

シミュレータは、起こりうる出来事が増えるほど、多くの条件を繰り返し調べる。では、進行状況から「この条件はもう二度と成立しない」と判断できるなら、その検査を安全にやめられないか。値の変化する向きを手がかりに、不要になった条件を実行中の探索から外す手法を、ハイブリッドシステムのモデリング言語HydLa向けに設計・実装した。

評価モデルでは、シミュレーション結果を変えずに、実行時間を従来のおよそ半分まで短縮した。重要なのは、すべての計算を一様に速くしたことではない。問題の構造を使って、考慮すべき可能性そのものを減らしたことである。

この研究で学んだ制約型プログラミングの考え方は、現在の私のデザイン哲学の土台になっている。結果を一つずつ直接指定するのではなく、規則、優先度、境界を定義し、その内側から成立する解を導くという姿勢である。

課題 —— 可能性が増えるほど、計算が遅くなる

HydLaは、連続的な変化と離散的な出来事が組み合わさる「ハイブリッドシステム」を、数学的・論理的な制約として記述するための言語である。手続きの順番をすべて書かなくても、何が成立すべきかを宣言することで、条件を満たす振る舞いをシミュレーションできる。

一方、条件に応じて有効になる規則が多いモデルでは、シミュレータは大量の候補を繰り返し検査する。すでに通り過ぎ、将来も成立しない条件まで候補に残り続けるため、モデルが大きくなるほど不要な計算が積み上がっていた。

題材 —— 連続と離散が混ざるシステム

跳ねるボールは、ハイブリッドシステムのわかりやすい例である。空中では位置と速度が連続的に変わり、床へ当たった瞬間には、跳ね返るという離散的な出来事が起きる。サーモスタット、自動車、ロボットも、規模は違っても同じ二種類の変化を内側に持つ。

評価には、水平に進むボールが、複数の区画に分かれた面で跳ね返るモデルを使った。面の区画ごとに「ボールがこの範囲へ来たら跳ね返る」という条件付きの規則がある。区画を増やせば、表現できる対象が増える一方、シミュレータが調べる条件も増える。

ボトルネック —— 条件の数が計算量を押し上げる

条件が満たされたときだけ有効になる規則を「ガード付き制約」と呼ぶ。評価モデルでは、ボールが床へ到達し、その水平位置が特定の区画内にあるときだけ、その区画の跳ね返り規則が有効になる。

区画数を10から200まで増やすと、従来のシミュレータはおよそ区画数の二乗に比例して遅くなった。規模の大きなモデルでは、物体、接触領域、起こりうる出来事が増えるため、同じ問題がより大きくなる。

調査 —— 処理時間の96%はどこにあったか

処理時間を計測すると、区画数100のモデルでは、全体の96%がFindMinTimeに使われていた。これは、候補の中から「次に起こる最も早い出来事」を探す処理である。そこで、すべてのガード条件が繰り返し評価されていた。

改善すべき場所は明確になった。計算方法全体を作り直すのではなく、FindMinTimeへ渡す候補を、安全に減らせばよい。シミュレーション結果を変えず、調べる必要のない可能性だけを外すことを目標にした。

アプローチ —— 二度と成立しない条件を安全に外す

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

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

変化の向きが変わらない場合

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

変化の向きが途中で変わる場合

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

結果 —— 評価モデルの実行時間を約半分に

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

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

この研究から得た視点

この研究で行ったのは、個々の計算を少しずつ速くすることではない。システムの振る舞いについてわかっていることを使い、考慮すべき可能性の集合を小さくすることだった。結果を変えずに探索空間を狭めるという考え方が、制約型プログラミングの強みである。

実装・評価したのは、変数が一方向に動き続ける場合である。変化の向きが途中で変わる場合は設計までにとどまり、評価は今後の課題として残った。単調性以外の性質を使い、不要な制約をさらに見つける余地もある。

現在の私が、AIの出力を直接デザインするのではなく、AIが探索できる条件や境界をデザインしようとするのも、この経験につながっている。複雑な結果を扱うとき、何を計算するかと同じくらい、何を考えなくてよいかを定義することが重要である。