Finite Tree Automaton とは

オートマトン プログラム合成

最近、プログラム合成の研究で Finite Tree Automaton (FTA、有限木オートマトン) を使った手法がいくつか見られる。このオートマトンはプログラムの集合を簡素に表現するために用いられる。プログラムの集合を簡素に表現する手法として、ちょっと前までは Version Space Algebra (VSA) がよく用いられていたが、ここ数年の流行りはボトムアップに構築する Finite Tree Automaton なのかもしれない。平成の VSA、令和の FTA。とは言ってもそんなに Finite Tree Automaton の論文の数が多いわけではないけど。

以下の3つの論文は Finite Tree Automaton を用いた合成手法である。

本記事では、Finite Tree Automaton とそのプログラム合成への応用について簡単にまとめる。ただし図や表記は論文 Inductive Program Synthesis Over Noisy Data (ESEC/FSE 2020) からの引用である。

Finite Tree Automaton (FTA)

プログラム合成では Finite Tree Automaton の中でもボトムアップに状態を計算するものがよく見られるため、Bottom-Up Finite Tree Automaton を簡単に FTA と呼び、以降で解説することにする。ちなみに、日本語だと Tree Automaton は「木オートマトン」と訳されるっぽい。

一般的な有限オートマトンが文字列入力として状態を決定するのに対し、FTA は木構造を入力とするオートマトンである。具体的には、木構造を葉から根の方向へ順に読み込み状態を遷移させてゆく。根を読み込んだときの状態によって、その木が受理 (accept) されるか拒否 (reject) されるか決定するものである。

参考：Tree automaton - Wikipedia

よりフォーマルに、F を言語とする FTA \mathcal{A} を以下のように定義する。

\mathcal{A} = (\mathcal{Q}, F, \mathcal{Q}_f, \Delta)

  • \mathcal{Q} は状態集合
  • \mathcal{Q}_{f} (\subseteq \mathcal{Q}) は受理状態 (accepting states)
  • \Delta は遷移関数であり、q, q_1, \dots q_k \in Q かつ f \in F として f(q_1, \dots, q_k) \rightarrow q という形をもつ。

なお、すべての f \in F は アリティ が定まっているものとする。たとえば、アリティが 0 である f は木構造の葉に対応する。ある入力 t が受理されるとは、t に対して \Delta の規則を適用すると q \in \mathcal{Q}_f に遷移することである。

FTA の例として以下を考えてみる。

  • \mathcal{Q} = \{q_T, q_F\}
  • \mathcal{Q}_{f} = \{q_T\}
  • F_0 = \{ \text{True}, \text{False} \} (アリティが 0 の言語)
  • F_1 = \{ \text{not} \} (アリティが 1 の言語)
  • F_2 = \{ \text{and} \} (アリティが 2 の言語)
  • \Delta は以下とする。

f:id:t-keita:20201208034345j:plain:w300

このとき、木 \text{and}(\text{True}, \text{not}(\text{False})) によって状態がどのように遷移するのか考える。まず、木構造を以下に図示する。

f:id:t-keita:20201208034529j:plain:w200

この木に対して \Delta に含まれる規則をボトムアップに適用してゆくことで、木の頂点ごとに状態を定める。まず、木構造の根にアリティが 0 の規則を適用すると以下になる。

f:id:t-keita:20201208034843j:plain:w200

次に、規則 \text{not}(q_F) \rightarrow q_T を適用する。

f:id:t-keita:20201208034852j:plain:w200

最後に、規則 \text{and}(q_T, q_T) \rightarrow q_T を適用する。

f:id:t-keita:20201208034902j:plain:w200

結果として、木構造の根に対応する状態が q_T \in \mathcal{Q}_f となり、この入力は受理される。ちなみに、木構造をプログラムだと見なしたとき、このオートマトンは入力となるプログラムの評価結果が \text{True} になるもののみ受理するように設計されている。このように木構造を根からボトムアップに処理し、木全体に対して状態を1つの計算するのが FTA である。

Concrete Finite Tree Automata (CFTA)

ここからは入出力例からのプログラム合成でよく用いられるオートマトン Concrete Finite Tree Automata (CFTA) について説明する。

プログラム合成の問題では、プログラムを生成するための Domain-Specific Language (DSL) G と、満たすべき入出力例 (\sigma, o) が与えられるのが一般的である。CFTA は、DSL G 上で表現されるプログラムのうち、入出力例 (\sigma, o) を満たすプログラムのみを受理する FTA である。

CFTA の状態は、DSL の文法規則 s と具体的な値 c ごとに存在しうる。つまり状態を q_{s}^{c} と表現できる。状態 q_{s}^{c} が存在するということは、与えられた入力値 \sigma のもとで、規則 s を実行した結果として値 c を実現する (部分的な) プログラムが存在する、という事実を表現している。さらに、DSL G の始記号を s_0、満たすべき出力値を o としたとき、状態 q_{s_0}^{o} が存在することは、その合成が成功することを意味する。

CFTA の遷移関数は DSL G の文法とその意味から導かれる。具体的には、DSL G の文法規則 s → f (s_1,· · · ,s_k ) に対して、その実行結果が f (c_1,c_2 . . .c_k) = c で与えられるとき、 遷移関数 f(q_{s_1}^{c_1}, \dots, q_{s_k}^{c_k}) \rightarrow s_{s_k}^{c} が存在する。

CFTA の例として以下の DSL を考えてみる。

f:id:t-keita:20210119010254p:plain:w300

n が始記号であり、x は入力変数、 id は恒等関数である。つまり、入力変数 x に 2 か 3 を足すか掛けるかしてできる式の集合を表している。

いま与えられた入出力例が 1 \mapsto 9 であるとする。このとき、CFTA の一部は以下のようになる。入力値から実現できる値は無数にあるため「一部」しか図示できない。

f:id:t-keita:20210119011016p:plain:w500

ただし、状態は x, n, t と具体的な値から構成されるため、x はひし形、 n は円、t は長方形で具体的な値を囲むことで各状態が表現されている。たとえば、左の方の 1 を円で囲んだ状態は q_{n}^{1} を表している。本来、演算子 + や \times は２引数関数であるため、2つの状態を入力として1つの状態へ遷移するような図を書くべきであるが、2次元で上手く図示できないため、「\times 2」や「+ 3」など同じ状態が複数ヶ所に現れてしまっている。

CFTA の作り方は論文参照。ざっくり言うと、入力値 \sigma に対して DSL の演算を繰り返し適用することで、どの文法規則を適用した時点で何の値が得られるかを列挙できる。それを CFTA として表現するだけである。

CFTA とプログラム合成

DSL と入出力例から構成した CFTA を利用してプログラム合成の問題を解くことができる。具体的には、CFTA をグラフ構造として見たとき、初期状態に対応するノードから受理状態に対応するノードに至る経路上の文法規則を求めることで、入出力例を満たすプログラムを構成できる。

上記の CFTA の例では、初期状態の「ひし形の1」から受理状態の「二重円の9」に至る経路を求めればよい。たとえば、「x」 ⇨「id」 ⇨「+ 2」⇨「\times 3」とたどることで、プログラム (id(x)+ 2) \times 3) を得ることできる。ちなみに経路が短いほどシンプルなプログラムが得られる。

このように合成の問題をグラフ構造の探索に帰着できることから、いくつかの CFTA の派生形が提案されている。

Inductive Program Synthesis Over Noisy Data (ESEC/FSE 2020) では、各ノードに重みをつけた State-weighted finite tree automata が提案されている。以下の赤字が各ノードに与えられた重みである。

f:id:t-keita:20210119013721p:plain:w400

さまざまな観点によって重みをつけることで、用途に応じた "よい" プログラムを優先的に合成できる。

Program Synthesis using Abstraction Refinement (POPL 2018) では、各状態が具体的な値ではなく "抽象的な値" に対応する abstract finite tree automata (AFTA) が提案されている。以下の AFTA の各状態は "抽象的な値" として値の範囲を示している。

f:id:t-keita:20210119014132p:plain:w400

AFTA を用いた合成アルゴリズムでは、シンプルな AFTA から始めて徐々に状態数を増やしてゆくことで、CFTA がもつ状態数の爆発的な増加を解決したものである。モデル検査において見られる abstraction refinement という考え方に着想を得ている。具体的な値の代わりに値を抽象的に表現するという点では抽象解釈 (abstract interpretation) に似ているともいえる。この論文はなかなか面白いのでいつか紹介記事を書きたい。

所感

  • ボトムアップにプログラムを合成するアプローチとして、同じ入力に対して同じ出力を返すようなプログラムの集合を1つにまとめることを observational equivalence に基づくプログラムのクラスタリングと呼ぶことがある。おそらくこの処理は CFTA の構築と本質的に同じことをしているのだが、CFTA としてプログラム集合を表現しておくことでオートマトン同士の演算 (union, intersection) をしたり、合成の問題をグラフの探索問題に帰着したり、なにかと使い勝手がよいのだと思われる。
  • にしてもこういう仕組みを考える人はすごい。オートマトンでプログラム集合を表現してみようとは思わない。言われてみれば難しい話ではないのだけど。
  • プログラムの集合を表現する他のアプローチとして Version Space Algebra が存在する。いつかこっちの紹介記事も書いてみたい。