makenowjust-labs/blog

MakeNowJust Laboratory Tech Blog

最新のオートマトン学習アルゴリズムL#について

2024-08-17 (更新: 2024-08-21) / 読むのにかかる時間: 約60.8

L#L^\# というオートマトン学習のアルゴリズムがあります。

2022年にVaandragerらによって提案された、最新のオートマトン学習のアルゴリズムです。 apartness relationという概念を用いて、よく知られているAngluinの LL^\ast とは少し違ったアイディアでオートマトンの学習を実現します。 学習に用いるデータ構造として、従来のobservation tableやdiscrimination treeではなく、observation treeというmembership query (output query) のキャッシュのようなものを利用するのも特徴です。

この記事では L#L^\# の詳細や実装について、論文 [Vaandrager et al., 2022] を参考に解説します。

想定読者: オートマトン理論やオートマトン学習について理解・関心がある。

L#L^\# とは

L#L^\# は 2022年にVaandragerによって提案された、最新のオートマトン学習のアルゴリズムです。 [Vaandrager et al., 2022] で発表され、その実装は https://gitlab.science.ru.nl/sws/lsharp で公開されています。 また、VaandragerによるVSTTE 2021での発表資料も公開されており、こちらも参考になります。

この記事では、論文[Vaandrager et al., 2022]発表資料を参考に、L#L^\# について解説します。

L#L^\# はオートマトン学習 (automata learning) のアルゴリズムの一つで、次のような特徴があります。

  • Angluinの LL^\ast とは異なり、apartness relationという「ある状態とある状態が (学習対象のオートマトンで) 異なる状態を表している」ことを表す関係 #\# を導入する。
  • 従来のobservation tableやdiscrimination treeではなく、observation treeというmembership query (output query) のキャッシュに似たデータ構造を用いる。

計算量の観点で見ても、オートマトン学習ではmembership queryの回数が O(kn2+nlogm)\mathcal{O}(k n^2 + n \log m) (kk はアルファベットの大きさ、nn は学習したオートマトンの状態数、mm は反例の長さの最大値) となることがベストであると考えられているのですが、L#L^\# はRivest-SchapireやTTTと同様にこの計算量に収まっています。 また[Vaandrager et al., 2022]の実験でも、既存のアルゴリズムと比較して遜色ない性能が示されていました。

このように L#L^\# は今最も注目のオートマトン学習アルゴリズムなのではないかと思います。

準備

集合 AA について、AA^\astAA の要素からなる (文字) 列の全体からなる集合を表します。 uAu \in A^\ast の長さは u|u| と書きます。 ε\varepsilon は長さ 00 の列 (空列空文字列) を表し、文脈に応じて aAa \in A を長さ 11 の列と見做すこともあります。 2つの列 u1A,u2Au_1 \in A^\ast,\, u_2 \in A^\ast について、u1u2u_1 u_2 を2つの文字列を並べたもの (連接) を表すものとします。

f ⁣:ABf\colon A \rightharpoonup BAA から BB への部分関数です。 このとき aAa \in A について f(a)f(a) が定義されているとき f(a) ⁣ ⁣f(a)\!\!\downarrow と書き、f(a)f(a) が定義されていないとき f(a) ⁣ ⁣f(a)\!\!\uparrow と書きます。

L#L^\# は論文ではMealy機械を学習するアルゴリズムとして提案されています。 そこでMealy機械について定義します。

参照しているMealy機械を明示するために上付き文字を付けて QM,q0M,δM,λMQ^\mathcal{M}, q_0^\mathcal{M}, \delta^\mathcal{M}, \lambda^\mathcal{M} のように書くことがあります。 δ\delta がすべての qQ,iIq \in Q,\,i \in I について定義されているとき、M\mathcal{M}completeと言います。

δ\delta は文字列について δ(q,ε)=q,δ(q,iu)=δ(δ(q,i),u)\delta(q, \varepsilon) = q,\,\delta(q, i u) = \delta(\delta(q, i), u) (iI,uIi \in I,\, u \in I^\ast) として拡張されます。 加えて、λ\lambda は文字列について λ(q,ε)=ε,λ(q,iu)=λ(q,i)λ(δ(q,i),u)\lambda(q, \varepsilon) = \varepsilon,\,\lambda(q, i u) = \lambda(q, i) \lambda(\delta(q, i), u) として拡張されます。

状態 qQq \in Q について L(q)={uIδ(q,u) ⁣ ⁣}\mathcal{L}(q) = \{ u \in I^\ast \mid \delta(q, u)\!\!\downarrow \} と定義します。 さらに q ⁣:L(q)O\llbracket q \rrbracket\colon \mathcal{L}(q) \to O^\astq(w)=λ(q,u)\llbracket q \rrbracket(w) = \lambda(q, u) と定義します。 2つの状態 q1,q2q_1, q_2 について q1=q2\llbracket q_1 \rrbracket = \llbracket q_2 \rrbracket のとき q1q2q_1 \approx q_2 と書きます。

最後に、Mealy機械の学習の問題について確認します。 次の2種類のクエリを考えます。

  • OUTPUT(u)\mathrm{OUTPUT}(u) (output query): 文字列 uIu \in I^\ast に対して、学習対象のMealy機械での出力列を返すクエリです。
  • EQUIV(H)\mathrm{EQUIV}(\mathcal{H}) (equivalence query): 仮説のMealy機械 H\mathcal{H} が学習対象のMealy機械と等価か確認し、等価な場合は yes\mathbf{yes} を、等価でない場合は反例となる文字列 vIv \in I^\ast (つまり、λH(q0H,v)OUTPUT(v)\lambda^\mathcal{H}(q_0^\mathcal{H}, v) \ne \mathrm{OUTPUT}(v)) を返します。

これらのクエリが与えられて、学習対象のオートマトンと等価なMealy機械 H\mathcal{H} (つまり EQUIV(H)=yes\mathrm{EQUIV}(\mathcal{H}) = \mathbf{yes} となる H\mathcal{H}) を求めるのがMealy機械の学習となります。

observation tree

まず L#L^\# で重要なデータ構造となるobservation treeについて説明します。

observation treeはMealy機械の一種として定義されます。

次のようなMealy機械 M1\mathcal{M}_1 があったとします。

このMealy機械に対するobservation treeとして、例えば次のようなMealy機械 T1\mathcal{T}_1 が考えられます。

このとき access(q)\mathrm{access}(q) の値は、例えば access(t2)=aa,access(t7)=bba\mathrm{access}(t_2) = aa,\, \mathrm{access}(t_7) = bba です。

observation treeはMealy機械の入力と出力を平坦に (状態の構造を忘れて) 記録したものだと考えられます。 つまり、observation treeは OUTPUT(u)\mathrm{OUTPUT}(u) のキャッシュそのものと捉えられます。 同じ文字列に対して OUTPUT(u)\mathrm{OUTPUT}(u) を呼び出すのは無駄なので、キャッシュするのは自然な考えです。

自然に記録している値を用いて学習が出来る」のが L#L^\# の強みの1つというわけです。

apartness relation

次に L#L^\# で重要となるapartness relationの概念について説明します。

apartness relationは構成主義の数学で用いられる道具で、Brouwerによって導入されHeytingによって公理化されました。 apartness relationは #\# の記号で書かれ、通常の不等号 \ne とは区別されます。

apartness relation #\# は次の公理を見たす2項関係です。

  1. ¬(x#x)\lnot (x \mathrel{\#} x) (irreflexivity)
  2. x#yy#xx \mathrel{\#} y \Rightarrow y \mathrel{\#} x (symmetricity)
  3. x#yx#zy#zx \mathrel{\#} y \Rightarrow x \mathrel{\#} z \lor y \mathrel{\#} z (co-transitivity)

Mealy機械 M\mathcal{M} について、次のようなapartness relationを定義できます。

このapartness relationはirreflexivitysymmetricityを満たしますが、co-transitivityを満たさない場合があります。 Mealy機械 M\mathcal{M} がcompleteでない場合、q1#Mq2q_1 \mathrel{\#_\mathcal{M}} q_2 でも δ(q,witness(q1,q2)) ⁣ ⁣\delta(q, \mathrm{witness}(q_1, q_2))\!\!\uparrow のとき、q1#Mqq_1 \mathrel{\#_\mathcal{M}} q とも q2#Mqq_2 \mathrel{\#_\mathcal{M}} q とも言えない可能性があるからです1

例えば、上の T1\mathcal{T}_1 では t1#T1t5t_1 \mathrel{\#_{\mathcal{T}_1}} t_5witness(t1,t5)=b\mathrm{witness}(t_1, t_5) = b ですが、δ(t2,b) ⁣ ⁣\delta(t_2, b)\!\!\uparrow のため t1#T1t2t_1 \mathrel{\#_{\mathcal{T}_1}} t_2 とも t5#T1t2t_5 \mathrel{\#_{\mathcal{T}_1}} t_2 とも言えません。

Mealy機械 M\mathcal{M} のobservation tree T\mathcal{T}について、T\mathcal{T} 上のapartness relation #T\#_\mathcal{T} は、M\mathcal{M} と次のような関係があります。

observation treeが (定義されている範囲で) 元のMealy機械の出力と等しいことから、このことはすぐに分かります。

この補題から、observation treeのapartness relationを考えることで、状態の組が少なくとも学習対象のMealy機械でも異なる状態の組を表している、ということが分かります。

Mealy機械 M\mathcal{M} 上のapartness relationについて、co-transitivityを満たさない場合があると定義した際に述べました。 しかし、次のweak co-transitivityであれば常に成り立ちます。

問題となる δM(q,witness(t1,t2)) ⁣ ⁣\delta^\mathcal{M}(q, \mathrm{witness}(t_1, t_2))\!\!\uparrow の場合を潰した条件になっています。

weak co-transitivityは学習の際に、区別可能な (apartness relationに含まれる) 状態の組を増やすのに役に立ちます。

L#L^\# アルゴリズム

ここからは L#L^\# のアルゴリズム本体について解説していきます。

これまで説明してきたように L#L^\# ではobservation treeを主なデータ構造として利用します。 そして、observation treeはoutput queryのキャッシュとして振舞います。 L#L^\# の実行中に管理されるobservation tree T\mathcal{T} について、output queryの呼び出しによって T\mathcal{T} が更新されていくことを明示するために、そのようなoutput queryの呼び出しを OUTPUTT(u)\mathrm{OUTPUT}_\mathcal{T}(u) と書くことにします。

L#L^\#T\mathcal{T} に加えて、次の2つの集合と1つの関係 (B,F,)(B, F, \rightsquigarrow) を管理しながら実行されます。

  • BQTB \subseteq Q^\mathcal{T}basis集合で、学習対象のMealy機械と対応付いている状態の集合です。basis集合の2つの状態 t1,t2Bt_1, t_2 \in B について t1#Tt2t_1 \mathrel{\#_\mathcal{T}} t_2 が成り立ちます。
  • FQTBF \subseteq Q^\mathcal{T} \setminus Bfrontier集合で、basis集合に含まれる状態から1文字で遷移できる状態を集めたものです。frontier集合の状態が、basis集合のすべての状態から区別できるようになったとき、その状態はfrontier集合からbasis集合へと移動します。
  • F×B\rightsquigarrow \subseteq F \times B はfrontier集合の状態から、まだ区別できていないbasis集合の状態への写像である関係です。={(s,t)F×B¬(s#Tt)}\rightsquigarrow = \{ (s, t) \in F \times B \mid \lnot (s \mathrel{\#_\mathcal{T}} t) \} を満たすように更新されています。

frontier集合の状態 sFs \in F について [s]B[s]_\rightsquigarrow \subseteq B[s]={tBst}[s]_\rightsquigarrow = \{ t \in B \mid s \rightsquigarrow t \} と定義します。

仮説のオートマトンの構築

T\mathcal{T} からの仮説のMealy機械 H\mathcal{H} の構築の説明のために、いくつか用語を定義します。

これらの用語について、もう少し補足の説明をします。

  • sFs \in Fisolatedということは、今学習対象のMealy機械と対応付いているすべての状態と区別されているということです。つまり、isolatedな ss は新しいbasis集合の状態になれる状態ということです。
  • sFs \in Fidentifiedということはこれまでに記録した限りではbasis集合の特定の状態と、学習対象のMealy機械上では同じ状態を表していると考えられます。つまり、T\mathcal{T}ss に遷移する場合、仮説のMealy機械 H\mathcal{H} では sts \rightsquigarrow t となる tt に対応する状態へと遷移することになります。
  • tBt \in Bcompleteということは、仮説のMealy機械を構築する際に遷移先の状態が存在せず遷移できないということが起こらないことを意味しています。

例として、observation treeを上の T1\mathcal{T}_1 として B={t0,t1},F={t2,t3,t5}B = \{ t_0, t_1 \},\, F = \{ t_2, t_3, t_5 \} とします。 次の図は、このときの様子を図にしたもので、赤いノードがbasis集合の状態を、緑のノードがfrontier集合の状態を表し、点線の矢印は \rightsquigarrow の関係を表します。

このとき、

  • [t2]={t0,t1}[t_2]_\rightsquigarrow = \{ t_0, t_1 \} なので t2Ft_2 \in F はisolatedでもidentifiedでもない状態です。
  • [t3]={t1}[t_3]_\rightsquigarrow = \{ t_1 \} なので t3Ft_3 \in F はidentifiedな状態です。
  • [t5]=[t_5]_\rightsquigarrow = \emptyset なので t5Ft_5 \in F はisolatedな状態です。

また、B={t0,t1}B = \{ t_0, t_1 \} は各入力文字 i{a,b}i \in \{ a, b \} について遷移先が定義されているため、BB はcompleteです。

observation tree T\mathcal{T}から仮説のMealy機械 H\mathcal{H} の構築は、次のように行います。

FF がidentifiedかつ BB がcompleteとしているので、仮説のMealy機械は正しく定義されます。

H\mathcal{H}T\mathcal{T} の一貫性

仮説のMealy機械はfrontier集合までの状態を元に構築しているため、場合によっては H\mathcal{H}T\mathcal{T}一貫していない、つまり、ある文字列で区別できる状態に遷移してしまう (δH(q0H,u)#TδT(q0T,u)\delta^\mathcal{H}(q_0^\mathcal{H}, u) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, u) となる文字列 uIu \in I^\ast が存在する) 場合があります。 このような場合、H\mathcal{H} は明らかに学習対象のMealy機械と等価ではないので、事前にチェックしておきたいです。

具体的には、次のようなアルゴリズムで、H\mathcal{H}T\mathcal{T} と一貫しているかチェックできます。

Algorithm 1 Check consistency between T\mathcal{T} and H\mathcal{H}

function CheckConsistency(H\mathcal{H})

queue\mathit{queue} \gets new queue of QT×QHQ^\mathcal{T} \times Q^\mathcal{H}

enqueue(queue,(q0T,q0H))\mathrm{enqueue}(\mathit{queue}, (q_0^\mathcal{T}, q_0^\mathcal{H}))

while queue\mathit{queue} is not empty do

(t,q)dequeue(queue)(t, q) \gets \mathrm{dequeue}(\mathit{queue})

if t#Tqt \mathrel{\#_\mathcal{T}} q then

return access(t)\mathrm{access}(t)

else

for iIδT(t,i) ⁣ ⁣i \in I \land \delta^\mathcal{T}(t, i)\!\!\downarrow do

enqueue(queue,(δT(t,i),δH(q,i)))\mathrm{enqueue}(\mathit{queue}, (\delta^\mathcal{T}(t, i), \delta^\mathcal{H}(q, i)))

end for

end if

end while

return yes\mathbf{yes}

end function

内容は T\mathcal{T} の状態と H\mathcal{H} の状態の組 (t,q)(t, q) を、初期状態から幅優先探索で t#Tqt \mathrel{\#_\mathcal{T}} q となっていないか探索しているだけです2。 また、返り値は一貫している場合は yes\mathbf{yes}、一貫していない場合は δH(q0H,u)#TδT(q0T,u)\delta^\mathcal{H}(q_0^\mathcal{H}, u) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, u) となる文字列 uu を返します。

こうすることで、比較的重いクエリであるequivalence queryを呼び出す回数を減らせます。

L#L^\# のアルゴリズム本体

L#L^\# は次のようにして、オートマトンを学習していきます。

  1. T\mathcal{T} を初期状態 t0t_0 のみのtree、BB{t0}\{ t_0 \}FF\rightsquigarrow を空集合で初期化します。
  2. 次の処理を繰り返します。
    1. \rightsquigarrowT\mathcal{T}B,FB, F に合わせて更新します。
    2. promotion: FF にisolatedな状態 sFs \in F がある場合、ssBB に移動し、繰り返しをやり直します。
    3. completion: BB にcompleteでない状態 tBt \in B がある場合、δT(q,i) ⁣ ⁣\delta^\mathcal{T}(q, i)\!\!\uparrow または δT(q,i)F\delta^\mathcal{T}(q, i) \notin F である iIi \in I について OUTPUTT(access(t)  i)\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(t)\;i) を呼び出し、δT(q,i)\delta^\mathcal{T}(q, i)FF に追加し、繰り返しをやり直します。
    4. identification: FF にidentifiedでない状態 sFs \in F がある場合、2つのbasis集合の状態 t1,t2[s]t_1, t_2 \in [s]_\rightsquigarrow について OUTPUTT(access(s)  witness(t1,t2))\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(s)\;\mathrm{witness}(t_1, t_2)) を呼び出し、繰り返しをやり直します。
    5. ここからequivalence checking: BB がcompleteかつ FF がidentifiedなので、仮説のオートマトン H\mathcal{H} を構築します。
    6. CheckConsistency(H)\text{\htmlClass{katex-ps-funcname}{CheckConsistency}}(\mathcal{H}) を呼び出します。
      • 反例の文字列 xx を返した場合、xx を記憶しておきます。
      • yes\mathbf{yes} を返した場合、EQUIV(H)\mathrm{EQUIV}(\mathcal{H}) を呼び出します。
        • 反例の文字列 yy を返した場合、δH(q0H,x)#TδT(q0T,x)\delta^\mathcal{H}(q_0^\mathcal{H}, x) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, x) となる yy の接頭辞で最小の xx を探します。
        • これも yes\mathbf{yes} を返した場合、H\mathcal{H} は学習対象のMealy機械と等価なので、それを返して学習を終了します。
    7. 反例の文字列 xxT\mathcal{T} に反映する手続き ProcCounterEx(H,x)\text{\htmlClass{katex-ps-funcname}{ProcCounterEx}}(\mathcal{H}, x) を呼び出します (この手続きProcCounterExについては後で説明します)。

つまり、FF のisolatedな状態を BB に移動しつつ (promotion)、BB がcompleteかつ FF がidentifiedとなるように処理を繰り返し、仮説のMealy機械が作れるようになったら、それを使って CheckConsistency(H)\text{\htmlClass{katex-ps-funcname}{CheckConsistency}}(\mathcal{H})EQUIV(H)\mathrm{EQUIV}(\mathcal{H}) を呼び出し、返された反例を T\mathcal{T} に反映していく、というのが L#L^\# の流れになります。

もう少し具体的な疑似コードで説明したものが、次のアルゴリズム (LSharp) になります。

Algorithm 2 The L#L^\# algorithm

function LSharp()

T\mathcal{T} \gets a tree with an intial state t0t_0

B{t0}B \gets \{ t_0 \} and FF \gets \emptyset

repeat

{(s,t)F×B¬(s#Tt)}\rightsquigarrow \gets \{ (s, t) \in F \times B \mid \lnot (s \mathrel{\#_\mathcal{T}} t) \}

// promotion:

if sF[s]=s \in F \land [s]_\rightsquigarrow = \emptyset then

BB{s}B \gets B \cup \{ s \} and FF{s}F \gets F \setminus \{ s \}

continue

end if

// completion:

if tBiI(δT(t,i) ⁣ ⁣δT(t,i)BF)t \in B \land i \in I \land (\delta^\mathcal{T}(t, i)\!\!\uparrow \lor \delta^\mathcal{T}(t, i) \notin B \cup F) then

OUTPUTT(access(t)  i)\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(t)\;i)

FF{δT(t,i)}F \gets F \cup \{ \delta^\mathcal{T}(t, i) \}

continue

end if

// identification:

if sFt1,t2[s]s \in F \land t_1, t_2 \in [s]_\rightsquigarrow then

OUTPUTT(access(s)  witness(t1,t2))\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(s)\;\mathrm{witness}(t_1, t_2))

continue

end if

// Now, BB is complete and FF is identified.

H\mathcal{H} \gets the hypothesis Mealy machine constructed from T\mathcal{T} and (B,F,)(B, F, \rightsquigarrow)

xx \gets CheckConsistency(H\mathcal{H})

if x=yesx = \mathbf{yes} then

yEQUIV(H)y \gets \mathrm{EQUIV}(\mathcal{H})

if yyesy \ne \mathbf{yes} then

OUTPUTT(y)\mathrm{OUTPUT}_\mathcal{T}(y)

xx \gets the shortest prefix of yy s.t. δT(q0T,x)#TδH(q0H,x)\delta^\mathcal{T}(q_0^\mathcal{T}, x) \mathrel{\#_\mathcal{T}} \delta^\mathcal{H}(q_0^\mathcal{H}, x)

end if

end if

if xyesx \ne \mathbf{yes} then

ProcCounterEx(H,x\mathcal{H}, x)

end if

until EQUIV(H)=yes\mathrm{EQUIV}(\mathcal{H}) = \mathbf{yes}

return H\mathbf{H}

end function

promotionやcompletionでは BBFF が変化するので、学習が進んでいることが分かります。 また、identificationではweak co-transitivity (補題2) により、このあとの \rightsquigarrow の更新で [s]|[s]_\rightsquigarrow| が小さくなるため、同様に学習が進みます。

promotion、completion、identificationでの OUTPUT(u)\mathrm{OUTPUT}(u) の呼び出し回数は、identificationでのものが支配的です。 k=I,n=Bk = |I|,\, n = |B| とすると、F|F| の大きさは knk n で抑えられて、各 sFs \in F について [s][s]_\rightsquigarrow の大きさは高々 nn のため、identificationでの OUTPUT(w)\mathrm{OUTPUT}(w) の呼び出し回数は O(kn2)\mathcal{O}(k n^2) で抑えられます。

後述するように、 ProcCounterEx(H,x)\text{\htmlClass{katex-ps-funcname}{ProcCounterEx}}(\mathcal{H}, x) は反例の文字列の長さ m=xm = |x| について O(logm)\mathcal{O}(\log m) 回の OUTPUT(u)\mathrm{OUTPUT}(u) の呼び出し回数で実現できます。 ProcCounterEx(H,x)\text{\htmlClass{katex-ps-funcname}{ProcCounterEx}}(\mathcal{H}, x) の呼び出し回数は高々 nn 回なので、全体での OUTPUT(w)\mathrm{OUTPUT}(w) の呼び出し回数は O(kn2+nlogm)\mathcal{O}(k n^2 + n \log m) で抑えられます。

計算量についての詳細な解析は論文を参照してください。

反例の処理

最後に、反例の処理を行うProcCounterExについて説明します。

反例の処理は新しい状態が増えることを目標とします。 L#L^\# において新しい状態が増えるとは、FF の状態が BB へと移動する (promotion) ことを意味します。 そして、promotionが行なわれるためには、その FF の状態がisolatedにならなければいけません。

仮説のオートマトンを構築した段階では、frontier集合の状態 sFs \in F はすべてidentifiedなのでsts \rightsquigarrow t となる tBt \in B が1つ存在しています。 そのためProcCounterExでは、その中のOUTPUTT(u)\mathrm{OUTPUT}_\mathcal{T}(u)の呼び出しで、ある tFt \in Fs#Tts \mathrel{\#_\mathcal{T}} t となるように T\mathcal{T} が更新されればいいわけです。

ProcCounterExは次のようなアルゴリズムになります3

Algorithm 3

procedure ProcCounterEx(H,x\mathcal{H}, x)

vv \gets the unique prefix of xx s.t. δT(q0T,v)F\delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F

while v<x|v| < |x| do // i.e. δT(q0T,x)F\delta^\mathcal{T}(q_0^\mathcal{T}, x) \notin F

qδH(q0H,x)q \gets \delta^\mathcal{H}(q_0^\mathcal{H}, x) and tδT(q0T,x)t \gets \delta^\mathcal{T}(q_0^\mathcal{T}, x)

wwitness(q,t)w \gets \mathrm{witness}(q, t) // Invariant:  q#Tt\ q \mathrel{\#_\mathcal{T}} t

v+xv2\ell \gets |v| + \lfloor \frac{|x| - |v|}{2} \rfloor

x1x[1]x_1 \gets x[1 \dots \ell] and x2x[+1x]x_2 \gets x[\ell + 1 \dots |x|]

q1δH(q0H,x1)q_1 \gets \delta^\mathcal{H}(q_0^\mathcal{H}, x_1) and t1δT(q0T,x1)t_1 \gets \delta^\mathcal{T}(q_0^\mathcal{T}, x_1)

OUTPUTT(access(q1)  x2  w)\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(q_1)\;x_2\;w)

if q1#Tt1q_1 \mathrel{\#_\mathcal{T}} t_1 then

xx1x \gets x_1

else

xaccess(q1)  x2x \gets \mathrm{access}(q_1)\;x_2

vv \gets the unique prefix of xx s.t. δT(q0T,v)F\delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F

end if

end while

end procedure

LSharpの中でProcCounterExを呼び出す前に OUTPUTT(x)\mathrm{OUTPUT}_\mathcal{T}(x) を呼んでいるので δT(q0T,x) ⁣ ⁣\delta^\mathcal{T}(q_0^\mathcal{T}, x)\!\!\downarrow ですが、xx の接頭辞のどこかで BB の状態から FF の状態へ遷移しているはずです。 そのような接頭辞をアルゴリズム中では vv として、ProcCounterExでは次の不変条件を保ちながら、vv 以降の xx の文字列の長さを二分探索のように半分にしていきます。

  • δH(q0H,x)#TδT(q0T,x)\delta^\mathcal{H}(q_0^\mathcal{H}, x) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, x)
  • vvxx の接頭辞で δT(q0T,v)F\delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F であるもの (ちょうど1つしか存在しない)

ループが終わったとき x=vx = v のため δT(q0T,x)F\delta^\mathcal{T}(q_0^\mathcal{T}, x) \in F となります。 さらに q=δH(q0H,x),t=δT(q0T,x)q = \delta^\mathcal{H}(q_0^\mathcal{H}, x),\, t = \delta^\mathcal{T}(q_0^\mathcal{T}, x) としたとき、不変条件から q#Ttq \mathrm{\#_\mathcal{T}} t が言えます。 よって tt がisolatedとなるため、新しい状態が生じるわけです。

次に、ループ中に不変条件が本当に保たれていることを確認していきます。 ProcCounterExでは、OUTPUTT(access(q1)  x2  w)\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(q_1)\;x_2\;w) を呼び出したあとに q1#Tt1q_1 \mathrel{\#_\mathcal{T}} t_1 で分岐を行なっています。 q1#Tt1q_1 \mathrel{\#_\mathcal{T}} t_1 が真の場合は xx1x \gets x_1 としますが、この場合は接頭辞も変わらないため、明らかに不変条件を満たしています。

一方、¬(q1#Tt1)\lnot (q_1 \mathrel{\#_\mathcal{T}} t_1) の場合はどうでしょうか。 t2=δT(q0T,access(q1)  x2)t_2 = \delta^\mathcal{T}(q_0^\mathcal{T}, \mathrm{access}(q_1)\;x_2) とおきます。 q=δH(access(q1)  x2)q = \delta^\mathcal{H}(\mathrm{access}(q_1)\;x_2) なので q#Tt2q \mathrel{\#_\mathcal{T}} t_2 が言えればよいです。 このとき w=witness(q,t)w = \mathrm{witness}(q, t)OUTPUTT(access(q1)  x2  w)\mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(q_1)\;x_2\;w) を事前に呼び出していて δT(t2,w) ⁣ ⁣\delta^\mathcal{T}(t_2, w)\!\!\downarrow となり、weak co-transitivity (補題2) より q#Tt2t#Tt2q \mathrel{\#_\mathcal{T}} t_2 \lor t \mathrel{\#_\mathcal{T}} t_2 が分かります。 そのため ¬(t#Tt2)\lnot (t \mathrel{\#_\mathcal{T}} t_2) が言えれば、目的の命題が得られます。

ここで、次の補題を考えます。

¬(q1#Mq2)\lnot (q_1 \mathrel{\#_\mathcal{M}} q_2) であれば、そこからの遷移が定義されているのであればその先でもapartness relationが成立しないことが維持されるということです。

ここで access(t)=x1  x2\mathrm{access}(t) = x_1\;x_2 かつ access(t2)=access(q1)  x2\mathrm{access}(t_2) = \mathrm{access}(q_1)\;x_2 であることから、tt および t2t_2 はそれぞれ x1x_1q1q_1 から文字列 x2x_2 で遷移した先の状態なことが分かります。 よって、分岐条件 ¬(q1#Tt1)\lnot (q_1 \mathrel{\#_\mathcal{T}} t_1) と上の補題より ¬(t#Tt2)\lnot (t \mathrel{\#_\mathcal{T}} t_2) が分かり、q#Tt2q \mathrel{\#_\mathcal{T}} t_2 が示せます。

最後に、このアルゴリズムが正しく停止するのか考えます。 基本的には xv|x| - |v| は減少していくのですが xv=1|x| - |v| = 1 の場合 (xv)/2==0\lfloor (|x| - |v|) / 2 \rfloor == 0 のため、¬(q1#Tt1)\lnot (q_1 \mathrel{\#_\mathcal{T}} t_1) で分岐した場合 xv|x| - |v| が減少せず、一見すると問題になりそうです。 ですが xv=1|x| - |v| = 1 ということは v=x1v = x_1 となっていて t1q1t_1 \rightsquigarrow q_1 のため access(q1)<x1|\mathrm{access}(q_1)| < |x_1| になるため xx の文字数が減少します。

さらに、この分岐で xxaccess(q1)  x2\mathrm{access}(q_1)\;x_2 としたときに x2x_2 が短すぎると、そのあと xx の接頭辞で δT(q0T,v)F\delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F となる vv が見つからないという事態が起こりそうにも思えます。 しかし、実際にはそのようなことは起こりません。 なぜなら δT(q0T,access(q1)  x2)B\delta^\mathcal{T}(q_0^\mathcal{T}, \mathrm{access}(q_1)\;x_2) \in B だとすると q=t2q = t_2 のため、明らかに先程示した q#Tt2q \mathrel{\#_\mathcal{T}} t_2 と矛盾するからです。

よってProcCounterExは正しく動作します。

実装

最後に、ここまで説明してきた L#L^\# をScalaで実装したものを示します。 空行を含めて280行程度のプログラムで、そこそこコンパクトに実装できているのではないかと思います。

import scala.annotation.tailrec
import scala.collection.mutable
import scala.util.boundary
 
final case class Mealy[Q, I, O](
    initial: Q,
    transition: Map[(Q, I), (O, Q)]
):
  def run(is: Seq[I]): (Seq[O], Q) =
    val os = Seq.newBuilder[O]
    var q = initial
    for i <- is do
      val (o, q1) = transition((q, i))
      os.addOne(o)
      q = q1
    (os.result(), q)
 
trait SUL[I, O]:
  def trace(is: Seq[I]): Seq[O]
 
  def findCounterEx(h: Mealy[?, I, O]): Option[Seq[I]]
 
  def inputAlphabet: Set[I]
 
  def outputAlphabet: Set[O]
 
final case class OTree[I, O](
    edges: Map[I, (O, OTree[I, O])] = Map.empty[I, (O, OTree[I, O])]
):
  def contains(is: Seq[I]): Boolean = get(is).isDefined
 
  def apply(is: Seq[I]): OTree[I, O] = get(is).get
 
  def get(is: Seq[I]): Option[OTree[I, O]] =
    is.headOption match
      case None    => Some(this)
      case Some(i) => edges.get(i).flatMap(_._2.get(is.tail))
 
  def inserted(ios: Seq[(I, O)]): OTree[I, O] =
    ios.headOption match
      case None => this
      case Some((i, o)) =>
        edges.get(i) match
          case None =>
            val t = OTree(Map.empty).inserted(ios.tail)
            OTree(edges ++ Map(i -> (o, t)))
          case Some((_, t)) =>
            OTree(edges ++ Map(i -> (o, t.inserted(ios.tail))))
 
  infix def apart(that: OTree[I, O]): Option[Seq[I]] =
    val queue = mutable.Queue.empty[(Seq[I], OTree[I, O], OTree[I, O])]
    queue.enqueue((Seq.empty, this, that))
    boundary:
      while queue.nonEmpty do
        val (is, t1, t2) = queue.dequeue
        for
          i <- t1.edges.keySet ++ t2.edges.keySet
          ((o1, t1), (o2, t2)) <- t1.edges.get(i) zip t2.edges.get(i)
        do
          if o1 != o2 then boundary.break(Some(is ++ Seq(i)))
          else queue.enqueue((is ++ Seq(i), t1, t2))
      None
 
  infix def ##(that: OTree[I, O]): Boolean =
    (this apart that).isDefined
 
final class LSharp[I, O](val sul: SUL[I, O]):
  type S = Seq[I]
 
  var root: OTree[I, O] = OTree()
 
  val basis = mutable.Set.empty[S]
  val frontier = mutable.Map.empty[S, Set[S]]
 
  val witnessCache = mutable.Map.empty[(S, S), Seq[I]]
 
  def learn(): Mealy[S, I, O] =
    basis.add(Seq.empty)
 
    while true do
      updateFrontier()
 
      if !(promotion() || completion() || identification()) then
        val h = checkHypothesis()
        if h.isDefined then return h.get
 
    sys.error("unreachable")
 
  private def outputQuery(is: Seq[I]): Unit =
    if root.contains(is) then return
 
    val os = sul.trace(is)
    root = root.inserted(is.zip(os))
 
  private def addBasis(t: S): Unit =
    basis.add(t)
    val tt = root(t)
    frontier.mapValuesInPlace: (s, ts) =>
      val st = root(s)
      if !(tt ## st) then ts ++ Set(t)
      else ts
 
  private def addFrontier(s: S): Unit =
    val st = root(s)
    val ts = basis.iterator.filter: t =>
      val tt = root.get(t).get
      !(tt ## st)
    frontier(s) = ts.toSet
 
  private def updateFrontier(): Unit =
    frontier.mapValuesInPlace: (s, ts) =>
      val st = root(s)
      ts.filter: t =>
        val tt = root(t)
        !(tt ## st)
 
  private def buildHypothesis(): Mealy[S, I, O] =
    val transition = Map.newBuilder[(S, I), (O, S)]
    val initial = Seq.empty[I]
 
    for t <- basis do
      val tt = root(t)
      for (i, (o, _)) <- tt.edges do
        var t1 = t ++ Seq(i)
        if frontier.contains(t1) then t1 = frontier(t1).head
        transition.addOne((t, i), (o, t1))
 
    Mealy(initial, transition.result())
 
  private def checkConsistency(h: Mealy[S, I, O]): Option[S] =
    val queue = mutable.Queue.empty[(S, OTree[I, O], S)]
    queue.enqueue((Seq.empty, root, h.initial))
 
    while queue.nonEmpty do
      val (u, tt, q) = queue.dequeue()
      val qt = root(q)
      (tt apart qt) match
        case None =>
          for (i, (_, tt1)) <- tt.edges do
            val q1 = h.transition((q, i))._2
            queue.addOne((u ++ Seq(i), tt1, q1))
        case Some(_) => return Some(u)
 
    None
 
  private def computeWitness(t1: S, t2: S): Seq[I] =
    witnessCache.getOrElseUpdate((t1, t2), (root(t1) apart root(t2)).get)
 
  private def promotion(): Boolean =
    val isolatedStates = frontier.iterator
      .filter(_._2.isEmpty)
      .map(_._1)
      .toSeq
 
    if isolatedStates.isEmpty then return false
 
    val s = isolatedStates.head
    frontier.remove(s)
    addBasis(s)
 
    true
 
  private def completion(): Boolean =
    val incompletePairs = basis.iterator
      .flatMap(q => sul.inputAlphabet.map((q, _)))
      .filter: (t, i) =>
        val s = t ++ Seq(i)
        !root.contains(s) || !basis.contains(s) && !frontier.contains(s)
      .toSeq
 
    if incompletePairs.isEmpty then return false
 
    for (t, i) <- incompletePairs do
      val s = t ++ Seq(i)
      outputQuery(s)
      addFrontier(s)
 
    true
 
  private def identification(): Boolean =
    val unidentifiedStates = frontier.keys
      .filter(p => frontier(p).size >= 2)
      .toSeq
 
    if unidentifiedStates.isEmpty then return false
 
    val s = unidentifiedStates.head
    val Seq(t1, t2) = frontier(s).take(2).toSeq
    val w = computeWitness(t1, t2)
    outputQuery(s ++ w)
 
    true
 
  private def checkHypothesis(): Option[Mealy[S, I, O]] =
    val h = buildHypothesis()
 
    val x = checkConsistency(h).orElse:
      sul
        .findCounterEx(h)
        .map: y =>
          outputQuery(y)
          var (tt, q) = (root, h.initial)
          val n = (0 until y.length).find: n =>
            val i = y(n)
            tt = tt.edges(i)._2
            q = h.transition((q, i))._2
            val qt = root(q)
            (tt apart qt).isDefined
          y.slice(0, n.get + 1)
 
    if x.isEmpty then return Some(h)
 
    procCounterEx(h, x.get)
    None
 
  private def procCounterEx(h: Mealy[S, I, O], x0: Seq[I]): Unit =
    var x = x0
    var v = frontier.keySet.find(s => x.startsWith(s)).get
 
    while v.size < x.size do
      val q = h.run(x)._2
      val tt = root(x)
      val w = (root(q) apart tt).get
 
      val l = v.size + Math.floorDiv(x.size - v.size, 2)
      val x1 = x.slice(0, l)
      val x2 = x.slice(l, x.size)
 
      val q1 = h.run(x1)._2
      val tt1 = root(x1)
      outputQuery(q1 ++ x2 ++ w)
 
      if (root(q1) apart tt1).isDefined then x = x1
      else
        x = q1 ++ x2
        v = frontier.keySet.find(s => x.startsWith(s)).get
 
@main
def main(): Unit =
  val traceCache = mutable.Map.empty[Seq[Char], Seq[Int]]
  var countFindCounterEx = 0
 
  val sul = new SUL[Char, Int]:
    def run(is: Seq[Char]): Int =
      if is == Seq('a') then 1
      else if is.count(_ == 'b') % 2 == 0 && is.last == 'b' then 1
      else 0
 
    def traceImpl(is: Seq[Char]): Seq[Int] =
      (1 to is.length).map: n =>
        val is1 = is.slice(0, n)
        run(is1)
 
    def trace(is: Seq[Char]): Seq[Int] =
      traceCache.getOrElseUpdate(is, traceImpl(is))
 
    def findCounterEx(h: Mealy[?, Char, Int]): Option[Seq[Char]] =
      countFindCounterEx += 1
      (0 to 2048).iterator
        .map(_.toBinaryString.replaceAll("0", "a").replaceAll("1", "b").toSeq)
        .flatMap(u => Seq(u, u.reverse))
        .find: u =>
          h.run(u)._1 != traceImpl(u)
 
    def inputAlphabet: Set[Char] = Set('a', 'b')
    def outputAlphabet: Set[Int] = Set(0, 1)
 
  val learner = new LSharp[Char, Int](sul)
  val h = learner.learn()
 
  println(h)
  println()
  println(s"#STATE = ${h.transition.size / sul.inputAlphabet.size}")
 
  println()
  println(s"#MEMBER = ${traceCache.size}")
  println(s"#EQUIV = ${countFindCounterEx}")

重要な点についていくつか説明します。

  • OTree (observation tree) をMealy機械の派生ではなく、独自のクラスとして実装しています。またOTreeはimmutableなデータ構造としています。
  • basisfrontierではOTreeの状態 (部分木) を保持するのではなく、木の状態へとアクセスする文字列を保持するようにしています。
  • frontierはfrontier集合に含まれる状態から、まだ区別できていないbasis集合の状態へのMapになっています。つまり、解説の FF\rightsquigarrow を組み合わせたような値になっています。

あとは大体解説をそのままコードに落とし込んだようになっていると思います。

あとがき

今回は最新のオートマトン学習アルゴリズムである L#L^\# について説明しました。

ProcCounterExについてが、自分にとっては引っ掛かりの多い部分だったように思います。 正しさ自体は理解できるのですが、Rivest-Schapireに対する線形探索のような、より単純な方法が結局最後までイメージできなかったのが悔しいところです。 相当賢いアイディアになっているのは分かるのですが、abstract counterexample analysis ([Isberner & Steffen, 2014])のようなフレームワークを確立している LL^\ast と比べると、それほど洗練されているわけではないということを感じます。

また、今回は省いたのですが、ADS (adaptive distinguish sequence) というものを用いてoutput queryの回数を減らす、といったアイディアも論文では説明しています。

observation treeを使ったオートマトン学習というアイディアは L#L^\# が初出というわけではなく[Soucha, 2020]が先行研究としてあるようです。 またVaandragerは L#L^\# を様々なオートマトンの拡張へと対応させる方向で研究を進めているようで、直近では [\Véronique et al., 2024] でtimedオートマトンへの対応を発表しています。

他のアルゴリズムも実装してみてoutput queryやequivalence queryの回数を比較してみたいです。

最後まで目を通していただきありがとうございました。

参考文献

[Vaandrager et al., 2022]:

Vaandrager, Frits, et al. "A new approach for active automata learning based on apartness." International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer International Publishing, 2022.

https://link.springer.com/chapter/10.1007/978-3-030-99524-9_12

[Isberner & Steffen, 2014]:

Isberner, Malte, and Bernhard Steffen. "An abstract framework for counterexample analysis in active automata learning." International Conference on Grammatical Inference. PMLR, 2014.

https://proceedings.mlr.press/v34/isberner14a

[Soucha, 2020]

Soucha, Michal, and Kirill Bogdanov. "Observation tree approach: active learning relying on testing." The Computer Journal 63.9 (2020): 1298-1310.

https://academic.oup.com/comjnl/article/63/9/1298/5525443

[Véronique et al., 2024]:

Bruyère, Véronique, et al. "Active Learning of Mealy Machines with Timers." arXiv preprint arXiv:2403.02019 (2024).

https://arxiv.org/abs/2403.02019

脚注

  1. つまり、Mealy機械 M\mathcal{M} がcompleteなら、co-transitivityも満たしている、ということでもあります。

  2. 説明を論文の内容に合わせるためにこのようにしていますが、T\mathcal{T} の方の状態がbasis集合かfrontier集合の状態である間は ¬(t#Tq)\lnot (t \mathrel{\#_\mathcal{T}} q) のはずなので、frontier集合の先の状態から始めた方が効率的なのではないかと考えています。

  3. 実のところ、このアルゴリズムは論文のものとは、再帰関数を明示的な繰り返しにするなど、かなり異なった書き方になっています。ですが本質的な処理は論文のものと変わらないはずです。また、論文では停止条件を δT(q0T,x)BF\delta^\mathcal{T}(q_0^\mathcal{T}, x) \in B \cup F としていましたが、後述の理由から δT(q0T,x)B\delta^\mathcal{T}(q_0^\mathcal{T}, x) \in B となることは無いため BB を省いて δT(q0T,x)F\delta^\mathcal{T}(q_0^\mathcal{T}, x) \in F としています。