| 研究課題/領域番号 |
19K20241
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 北里大学 |
|---|
研究代表者 |
高野 保真 北里大学, 一般教育部, 講師 (70780550)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2021年度: 390千円 (直接経費: 300千円、間接経費: 90千円)
2020年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2019年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 制約ソルバ / SMT / 機械学習 / オートチューニング / 背景理論付きSAT |
|---|
| 研究開始時の研究の概要 |
「背景理論付きSAT」(以下SMTと呼ぶ)の制約式としてハードウェアやソフトウェアの仕様を定義し、SMTソルバにより満たす値の組み合せがあるかを判定することで仕様を検証する手法に注目が集まっている。与える制約式ごとにSMTソルバの判定時間は大きく異なり、検証にかかる時間を見積もることが難しいという問題がある。
本研究は、制約式の意味を変えない範囲で事前に変換し、短かい求解時間が期待できるSMTソルバを自動で選択する手法を提案する。具体的には、大量の既存のベンチマーク制約式をSMTソルバに与えて事前に求解時間を蓄積しておき、その結果から学習モデルを作成して利用する。
|
| 研究実績の概要 |
「背景理論付きSAT」（以下、SMTと呼ぶ）という形式の制約式に対して、SMTソルバと呼ばれるソフトウェアを利用して種々の制約問題を解く方法が知られている。SMTソルバは与える制約式をどう書くかによって求解時間が異なるが、どのように書けばよいかはSMTソルバの実装に依存する面が大きい。また、SMTソルバの実装は複雑になっており、短い求解時間が期待できるように制約式を人手で作成することは難しい。
そのため、数あるSMTソルバの中から適したSMTソルバを選択する手法や、SMT制約式の自動変換方法の確立を目指している。機械学習の学習モデルを作成し、その学習モデルを利用して求解時間を見積ることで、ソフトウェア・ハードウェアの検証に用いる制約式の求解時間の短縮に統計的な手法が有効であるかを明らかにすることが目的となる。
研究計画時にはSMT制約式を「抽象構文木」として解釈し、それを特徴量として機械学習する予定であったが、SMTソルバに関するオートチューニング方法の既存研究 [Balunovicら、NeurIPS、2018]ですでに検討がなされていることが分かった。そのため、あるSMTソルバの実装（Z3）で得られるログ情報を用いて得られた学習結果が、他のSMTソルバに転用できるかを検討している。
これまでに，対象とするSMT制約式を収集し、Z3というSMTソルバが出力するログ情報を利用する方針を定めて、機械学習を行うための基盤を整えた。Z3のログ情報を用いたデバッグツールAxiom Profiler [Beckerら,TACAS2019] の手法で用いている構造を制約式の特徴量として利用するように取り組んでいる。
現状で大幅に計画が遅れており、2024年度中に研究を完了するように延長申請した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
SMTソルバの性能向上と、ハードウェアの性能向上により、当初対象としていた「解が現実的な時間で求まらないような制約式」が、ほとんど存在しないこととなってしまった。そのため、解決すべき問題から見直すために時間がかかった。
Transformerを利用した機械学習手法を検討している。
|
| 今後の研究の推進方策 |
SMT制約式の再収集により遅れてしまっており、まず対象となる制約式を決定する。
それに加えて、Z3で見積った情報を他のSMTソルバへ転用する方法の検討について合わせて進める。
本手法の効果の確認のため、SMTソルバに関するオートチューニング方法の関連研究[Balunovicら、NeurIPS、2018]との比較を行う。その論文で変数の出現数、
抽象構文木、周辺に現れる語という3種類の制約式の機械学習時の特徴量の表現方法が検討している。そのため、本研究のログ情報を用いた手法の有効性を確認する。
2024年度中に成果の国内・国際会議での対外発表を考えている。
|
