SMT制約式の機械学習を用いた自動チューニング

2019 Fiscal Year Research-status Report

• Project/Area Number: 19K20241
• Research Institution: Kitasato University
• Principal Investigator: 高野 保真 北里大学, 一般教育部, 講師 (70780550)
• Project Period (FY): 2019-04-01 – 2022-03-31
• Keywords: 制約ソルバ / 背景理論付きSAT / オートチューニング / 機械学習

Outline of Annual Research Achievements

「背景理論付きSAT」（以下、SMTと呼ぶ）という形式の制約式に対して、SMTソルバと呼ばれるソフトウェアを利用する際の求解時間に関して研究を進めている。具体的には、本研究は 1) SMTソルバの利用時に短かい求解時間が期待できる制約式のオートチューニング方法と、2) SMTソルバの選択方法の開発を目指している。大量の既存のベンチマーク制約式をSMTソルバに与えて事前に求解時間を蓄積しておき、その結果から機械学習モデルを作成し、その学習モデルを利用して求解時間を見積る。このことで、ソフトウェア・ハードウェアの検証に用いる制約式の求解時間の短縮に、統計的な手法が有効であるかを明らかにすることが目的となる。
本年度は、機械学習のための、制約式の特徴量の抽出方法について調査・検討した。SMTの制約式は一種のプログラムとして記述されるため、予約語や変数名を考慮して制約式の特徴量を抽出する必要があり、機械学習が成果を挙げている自然言語処理の手法をそのまま利用することはできないという仮定から研究をスタートした。
まずは、コンピュータが内部的に制約式を解釈した結果である「抽象構文木」に変換し、特徴量を抽出するような手法を検討した。この場合、制約式の文面上の違いを取り除いて制約の構造を扱うことができることが分かったが、あくまで静的な構造であるため求解時の挙動を表現していない点、機械学習時に絞るべき情報の選択に合理的な基準を定めることが難しそうな点という2点において、十分ではないと判断した。
そのため、SMTソルバのログ情報を用いること検討している。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

2019年度は、1) 学習に用いるベンチマーク制約式の収集、2) 制約式を機械学習の入力とするための特徴量の抽出方法の開発の2点を行う計画を立てた。
1) に関して、ベンチマーク制約式にはSMT-LIBベンチマークを用いて、ベンチマーク制約式を種々のSMTソルバで実行することで、学習に用いるデータの収集を行う予定であった。しかし、事前の研究 [高野ら、第35回日本ソフトウェア科学会大会、2018] で用いたデータを改めて検討した結果、そのまま使うことが可能であると判断した。このデータは、一般のコンピュータで求解時間がかかるものを抽出するために、Z3、CVC4、Yicesという3種類のSMTソルバでSMT-LIBの種々の制約式を実行したデータである。計測したコンピュータが若干古かったため再計測することを計画したが、研究の最終結果として得られるオートチューニングやSMTソルバ選択方法の対象が必ずしも最新のコンピュータだけではないと判断し、新たに収集せずにこの点に掛ける時間を短縮できると判断した。
2) に関して、「研究実績の概要」で述べた抽象構文木を用いる方法の検討に時間がかかった。結果、その方法は諦めSMTソルバのログ機能を利用する手法へ切り替えることに決めた。また、その調査の過程で、本研究の申請時には分かっていなかったSMTソルバに関するオートチューニング方法の関連研究 [Balunovicら、NeurIPS、2018] があることが分かった。この研究は、制約式の意味を替えない範囲で色々な変形を試すために機械学習を用いており、変形手法を参考にできる。
以上のことから、2) に想定以上の時間がかかったが、1) にかかるはずであった時間が削減できたため、全体としてはおおむね順調に進んでいる。

Strategy for Future Research Activity

「研究実績の概要」で述べたように、SMTソルバのログ情報を用いる手法の実装を進める予定である。具体的には、Z3というSMTソルバが出力するログ情報を利用する。ログ情報には、ある制約式の解を求める際の、Z3内の探索内容を記録しているため、より求解時間の実態を表現している。ここで抽象構文木を用いる場合と違って問題となるのは、求解が無限ループに落ち入り、解が得られないことがSMTソルバでは高い頻度で起きることである。
そのような問題に対しては、Z3のログ情報を用いたデバッグツール Axiom Profiler [Beckerら, TACAS2019] の手法を参照する。このツールは、制約式中で量化子を利用した際の求解時間の低下原因の調査のため、ログをグラフ化して表現するが，そのグラフと同様の構造を本研究の機械学習に用いる特徴量とすることが考えられる。なお、ログ情報は、SMTソルバの実装に依存してしまうため、本研究の「SMTソルバの選択方法の開発」には、対象とする各SMTソルバにログ機能が必要となり、そのままでは用いることができない。そのため、他のSMTソルバのログ機能についても調査し、SMT制約式とログの関連付けができるかなども検討する。
続いて、「現在までの進捗状況」で挙げた関連研究との比較を行う。その論文で出現数、抽象構文木、周辺に現れる語という3種類の制約式の機械学習時の特徴量の表現方法が検討しているため、本研究の比較相手として利用することができる。比較を可能とするため、本研究ではその論文で用いられている設定の機械学習手法を用いる。
以上の実装を2020年度中に完了し、2021年度は成果発表に当てる予定である。

Causes of Carryover

2019年度は、開発に用いるノート型パーソナルコンピュータと、機械学習のためのコンピュータに必要となる部品を購入したが、残りの額で購入が必要な物品がなかったため剰余金が発生してしまった。
2020年度の学会参加のための旅費に組み入れて利用する予定である。