Interpolants as Classifiers
線形算術の論理式A∧Bのクレイグ補間となる線形算術論理式を求めるために、AとBからサンプリングした点を使ってSVMで分離平面を求める話で、言われてみれば当たり前だけど、面白かった。
プログラム解析への応用を考えると典型的にはAとBはinfeasibleであるtraceの前半と後半を論理式で表現したものだけど、Aからのサンプリングに関してはソルバで解かずとも、単にランダム生成した入力から普通に実行することもできて、非線形性などソルバが苦手なものが入っても大丈夫。
また、線形分離できない場合にも、例えばBの点を1個ずつAから分離するようなinterpolantを求めて連言をとる、みたいなことをすれば、連言や選言の形をしたinterpolantを求めたりもできる。
https://theory.stanford.edu/~aiken/publications/papers/cav12a.pdf
https://link.springer.com/chapter/10.1007/978-3-642-31424-7_11
Interpolants as Classifiers
