日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

機械学習を用いた SMT ソルバの自動選択と自動チューニングに向けて
高野 保真

坂地 泰紀

佐藤 重幸

近年，背景理論付き SAT（SMT）技術の発展に伴ない，SMT の制約式によるモデル化を用いた検証手法が様々な用途で利用されている．SMT ソルバを用いることで，制約式を高い抽象度で記述できるという利点があるものの，与える制約式によって 1 秒未満から数日経っても判定が終わらない場合など求解時間は様々であり，結果が得られるまでの時間を見積ることが難しい．さらに SMT ソルバごとに制約式に対する得手不得手があるため，現状では，判定結果を得るために試行錯誤が必要となっている．本研究では，与えられた制約式に対して短かい求解時間が期待できる SMT ソルバを，自動で選択する手法の実現に向けた取り組みについて述べる．対象とするそれぞれの SMTソルバごとに，既存のベンチマーク制約式を与えて事前に求解時間を蓄積しておく．その結果を機械学習し，学習済
みのモデルを用いて与えられた制約式の求解時間を見積り，適した SMT ソルバを選択する機構の実現を目指している．SMT の制約式は，変数などを含んだプログラムとして記述されるため，特徴量の抽出や学習手法などにおける既存手法のの適用性を明らかにすることが最終的な目標である．その取り組みの第一段階として，本論文では，制約式中の予約語の出現頻度に基づいた学習効果について予備的な実験の結果を示す．

In recent years, verification methods using modeling by Satisfiability Modulo Theories (SMT) technology
are used for various purposes. With the SMT solvers, we can describe constraint expressions with a highdegree of abstraction. Although the SMT solvers are excellent performance, it is diﬃcult to estimate its
execution time and sometimes it can be several days. We are studying about a method of automaticallyselecting the SMT solver which can expect short solving time for a given SMT expression. In advance,
execution times of the benchmark constraint expressions of SMT are accumulated and used for machinelearning. The machine learned model estimates the solution time of the given constraint expression andselects the suitable SMT solver. Since the constraint expression of SMT is described as a program including
variables, our goal is to clarify the applicability of the existing machine learning method. As a first step inthat eﬀort, this paper shows the results of preliminal experiments on the machine learning of the occurrence
frequency of reserved words in constraint expressions of SMT.

1 はじめに近年，ソフトウェアやハードウェアのシステムの複雑化にともない，その設計や実装の検証が重要度を∗ Toward Automatic Selection and Automatic Tuningof SMT Solver Using Machine LearningThis is an unrefereed paper. Copyrights belong tothe Authors.
Yasunao Takano, 青山学院大学 理工学部 情報テクノロジー学科, Dept. of Integrated Information Technology, Aoyama Gakuin University.
Hiroki Sakaji, 東京大学大学院 工学系研究科 システム創成学専攻, School of Engineering, The University ofTokyo.
Shigeyuki Sato, 高知工科大学 情報学群, School of Information, Kochi University of Technology.

増してきている．そのため，システムが満たすべき性質を制約式としてモデル化して定義し，その制約式をソルバと呼ばれるソフトウェアを用いて検証する手法に注目が集まっている．中でも背景理論付きSAT（Satisfiability Modulo Theories, 以下 SMT と呼ぶ）技術の発展 [5] に伴なって，SMT ソルバを用いた検証手法に注目が集まっており，Microsoft Re-search の Z3 [3]，Stanford University の CVC4 [1] ，
SRI International の Yices [4] など優れた SMT ソル

バが研究・開発されている．

∧ x0 = 2

SMT ソルバは，一種のプログラムとして与えられる制約式に対して，制約式中の変数に割り当てる値の∧ guard1 = (x0 > 1)組み合せを探索し，制約式を満たすか判定する．与え∧ guard2 = (guard1 ∧ (x0 %2 = 0))

る制約式ごとに，その求解時間は大きく異なり，さら∧ x1 = if guard2 then x0 /2 else x0···に使用する SMT ソルバごとにも制約式に対する得∧ ¬((x4 ≤ 1) ∧ (x4 = 1))

手不得手があるため，選択する SMT ソルバによっては数日経っても解が得られない場合もある．その上，

図1

SMT の制約式

現状では，ある制約式に対する求解時間を見積ることは大変難しく，SMT ソルバを利用する検証手法の欠とする機械学習に対して応用できるか明らかにする点となっている．見積りが難しいのは，個々の SMTことが本研究の主題である．なお，本論文はそのようソルバの実装が複雑化しているためであり，現状ではな試みの第一段階として，SMT の制約式を機械学習使用する SMT ソルバを変更したり，与える制約式のの対象とする際の前提条件を考察し，SMT-LIB 形式構造を変更するなど試行錯誤の上で SMT ソルバを[2] の予約語の頻度を用いた場合の予備実験を示す．

利用する必要がある．
これまで，我々は与える制約式の構造を変更し，部分的な解を蓄積することで制約式の結果を絞り込む

2 SMT
2. 1 SMT の制約式

手法 [7] について研究してきた．具体的には，制約式

SMT の制約式は，整数，等号，算術演算，ビット中の部分式の除去と変数の取り得る値を変更するこ

ベクタなどに関する背景理論を使って記述できるたとで制約を緩和し，そのことで一定時間内に結果が得め，表現力が高く，SAT の制約式に帰着するよりもられれば，その情報を組み合せて解を見積る手法であ元の問題の記述を保ったまま表現できるという特徴がる．そこでは，制約式に少しの変更を加えただけの緩ある．

和であっても SMT ソルバのふるまいが変わること

たとえば，論文 [6] にあるモデル検査を記述したを明らかにしたが，緩和方法と求解時間の間に明確なSMT の制約式の一部を図 1 に示す． ここで，変数関連性は見出せなかった．

x0 や x1 は整数値をとり，除算（/）や剰余（%）など

本研究では，与えられた制約式に対して短かい求整数上の演算を利用できる．また，guard1 や guard2解時間が期待できる SMT ソルバを，自動で選択すは真理値を取る変数であり，それを利用した条件分岐る手法の開発を目指す．そのために，ある定めた時も可能である．実際には，整数のみでなく実数，さら間内に SMT ソルバが解を返すかどうかという二値に，限定子，未解釈関数など複数の背景理論を組み合分類問題と考えて，機械学習を用いる．つまり，利用わせて制約式を記述することができる．このような制可能な SMT ソルバごとに，既存のベンチマーク制約式を，プログラムとして記述し，SMT ソルバに与約式を与えて事前に求解時間を蓄積しておき，そのえる．図 1 の制約式を代表的な形式である SMT-LIB結果から学習する．その学習済みのモデルを用いて，形式を用いて記述した例を図 2 に示す． 変数定義な与えられた制約式の求解時間を見積り，適した SMTどが必要であるが，図 1 の制約式をそのまま書き下ソルバを提示することが目標である．

すことができ，S 式により変数や計算式などを用いる

2 節で述べるように，SMT の制約式はプログラムため，制約式を一種のプログラムとみなすことがでとして記述されるため，機械学習による研究の進展がきる．以降，本研究では，個別の行ではなく図 2 の著しい自然言語処理に対する知見がそのまま使えるような制約全体をまとめて制約式と呼ぶこととする．

わけではない．そのため，既存の機械学習における前

ここで注目すべきは，プログラムであるので，x0 と処理方法・学習方法などの知見を，プログラムを対象いう変数はそのプログラム中で一致すればよく，他の( set-logic QF_NIA )( declare-fun x0 () Int )( declare-fun x1 () Int )( declare-fun x4 () Int )( declare-fun guard1 () Bool )( declare-fun guard2 () Bool )...
( assert( let (( x0 2)( guard1 ( > x0 1))( guard2 ( and guard1(= ( mod x0 2) 0)))...
( x1 ( ite guard2 (/ x0 2) x0 )))( not ( and ( <= x4 1) (= x4 1)))))( check-sat )

CVC4
Z3
71
2663

173441331

203
229

Yices

図3

QF NRA における解が得られない制約式の数• 結果が不明（unknown）
図2

SMT-LIB 形式の SMT の制約式

SMT ソルバの本来の目的は，充足性の判定であるので，与えた制約式が sat もしくは unsat であるかが制約式に出現する x0 とは分けて考えなければならな重要であるが，本研究では何らかの結果が得られるかい点である．このことは，プログラムを機械学習の対にのみ注目し，以下の二種類に分けて扱う．

象とする本研究において，特徴量の抽出時に考慮すべ

1. sat と unsat （以後，解が得られるという）き事項である．さらに，declare-fun や assert と

2. unknown もしくは，ある一定時間に SMT ソル

いったプログラムの予約語もあるため，一般の文章にバが結果を返さない場合（以降，解が得られないおける単語とプログラムの変数・予約語を同一視するという）ことはできない．詳しくは，3. 2 節で述べる．

与えた制約式の充足性は sat と unsat のいずれかし典型的な制約式は，SMT-LIB ベンチマーク †1 にか取り得ないものの，使用する SMT ソルバによって集められている．SML-LIB ベンチマークは背景理論解が得られるかどうかが異なることに注意されたい．

ごとに 40 ほどに分類されており，それぞれが数個かそれは，探索手法や背景理論の実現方法などによる違ら約 4 万個の制約式を含み，全体では，約 20 万個のいに起因して，制約に対する SMT ソルバごとの得手制約式がある．その多くが現実の検証システムなどか不得手があるためである．SMT-LIB ベンチマークのら取られているため，多くの SMT ソルバが性能指QF NRA セットを 4 節で述べる予備実験の環境で実標としている．

行した場合に，1 分以内に解が得られなかったベンチマーク数を図 3 に示す． 代表的な SMT ソルバであ2. 2 SMT ソルバ

る Z3，CVC4，Yices について，ベン図で表わして

図 2 のような制約式を与えると，SMT ソルバは，いる．たとえば，図中の 203 は CVC4 と Yices で制約式中の変数に割り当てる値の組み合せ（以降，値は解が得られないものの，Z3 では解が得られるベン割当て）を探索する．その結果，以下の三通りのいずチマーク数を示す．つまり，それら 203 個のベンチれかが得られる．

マークにおいては，Z3 を選択すべきである．さらに，• 与えた制約式を満たす値割当てが存在する（充足可能，sat）• 満たす値割当てが存在しない（充足不能，unsat）

3 つの重なりである 441 個を除けば，適切な SMTソルバを選択できれば，1 分以内に解が得られることが分かる．なお，4 節で示すように，全ベンチマークで 11,601 個の制約式であるため，約 96% のベンチ

†1 http://smtlib.cs.uiowa.edu/benchmarks.shtml

マークが 1 分以内に解が得られる可能性がある．

しかし，このような問題があることは分かっている

大きく影響すると考えるためである．

ものの，一般の制約式に対して，どの SMT ソルバを選択するかは，SMT-Comp†2 など背景理論全体に対

3. 2 SMT 制約式の学習する平均的な性能や，SMT ソルバの利用経験を元に一定時間に解が得られるソルバを見つけることがするなどしても現状では困難である．

目標であるので，以下のような二値分類問題とする．
正例 解が得られる

3 提案手法負例 解が得られない以上の状況を踏まえて，本研究では，与えられた制sat や unsat のそれぞれを求めるのが得意とされる

約式に対して短かい求解時間が期待できる SMT ソ

SMT ソルバも本来は判別すべきであるが，簡単のたルバを，自動で選択する手法の開発を目指す．制約

め本研究では解が得られるとして区別しない．ここ

式の求解時間を見積るために，ある定めた時間内にで注意すべきは，解が得られないと予測したもののSMT ソルバが解を返すかという二値分類問題として解が得られる場合（False negative）と，解が得られとらえて，機械学習を用いる．

ると予測したものの解が得られなかった場合（Falsepositive）の扱いである．実際の予測結果を利用して
3. 1 概要

SMT ソルバを選択する際には，False negative で本研究の全体像を図 4 に示す．学習フェーズでは，あっても一定時間内に解が得られることになるため，対象とする SMT ソルバごとに，既存のベンチマーク

SMT ソルバ選択という面からみると問題にはならな制約式を与えて求解時間から，ある定めた時間以内にい．一方で，False positive は避けなければならず，結果が返されていれば，その SMT ソルバで，その制適合率（precision）が高くなるような学習モデルが約式で解が得られたと記録する．その情報を蓄積し，望まれる．

制約式と解の有無を二値分類問題となるように機械学

また，学習のためのデータセットは，SMT ソルバ習する．個別の SMT ソルバの探索アルゴリズムにを一定時間で打ち切るように実行すれば，教師ありは立ち入らず，ブラックボックスとしてとらえて制約学習のデータセットをオーバサンプリングしやすい．

式を入力，求解時間を出力として扱い，sat と unsat

たとえば，SMT-LIB ベンチマークを元に，制約式のという本来の解を求めることを対象としていない．

意味を変えない範囲で文の順番を動かしたり，構文のそれに続いて，得られた学習済みのモデルを用いて，選択フェーズで与えられた制約式の求解時間を見置き換えにより制約式を自動生成できる．
制約式の特徴量の抽出に関しては，2. 1 節で述べた積り，適した SMT ソルバを提示することが目標でように，SMT 制約式がプログラムとして記述されてある．つまり，図 3 に示したような，解が得らないいることを考慮しなくてはならない．予約語は各プSMT ソルバを避けることができればよい．

ログラムで共通の単語として扱えるものの，変数は対応する背景理論の豊さと利用者数の面から Z3，そのスコープも含めてプログラムごとに考慮すべき

CVC4，Yices を対象とし，ベンチマーク制約式にはであり，また，リテラルが各 SMT 制約式を特徴づけSMT-Comp でも用いられている SMT-LIB ベンチている場合も考えられる．さらには，SMT ソルバにマークを用いる．なお，SMT-LIB ベンチマークを利よっては，語順が求解時間に影響している場合も考用する際に，背景理論の異なる制約式をまとめて扱うえられる．つまり，語順によって個々の SMT ソルバことはせず，それぞれの背景理論ごとに学習モデルをの探索アルゴリズムにおける変数選択順への影響や，作ることとする．データセット数が小さくなってしま評価順序に大きく影響があるためである．

うものの，背景理論の違いは SMT ソルバの特性に以上のように，プログラムとしてのふるまいを考慮した上で特徴量を抽出することが厳密には求めら†2 http://smtcomp.sourceforge.net

れるが，本論文はその前段階として，非常に単純な抽図4

出方法である予約語と組込関数の出現頻度を特徴量全体像
表11 分を閾値とした QF NRA の結果とした場合の学習効果を確認する．単純ではあるが，

SMT-LIB 形式の予約語と組込関数を言語プリミティブとして考えれば，その出現頻度が求解時間に影響していることも考えられるため，確認する意義はある．

正例

負例

Z3

10585

1016

CVC48223

3378

Yices

10397

1204

4 予備実験たため，21 次元の特徴ベクトルに変換した．さらに，

SMT 制約式の機械学習に向けて，SMT-LIB 形式個々の値のスケールを統一するため，scikit-learn のの予約語と組込関数の頻度を用いた場合の予備実験を行なった．学習には，Python による機械学習ライ
ブラリ scikit-learn を用いる．

StandardScaler により標準化した．
正例と負例の数に差があるため，以下の処理により，学習データと評価データを分割した．

1. 正例を 3 分割，負例を 3 分割する．
4. 1 実験方法

2. 正例 1/3 と負例 1/3 を合わせてシャッフルしまず，SMT-LIB ベンチマークから QF NRA の背A とし，正例 2/3 と負例 2/3 を B とする．

景理論を選択し，以下に示す実験環境で 1 分を閾値と

3. B における負例の数を，B における正例の数にして解が得られるかどうかを対象とする Z3，CVC4，Yices で実行し，データセットを用意した．実験環

合わせ、合算しシャッフルし C とする．

4. C を学習データ，A を評価データとする．

境は，CPU が Intel Core i5-2400 3.1GHz で，メイ

ここで，学習データは正例と負例の数が同じになり，ンメモリが 4GB の PC 上で動く Linux 4.4 である．

評価データにおいては数は変更していないため，現実

QF NRA は量化子なしの非線形実数演算を用いた制に得られる割合で出現する正例と負例を正しく分類

約式を集めたベンチマークで，11,601 個の制約式かできるかという問題設定と考えることができる．

らなる．表 1 に示す結果の分布となった．なお，2. 2節の図 3 に示したのは，負例を SMT ソルバ間の差4. 2 実験結果異を示すようにベン図に示したものである．

scikit-learn で典型的な分類器を利用して，予測結ここで用いた制約式を，SMT-LIB の仕様に従っ果の適合率（precision）と再現率（recall）を測定して，プログラムを構文解析し，予約語と組込関数のた．結果を図 2 に示す．最も適合率の高い Z3 の決定みを抽出し，その頻度を数えた．この際，164 種類の予約語と組込関数のうち，21 種類が使用されてい表21 分を閾値とした QF NRA の結果

Z3

CVC4適合率

再現率

適合率

再現率

適合率

再現率

SVM（RBF カーネル）

0.941

0.986

0.712

0.998

0.930

0.986

SVM（linear カーネル）

0.934

0.991

0.714

0.999

0.923

0.990

決定木

0.962

0.977

0.720

0.991

0.950

0.972

確率的勾配降下法

0.938

0.990

0.717

0.997

0.927

0.989

木によるモデルの混同行列は，以下のとおりである．
 
TN FP
203 135=
FN TP81 3447
一方で，最も適合率の低い CVC4 の SVM（RBFカーネル）によるモデルの混同行列は以下のとおりである． 

Yices
TNFP

=
191107

FN TP
5 2736
いずれの場合にも，正例と予測することが再現率の高さにつながっており，図 1 に示したように正例に偏ったデータである傾向によるところが大きい．パラメータの調整やデータセットの検討により，結果の分析が今後必要である．

5 まとめと今後の課題
本研究では，与えられた制約式に対して短かい求解時間が期待できる SMT ソルバを，自動で選択する手法の開発を目指して，ある定めた時間内に SMTソルバが解を返すかどうかという二値分類問題と考えて，機械学習を用いる手法を示した．本論文はそのような試みの第一段階として，SMT の制約式を機械学習の対象とする際の前提条件を考察し，SMT-LIBの仕様にもとづいて構文解析し，予約語と組込関数の頻度を用いた学習モデルにより予備的な実験の結果を示した．
今後の課題は，以下の 3 点である．

1. 実験結果の詳細な検討と，学習・テストデータセットの検討

2. よりプログラムの意味を反映した特徴量の抽出方法の開発

3. 制約式のオートチューニング手法の開発
1 つ目に関して，4 節で示した結果の詳細な検討はまだ完了しておらず，学習・テストに用意するデータセットについてもさらに検討が必要である．また，2つ目について，今回の実装は予約語と組込関数の頻度という非常に単純な特徴量を用いたが，3. 2 節で述べたようなプログラムとしての変数などの要素を含めたベクトル化手法について扱う．3 つ目に関して，どのSMT ソルバを用いても解が得られないと予測される制約式について，意味を変えない範囲で式を変形し，SMT ソルバの選択フェーズを繰り返す．変形した式を学習モデルで予測させることで，SMT ソルバを繰り返し利用するよりも効率的に解を探索できると考えている．

参 考 文 献[1] Barrett, C., Conway, C. L., Deters, M., Hadarean,L., Jovanović, D., King, T., Reynolds, A., andTinelli, C.: CVC4, Proceedings of the 23rd International Conference on Computer Aided Verification,
2011, pp. 171–177.
[2] Barrett, C., Fontaine, P., and Tinelli, C.:
The SMT-LIB Standard Version 2.5, http://smtlib.cs.uiowa.edu/language.shtml, 2015.
[3] De Moura, L. and Bjørner, N.: Z3: An Eﬃcient
SMT Solver, Proceedings of the Theory and Practiceof Software, 14th International Conference on Tools
and Algorithms for the Construction and Analysisof Systems, 2008, pp. 337–340.
[4] Dutertre, B.: Yices 2.2, Computer-Aided Verification (CAV’2014), Biere, A. and Bloem, R.(eds.),
Lecture Notes in Computer Science, Vol. 8559,
Springer, July 2014, pp. 737–744.
[5] 岩沼宏治, 鍋島英知: SMT:個別理論を取り扱う SAT技術 (<特集> 最近の SAT 技術の発展), 人工知能学会誌, Vol. 25, No. 1(2010), pp. 86–95.
[6] 土屋達弘: 充足可能性判定を利用したモデル検査,
コ ン ピュー タ ソ フ ト ウェア, Vol. 29, No. 1(2012),
pp. 1 19–1 29.
[7] 高野保真, 千代英一郎: 反復的な試行にもとづく SMTソルバ実行戦略の検討, 情報処理学会論文誌プログラミング（PRO）, Vol. 11, No. 2(2018), pp. 9–19.