タグ: 機械学習

制御系の検証を強化学習を用いて行う

~ yoriyuki

今日はFalsification of Cyber-Physical Systems Using Deep Reinforcement Learning(arXiv版)という私が共著した論文を紹介する。今年のFM（形式検証の国際会議）で発表されたショートペーパーだ。内容は、制御系の検証（必要な性質を満たしているか確かめること）を強化学習を使って行うというものだ。

制御系の検証は難しい。まず、制御の対象は普通物理系なので、微分方程式を解かないといけない。もちろん微分方程式を調べるにはいっぱい数学の理論があって、それを使えば良いわけだが、難しいのは今どきの制御系は往々にしてデジタルだ、ということだ。離散的にモードが変化したりする。こういう離散系と微分方程式が混ざったシステムはハイブリッドシステムと言われるが、解くのがとても難しい。

ハイブリッドシステムを検証する方法だが、完全な検証はごく単純なものしかできず、また計算も大変であることが分かっている。というわけで、普通にテストするしかないわけだが、複雑なシステムだとテストをデザインするのは難しいし、欠陥を見落としてしまうかもしれない。

そこで、自動的にテストを生成することが考えられる。特に、与えられた性質をシステムが満たさないことを示すテスト（反例）を探索することをFalsificationと呼ぶ。今回紹介する論文は、Falsificationを深層強化学習を用いてする手法を開発し、ベンチマークを行った研究である。

ロバストネスによる反例発見

いくつかの性質を考えよう。一つは安全性だ。出力の適当な不等式で書ける性質Pについて、「つねにPが成り立つ」が安全性だ。

ロバストネスによる反例発見とは、これらの性質にロバストネスという数値を定義し、ロバストネスを最小にするような入力を探索することにより反例を見つける手法だ。ロバストネスは、性質がどれだけロバストに成り立つかを表す数値で、マイナスになるとその性質は成り立たないように定義する。

例えば、Pを単純にy \leq cとする。ここでyは出力、cはある定数とする。このとき、Pについての安全性は\min c - yと定義される。定義から分かるように、ある時点でyがcを上回れば、ロバストネスはマイナスになる。

本当は安全性だけでなく、任意のMTL(Metric Temporal Logic)という論理式で書ける性質についてロバストネスが定義できるが、複雑になるので説明はしない。

いろいろな最適化技法（たとえば焼きなまし法）を用いてロバストネスを最小化する入力を探索する手法が、 Robustness guided falsificationだ。これまでいろいろな研究が行われてきたが、残念ながらまだ実用的な技術とは言えないだろう。一つの理由は、最適化の1ステップごとにシステム全体を最初から最後まで実行する必要があり、計算時間がかかってしまうからだ。他に、局所最適解に落ち込みがちという問題もある。

強化学習によるロバストネス最小化

そこで、最適化に強化学習を用いることを考える。強化学習はオンラインで、つまりシステムの実行が途中の状態で、学習を進め最適な解に近づくような入力を生成できるからだ。

しかし、問題がある。強化学習は\gammaは割引き率、r_iは時刻iでの利得とすると、

\sum \gamma^i r_i

の期待値を最大化しようとする。一方、ロバストネスは最小値により定義されており、合計ではない。

そこで、次のような近似を用いる。

\max (a_1, \ldots, a_n) \sim \log \sum_{i = 0}^n e^{a_i}

この近似を用いると、

\min c - y = - \max -(c - y) \sim - \log \sum e^{-(c-y)}

と書けるので、

\sum e^{-(c-y)}

を最大化すればよいが、これはe^{-(c-y)}を利得とする強化学習問題になっている。

実装と実験

実装は制御系のシミュレーションをMATLAB/Simulinkで、強化学習の実装はChainerRLを用いており、全体をPythonのスクリプトで結合している。対象にした制御系はHoxhaらの論文にあるものを用いている。(S-Taliroに付いてくる）。強化学習アルゴリズムはA3CとDDQN+NAFを用いた。

実験は9つの性質についてA3C, DDQNと比較対象としてS-TaLiroに実装されているSA（Simulated Annealing, 焼きなまし法）とCE（Cross Entropy法、クロスエントロピー法）を用いて実験を行った。それぞれの方法について、対象の系のシミュレーションを最大200回まで行ってよいこととし、200回シミュレーションを行っても反例が見つからなければ実験を打ち切ることとした。これを20回を繰り返し、200回以内に反例を発見できた割合(Success rate)と反例発見に要した回数の中央値(numEpisode)を求めた。また、入力データをどれくらいに時間刻みで変化させるかで違った結果が出るため、シミュレーション中の時間で1秒、5秒、10秒と時間刻みを変化させて実験をし、Success rateが最も良いもの、それで決まらなければnumEpisodeが良いものをそれぞれのアルゴリズム毎に選んだ。（ただし、実験によっては、1秒のものは何日かけても終わらなかったので省いてある）

実験結果を上の表に示す。ΔTは選ばれた時間刻みだ。横に示されたSuccess rateやnumEpisodeはベストなΔTのものである。黒字で示された数字は4つの手法間でベストなもの、*やがついた数字はベースラインと比較して（あるいは提案手法と比較して）差が有意である場合を示している。*はp < 0.05を、はp < 0.001を示している。

大雑把な傾向としては、強化学習の方が良い成績を収めていることが分かる。ただし、CEは性質によっては強化学習と匹敵するかそれを超える性能を出している。しかし、CEは性能が極端に悪い場合も多い。

課題

実は、強化学習を利用した実装は現状、大変遅い。ほとんどの実行時間がSimulinkのシミュレーターのものなので、これは強化学習の問題ではなく、PythonからSimulinkを呼ぶ方法に問題があるようだ。また、φ5のfalsificationが簡単すぎてバグがあるように見える。また、強化学習は生成した入力は階段関数になっているが、S-TaLiroはスプライン補間をしており、これは実験結果に影響があるかもしれない。

実装と実験データはこちらに公開されている。

https://www.dropbox.com/s/e1rxokcl8t7nw2c/RL.tar.bz2?dl=0