| Project/Area Number |
19K20241
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kitasato University |
|---|
Principal Investigator |
高野 保真 北里大学, 一般教育部, 講師 (70780550)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2021: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2020: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2019: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 制約ソルバ / SMT / オートチューニング / 機械学習 / 背景理論付きSAT |
|---|
| Outline of Research at the Start |
「背景理論付きSAT」(以下SMTと呼ぶ)の制約式としてハードウェアやソフトウェアの仕様を定義し、SMTソルバにより満たす値の組み合せがあるかを判定することで仕様を検証する手法に注目が集まっている。与える制約式ごとにSMTソルバの判定時間は大きく異なり、検証にかかる時間を見積もることが難しいという問題がある。
本研究は、制約式の意味を変えない範囲で事前に変換し、短かい求解時間が期待できるSMTソルバを自動で選択する手法を提案する。具体的には、大量の既存のベンチマーク制約式をSMTソルバに与えて事前に求解時間を蓄積しておき、その結果から学習モデルを作成して利用する。
|
| Outline of Annual Research Achievements |
「背景理論付きSAT」（以下、SMTと呼ぶ）という形式の制約式に対して、SMTソルバと呼ばれるソフトウェアを利用してモデル化した種々の制約問題を解く方法が知られている。SMTソルバは与える制約式によって求解時間が異なるため、短かい求解時間が期待できるように制約式を変換し、数あるSMTソルバの中から適したSMTソルバを選択する手法の確立を目指している。
機械学習の学習モデルを作成し、その学習モデルを利用して求解時間を見積ることで、ソフトウェア・ハードウェアの検証に用いる制約式の求解時間の短縮に、統計的な手法が有効であるかを明らかにすることが目的となる。機械学習のモデルとしては、研究計画時に主流であったCNN・RNNを用いることとしていた。
研究計画時にはSMT制約式を「抽象構文木」として解釈し、それを特徴量として機械学習する予定であったが、SMTソルバに関するオートチューニング方法の既存研究 [Balunovicら、NeurIPS、2018]で検討がなされていることが分かったため、ログ情報を用いてその改善を目指すこととした。
これまでに，対象とするSMT制約式を収集し、Z3というSMTソルバが出力するログ情報を利用する方針を定めて、機械学習を行うための基盤を整えた。Z3のログ情報を用いたデバッグツールAxiom Profiler [Beckerら,TACAS2019] の手法で用いている構造を制約式の特徴量として利用するように取り組んでいる。
申請時は3年で研究を完了する予定であったが、現状で大幅に計画が遅れており、2023年度中に研究を完了するように延長申請した。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
2019年度に実行時間の改善が必要である既存のベンチマークSMT制約式を収集したが、SMTソルバの性能向上と、ハードウェアの性能向上により、オートチューニングすべき制約式の再定義が必要となってしまった。そもそも、研究計画時に対象としていた求解時間がかかるSMT制約式が減ってしまったということになる。
また、SMTソルバに関するオートチューニング方法の既存研究 [Balunovicら、NeurIPS、2018]ではとの対比のために必要な実装に時間がかかっている。
機械学習の手法について、CNN・RNNとディープラーニングモデルを使用する予定だったが、Transformerを用いた手法の精度の良さにより、主流が移ってきており、本研究でも再検討している。
|
| Strategy for Future Research Activity |
SMT制約式の再収集により遅れてしまっており、昨年度行う予定であったAxiom Profilerで対象とする制約式のログ情報を取得する作業と、Axiom Profilerの解析を合わせて進める。
本手法の効果の確認のため、SMTソルバに関するオートチューニング方法の関連研究[Balunovicら、NeurIPS、2018]との比較を行う。その論文で変数の出現数、抽象構文木、周辺に現れる語という3種類の制約式の機械学習時の特徴量の表現方法が検討している。そのため、本研究のログ情報を用いた手法の有効性を確認する。
また、機械学習のモデルについても再検討する。
2023年度中に成果の国内・国際会議での対外発表を考えている。
|
