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

今日は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

ソフトウェア工学に文句をつける

本稿ではソフトウェア工学の論文を1つ例として取り上げ、その内容に文句をつけたいと思う。取り上げる論文は、ソフトウェア工学の論文としてきちんとしたもので、ソフトウェア工学のトップ会議の一つであるISSTAで発表されたものである。

Milos Gligoric et al., Comparing non-adequate test suites using coverage criteria, ISSTA’13

PDF

論文の解説

ソフトウェアがちゃんとできているか、確かめるよくあるやり方はテストである。ソフトウェアにやってきそうな入力をいくつか用意し、実際にソフトウェアに入力してみる。そしてその結果をみて、ソフトウェアが期待通りに動くか確かめる。

ここで問題は、あらゆる可能な入力に対応するテストを用意することは、ほとんどの場合、不可能であるということだ。というのも、ソフトウェアが受け付ける入力の数は膨大なものになってしまうことが多いので。

というわけで、不完全なテストの「良さ」を評価するために「カバレッジ」という概念が登場する。ソフトウェアテストのカバレッジの概念は多数提案されていて、例えば

  • コードカバレッジ:テストによって実行されるコード(例えばプログラムの文)が全体のどれだけか。この論文ではステートメントカバレッジと呼んでいる。
  • ブランチカバレッジ:プログラムの中に含まれる分岐のうち、どれだけが実行されたか
  • パスカバレッジ:プログラムの中に含まれる実行パスがどれだけ実行されたか

などなど。これらのカバレッジ基準によって、テストが評価できる…わけだが、評価基準がたくさんあるので、評価基準自体の評価が必要になる。それをしましょう、というのがこの論文。ただし、カバレッジ基準が完全に満たされている(100%のとき)場合は先行研究があるので、基準が完全に満たされない場合を考えた、というのがこの論文の新しさ。カバレッジ基準が100%満たされることはめったにないので、この論文のやっていることは意義が大きい。

さて、どのようにカバレッジ基準の妥当性を評価するか。テストは究極的にはバグを見つけるためのものなので、そのテストがバグを発見できる確率とカバレッジ基準の達成度合いの相関を見る。バグは人為的にコードをランダムに変化させることにより生成する。テストによるランダムな生成によるバグの発見率と、人間が作るバグの発見率は、相関していることが知られているので、このような評価で問題ない。

さて、この論文の結論は本稿の目的とはあまり関係ないが、一応書いておくと、ブランチカバレッジが、他の複雑な基準を押しのけて、一番良い。ただし、テストが十分行える状況ではAIMP (acyclic intra-method paths)カバレッジという基準が良いらしい。

文句をつける

さて、この論文、動機づけも明確で良いし、実験もきちんと行われていて興味深い結論を引き出している。考察も示唆的だと思う。良い論文だと思う。

それでも文句をつけたくなる。

  1. 理論的な基盤の欠如:この論文の結論の正当化には、直感に訴えた議論はあっても理論的なものはない。
  2. 特定のデータセットやツールに依存している
  3. 特定の言語(Java)とプログラミングパラダイム(オブジェクト指向言語)に限定された研究である

ランダムなバグを検出するのにどのようなテストを行えばよいか、というのは原理的には純粋に理論的な課題なはず。もちろん実際は難しいかもしれないが、近似的な議論とか、なにかできないのだろうか。大量なデータを用いた経験的な研究を行うのが最近のソフトウェア工学研究のトレンドだが、理論的な正当化が不十分であるように思う。そして、理論的な正当化が不十分であるために、次に述べるように、結果の一般性に疑念が生じる。

2.は言いがかりのように聞こえるかもしれない。実験をする以上、何かのデータセットやツールに依存せざるを得ないのは明らかではないだろうか。しかし、ソフトウェア工学分野の研究では、比較を公平にするためもあるのだろうが、同じデータセットやツールが複数の研究で繰り返し用いられている。つまり、研究分野自体が特定のデータセットに過学習しかねないように思う。

さらに言えば、現在のソフトウェア工学のほとんどがJavaプログラムを対象にしている(CやC++が対象になることもある)。これは不健全な状況だと思う。別のプログラミング言語やパラダイムが主流になったとき、またすべての研究を一からやり直すのだろうか。

ではどうすればよいか

あまり大した提言はできないのだが、まず大量データを解析して経験的に結論を下すだけではなく、なぜそれが成り立つか、理論的な考察が必要だ。理論的な考察があって初めて、得られた結果が一般性を持つのかどうか、異なったプログラミングパラダイムに適応可能か、といったことが分かるはず。

もう一つは、Javaだけではなく、異なった言語・パラダイムの研究を行うべきだということ。静的型付けがあるのとないのとではどう違うか。型推論はどのような影響を与えるか。オブジェクト指向と関数型言語ではどう違うか。などなど。

まあ、お前がまずやれ、という話になりそうだが…