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

2020 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: 制約ソルバ / SMT / オートチューニング / 機械学習

Outline of Annual Research Achievements

「背景理論付きSAT」（以下、SMTと呼ぶ）という形式の制約式に対して、SMTソルバと呼ばれるソフトウェアを利用する際の求解時間に関して研究を進めている。具体的には、本研究は 1) SMTソルバの利用時に短かい求解時間が期待できる制約式のオートチューニング方法と、2) SMTソルバの選択方法の開発を目指している。学習モデルを作成し、その学習モデルを利用して求解時間を見積る。このことで、ソフトウェア・ハードウェアの検証に用いる制約式の求解時間の短縮に、統計的な手法が有効であるかを明らかにすることが目的となる。
2019年度に利用する時間がかかるSMT制約式を洗い出すことはできている。2019年度の研究開始時にはSMTの制約式を「抽象構文木」として扱う方法を検討したが、不十分と分かったため、2020年度は、Z3というSMTソルバが出力するログ情報を利用する手法について検討した。
ログ情報には、ある制約式の解を求める際の、Z3内の探索内容を記録しているため、より求解時間の実態を表現している。ログ情報を用いる場合には、求解が無限ループに落ち入り、解が得られないことがSMTソルバでは高い頻度で起きるため、対象とするSMT制約式のすべてに対してログ情報を得ることができない可能性がある。
そのような問題に対して、Z3のログ情報を用いたデバッグツール Axiom Profiler [Beckerら, TACAS2019] の手法を参照にしている。このツールは、制約式中で量化子を利用した際の求解時間の低下原因の調査のため、ログをグラフ化して表現するが，そのグラフと同様の構造を本研究の機械学習に用いる特徴量とすることが考えられる。

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

2019年度に対象とするSMT制約式を収集・決定し、2020年度は、研究実績の概要で述べたZ3のログ情報を用いる手法の確立を計画していた。
しかし、2020年度は本務校でのオンライン授業準備等に追われて研究の時間を十分に取ることができず、Axiom Profilerの論文の調査しか進められなかった。
ただ，Axiom Profilerの解析という具体的な進め方に目処は立っているため、遅れを取り戻すことはできると考えている。

Strategy for Future Research Activity

Axiom Profilerの手法を参考にZ3のログ情報を用いた特徴量の抽出手法を実装する。
なお、ログ情報は、SMTソルバの実装に依存してしまうため、本研究の「SMTソルバの選択方法の開発」には、対象とする各SMTソルバにログ機能が必要となり、そのままでは用いることができない。そのため、他のSMTソルバのログ機能についても調査し、SMT制約式とログの関連付けができるかなども検討する。
続いて、「現在までの進捗状況」で挙げた関連研究との比較を行う。その論文で出現数、抽象構文木、周辺に現れる語という3種類の制約式の機械学習時の特徴量の表現方法が検討しているため、本研究の比較相手として利用することができる。比較を可能とするため、本研究ではその論文で用いられている設定の機械学習手法を用いる。
2020年度中の計画が思うように進められなかったため、今年度中に実装、成果の国内・国際会議での対外発表を考えているが、スケジュール的に厳しいことも考えて、2022年度への研究期間延長も考えている。

Causes of Carryover

2020年度に本務校でのオンライン授業準備等に追われて研究の時間を十分に取ることができなかったため、本来予定していた国内会議発表に関する経費を使用しなかった。
次年度は発表を計画しており、2021年度分と合わせて発表に関わる経費として利用する計画である。