| 研究課題/領域番号 |
19K20241
|
|---|
| 研究機関 | 北里大学 |
|---|
研究代表者 |
高野 保真 北里大学, 一般教育部, 講師 (70780550)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | 制約ソルバ / SMT / オートチューニング / 機械学習 |
|---|
| 研究実績の概要 |
「背景理論付きSAT」（以下、SMTと呼ぶ）という形式の制約式に対して、SMTソルバと呼ばれるソフトウェアの選択法について研究を進めている。SMTソルバは与える制約式によって求解時間が異なるため、短かい求解時間が期待できるように制約式を変換し、数あるSMTソルバの中から適したSMTソルバを選択する手法の確立を目指している。
機械学習の学習モデルを作成し、その学習モデルを利用して求解時間を見積ることで、ソフトウェア・ハードウェアの検証に用いる制約式の求解時間の短縮に、統計的な手法が有効であるかを明らかにすることが目的となる。
2019年度に対象とするSMT制約式を収集し、2020年度にSMTソルバのログ情報を用いる方針を固めた。研究計画時には制約式を「抽象構文木」を特徴量として機械学習する予定であったが、SMTソルバに関するオートチューニング方法の既存研究 [Balunovicら、NeurIPS、2018]で検討がなされていることが分かったため、ログ情報を用いてその改善を目指すこととした。
2021年度は、Z3というSMTソルバが出力するログ情報を利用し、機械学習を行うための基盤を整えた。ログ情報には、ある制約式の解を求める際の、Z3内の探索内容を記録しているため、より求解時間の実態を表現している。2020年度に調査したZ3のログ情報を用いたデバッグツールAxiom Profiler [Beckerら, TACAS2019] の手法で用いている構造を制約式の特徴量として利用するように取り組んでいる。
申請時は3年で研究を完了する予定であったが、現状で大幅に計画が遅れており、2022年度中に研究を完了するように延長申請した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
2019年度に収集し，学習対象とすることを決定したSMT制約式に対して、Z3のログ情報を改めて取りなおさなくてはならなくなった。制約式の動作をより表現しているログ情報ではあるが、Axiom Profilerで実行して再度実行情報を取得する必要があるためである。また、2019年度の時点では求解時間がかかっていると判定した制約式も現在の実行環境では短い求解時間で結果が得られている場合もあり、見直しが必要となった。
技術的には、Axiom ProfilerはZ3の動作をグラフ化して表現するので，Axiom Profilerのグラフ構造の作成方法を解析し、機械学習の特徴量として用いる計画であった。ただ、グラフ構造の作成方法の解析が当初予定していたようには進められなかった。
|
| 今後の研究の推進方策 |
Axiom Profilerで対象とする制約式のログ情報を取得する作業と、Axiom Profilerの解析を合わせて進める。ログ情報の取得は自動化できることが分かっている。Axiom Profilerの解析は、制約式を特徴量として用いるために必要であるが、グラフ構造を機械学習する既存の手法を用いればよいと考えている。
また、他のSMTソルバのログ機能についても調査し、SMT制約式とログの関連付けができるかなども検討する。ログ機能が十分でないSMTソルバに対しては、Z3に対するAxiom Profilerの結果から求解時間が推定可能であるかを検討する。
本手法の効果の確認のため、SMTソルバに関するオートチューニング方法の関連研究 [Balunovicら、NeurIPS、2018]との比較を行う。その論文で変数の出現数、抽象構文木、周辺に現れる語という3種類の制約式の機械学習時の特徴量の表現方法が検討している。そのため、本研究のログ情報を用いた手法の有効性を確認する。
研究機関を延長したので、2022年度中に実装、成果の国内・国際会議での対外発表を考えている。
|
| 次年度使用額が生じた理由 |
当初予定していた国際会議発表を行うことができなかったため、旅費/発表準備等の経費がかからなかったため。
|
