研究コミュニティ SyGuS について
今日はプログラム合成のコミュニティ SyGuS についての紹介。例によって日本で自分くらいしか興味がなさそうなトピック。そのうちきっと国内でも人気が高まるはず。。。
SyGuS とは
SyGuS はプログラム合成についての有力な研究コミュニティである。プログラム合成のソルバーを評価するためのベンチマークが登録されている StarExec には、2021年1月時点で289名のメンバーが登録されている。公式ページは以下である。
このコミュニティでは、プログラム合成の研究を活性化する取り組みが行われている。たとえば、プログラム合成の問題を共通的に記述するための言語 SyGuS Language を定義している。この言語で記述されたさまざまな問題がベンチマークとして公開されており、プログラム合成の手法の評価に活用できるようになっている。実際、プログラミング系のコミュニティの論文において、SyGuS のベンチマークを使用して手法の評価を行うのが定番となっている。
それに加えて、プログラム合成のソルバーの性能を競うコンペティションが毎年開催されている。 国際会議 CAV (International Conference on Computer-Aided Verification) の併設ワークショップとして SYNT Workshop が開催されており、そこでコンペティションが開催される。コンペティションにはいくつかのトラックがあり、2019年は以下の5つのトラックが設けられた。
- General SyGuS track (General),
- Invariant synthesis track (Inv),
- Conditional Linear Integer Arithmetic track (CLIA),
- Programming By Examples [Theory of Strings] track (PBE-Strings), and
- Programming By Examples [Theory of Bit Vectors] track (PBE-BV).
汎用的なソルバーを作ってすべてにエントリーしてもよいし、ドメインに特化したソルバーを作ってトラックを絞ってエントリーしてもよい。過去のコンペティションの結果は 公式サイト から参照できる。2020年はコンペティションが開催されていなかったが、2021年は 開催予定らしい。
問題の形式
SyGuS では、プログラム合成の問題が形式的に以下のように定義されている。
A Syntax-Guided Synthesis problem (SyGuS, in short) is specified with respect to a background theory
, such as Linear-Integer-Arithmetic (LIA), that fixes the types of variables, operations on types, and their interpretation. To synthesize a function
of a given type, the input consists of two constraints: (1) a semantic constraint given as a formula
built from symbols in theory
of expressions from
such that the formula
] is valid.
ざっくり要約すると以下のような感じである。
- 問題のドメインが指定され、許される型や演算子とその意味が定義される。
- 関数
- Syntax-Guided Synthesis problem (SyGuS) は、この2種類の制約を満たす関数
要するに、使える文法が固定された状況で、制約を満たすプログラムを見つけてね、って問題である。制約式を満たすプログラムの意味が一意に定まる問題もあれば、制約が曖昧であるため解が無数に存在する問題もある。
The SyGuS Language Standard
SyGuS の問題を記述するための言語 SyGuS Language が定義されている。この言語は SMT ソルバーの問題を記述する言語 SMT-LIB にインスパイアされている。
この言語を用いて記述した問題の例を以下に示す。この問題の正解となるプログラムは、2つの引数の最大値を返すような関数、いわゆる max 関数である。
;; The background theory is linear integer arithmetic
(set-logic LIA)
;; Name and signature of the function to be synthesized
(synth-fun max2 ((x Int) (y Int)) Int
;; Declare the non-terminals that would be used in the grammar
((I Int) (B Bool))
;; Define the grammar for allowed implementations of max2
((I Int (x y 0 1
(+ I I) (- I I)
(ite B I I)))
(B Bool ((and B B) (or B B) (not B)
(= I I) (<= I I) (>= I I))))
)
(declare-var x Int)
(declare-var y Int)
;; Define the semantic constraints on the function
(constraint (>= (max2 x y) x))
(constraint (>= (max2 x y) y))
(constraint (or (= x (max2 x y)) (= y (max2 x y))))
(check-synth)
ソースコードの引用元：https://sygus.org/language/
この例では、プログラムを構成するための文法が定義され、その後満たすべき制約が記述されている。文法では、整数型の変数の足し算や引き算、if-then-else 式などが許されている。意味的な制約としては3つの式が存在している。この制約を人間が書くくらいなら max 関数を人間が書いた方が早いというのはご愛嬌。
ちなみに、以下のプログラムがこの問題の解のひとつである。
(define-fun max2 ((x Int) (y Int)) Int (ite (>= x y) x y))
公開ベンチマークとソルバー
終了したコンペティションのベンチマークやソルバーは StarExec からダウンロード可能である。その他に、サンプルのソルバーや SyGuS Language 用のパーサーが Github 上で公開されている。
サンプルのソルバーの実行手順を以下にメモしておく。ソルバーは C++ で書かれているが、依存関係の問題でビルドに何度か失敗したので Docker のコンテナの中で環境を構築することにした。それにしてもビルドって行為がダルい。早く人類がビルドに悩まなくて良い時代が来てほしい。
Docker をインストールし、以下の内容を Dockerfile というファイル名で保存する。
FROM ubuntu:18.04 WORKDIR /root/sygus/ RUN apt update \ && apt install -y wget gcc \ && apt install -y make g++-4.8 git bison flex autoconf python \ && ln -f /usr/bin/g++-4.8 /usr/bin/g++ # boost setup RUN wget http://sourceforge.net/projects/boost/files/boost/1.57.0/boost_1_57_0.tar.bz2 \ && tar --bzip2 -xf boost_1_57_0.tar.bz2 \ && cd boost_1_57_0 \ && ./bootstrap.sh --with-libraries=program_options,system \ && ./b2 install -j4 --prefix=/usr \ && ldconfig # enumerativesolver RUN git clone https://github.com/rishabhs/sygus-comp14.git \ && cd sygus-comp14/solvers/enumerative/esolver-synth-lib \ && make -j4 RUN cp ~/sygus/sygus-comp14/solvers/enumerative/esolver-synth-lib/bin/debug/esolver-synthlib ~/sygus # stochastic solver RUN apt install -y libz3-dev libgmp-dev RUN cd ~/sygus/boost_1_57_0 \ && ./bootstrap.sh --with-libraries=regex \ && ./b2 install -j4 --prefix=/usr ## build parser RUN cd ~/sygus/sygus-comp14/parser/synthlib2parser/ \ && make -j4 \ && make opt -j4 ## build solver with appropriate configuration RUN cd ~/sygus/sygus-comp14/solvers/stochastic/stoch-SyGuS-14 \ && sed -i 's/..\/parser\/src\/include\//..\/..\/..\/parser\/synthlib2parser\/src\/include\//g' build \ && sed -i 's/..\/parser\/lib\/debug\//..\/..\/..\/parser\/synthlib2parser\/lib\/debug\//g' build \ && sed -i 's/..\/parser\/lib\/opt\//..\/..\/..\/parser\/synthlib2parser\/lib\/opt\//g' build \ && sed -i 's/clang++/# clang++/g' build \ && sed -i 's/echo "Clang done./# echo "Clang done./g' build \ && ./build RUN cd ~/sygus/sygus-comp14/solvers/stochastic/stoch-SyGuS-14 \ && mv a.out stochastic_solver \ && cp stochastic_solver ~/sygus/
Dockerfile のあるディレクトリで以下のコマンドを実行することで Docker イメージのビルドを行う。
おそらくビルドには数十分要する。
$ docker build -t sygus .
sygus という名前の Docker イメージが作成されたので、これを使ってコンテナを起動する。
$ docker run -it sygus
これでコンテナ上で動く ubuntu に入れる。ディレクトリには2種類のビルド済みのソルバーが存在する。
（公開されてるソルバーは3種類あったが、面倒なので2種類だけ頑張ってコンパイルした。）
root@3e23f40e5647:~/sygus# ls boost_1_57_0 boost_1_57_0.tar.bz2 esolver-synthlib stochastic_solver sygus-comp14
2種類のソルバーをそれぞれ実行してみる。
引数に与えた問題は2014年の SyGuS コンペの簡単な問題 (2引数の max 関数を合成する問題) である。
root@3e23f40e5647:~/sygus# ./esolver-synthlib sygus-comp14/benchmarks/integer-benchmarks/max2.sl Solution 0: (define-fun max2 ((x Int) (y Int)) Int (ite (<= x y) y x)) ----------------------------------------------- root@3e23f40e5647:~/sygus# ./stochastic_solver sygus-comp14/benchmarks/integer-benchmarks/max2.sl (define-fun max2 ((x0 Int) (x1 Int) ) Int (ite (>= x0 x1) (- x0 0) x1))
表現は異なるが、どちらも合成に成功していることが分かる。めでたし。
