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

使用SMT约束机器学习进行自动调优

基本信息

批准号：
19K20241
负责人：
高野保真
金额：
$ 1.08万
依托单位：
Kitasato University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Early-Career Scientists
财政年份：
2019
资助国家：
日本
起止时间：
2019-04-01 至 2024-03-31
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19K20241/
关键词：
制約ソルバ SMT オートチューニング機械学習背景理論付きSAT

项目摘要

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

已知一种方法可以解决使用称为SMT求解器的软件建模的各种约束问题，以限制“与后台理论”的约束表达式（以下称为SMT）。由于解决方案时间取决于SMT求解器给出的约束表达式的不同之处，因此我们旨在建立一种转换约束表达式的方法，以便可以预期一个简短的求解时间，并从许多SMT求解器中选择适当的SMT求解器。目的是为机器学习创建学习模型，并使用学习模型来估计解决方案时间，并阐明统计方法是否有效减少用于验证软件和硬件的约束表达式的解决方案时间。作为机器学习的模型，将使用CNN和RNN，它们是研究计划期间的主流。在研究项目期间，SMT约束表达式被解释为“抽象的语法树”，并计划将机器学习用作特征数量，但是由于发现该研究是在现有研究中对SMT溶解器的自动调节方法进行的[Balunovic等人[Balunovic等人，Neurips，2018]，因此我们决定使用日志信息来实现进一步的改进。到目前为止，我们已经建立了一项策略，以收集目标SMT约束公式并使用名为Z3的SMT求解器输出的日志信息输出，并为机器学习建立了基础。我们正在努力使用Axiom Profiler方法中使用的结构，Axiom Profiler（一种使用Z3日志信息的调试工具）作为约束表达式的特征。在申请时，该研究计划在三年内完成，但是当前的计划大大延迟了，并应用了扩展程序，以完成2023年的研究。