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

点击翻译按钮获取中文摘要

「背景理論付きSAT」（以下、SMTと呼ぶ）という形式の制約式に対して、SMTソルバと呼ばれるソフトウェアを利用してモデル化した種々の制約問題を解く方法が知られている。SMTソルバは与える制約式によって求解時間が異なるため、短かい求解時間が期待できるように制約式を変換し、数あるSMTソルバの中から適したSMTソルバを選択する手法の確立を目指している。機械学習の学習モデルを作成し、その学習モデルを利用して求解時間を見積ることで、ソフトウェア・ハードウェアの検証に用いる制約式の求解時間の短縮に、統計的な手法が有効であるかを明らかにすることが目的となる。機械学習のモデルとしては、研究計画時に主流であったCNN・RNNを用いることとしていた。研究計画時にはSMT制約式を「抽象構文木」として解釈し、それを特徴量として機械学習する予定であったが、SMTソルバに関するオートチューニング方法の既存研究 [Balunovicら、NeurIPS、2018]で検討がなされていることが分かったため、ログ情報を用いてその改善を目指すこととした。これまでに，対象とするSMT制約式を収集し、Z3というSMTソルバが出力するログ情報を利用する方針を定めて、機械学習を行うための基盤を整えた。Z3のログ情報を用いたデバッグツールAxiom Profiler [Beckerら,TACAS2019] の手法で用いている構造を制約式の特徴量として利用するように取り組んでいる。申請時は3年で研究を完了する予定であったが、現状で大幅に計画が遅れており、2023年度中に研究を完了するように延長申請した。