L # L^\# L # というオートマトン学習のアルゴリズムがあります。
2022年にVaandrager らによって提案された、最新のオートマトン学習のアルゴリズムです。
apartness relation という概念を用いて、よく知られているAngluinの L ∗ L^\ast L ∗ とは少し違ったアイディアでオートマトンの学習を実現します。
学習に用いるデータ構造として、従来のobservation tableやdiscrimination treeではなく、observation tree というmembership query (output query) のキャッシュのようなものを利用するのも特徴です。
この記事では L # L^\# L # の詳細や実装について、論文 [Vaandrager et al., 2022] を参考に解説します。
想定読者 : オートマトン理論やオートマトン学習について理解・関心がある。
L # L^\# 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 # L^\# L # はオートマトン学習 (automata learning) のアルゴリズムの一つで、次のような特徴があります。
Angluinの L ∗ L^\ast L ∗ とは異なり、apartness relation という「ある状態とある状態が (学習対象のオートマトンで) 異なる状態を表している」ことを表す関係 # \# # を導入する。
従来のobservation tableやdiscrimination treeではなく、observation tree というmembership query (output query) のキャッシュに似たデータ構造を用いる。
計算量の観点で見ても、オートマトン学習ではmembership queryの回数が O ( k n 2 + n log m ) \mathcal{O}(k n^2 + n \log m) O ( k n 2 + n log m ) (k k k はアルファベットの大きさ、n n n は学習したオートマトンの状態数、m m m は反例の長さの最大値) となることがベストであると考えられているのですが、L # L^\# L # はRivest-SchapireやTTTと同様にこの計算量に収まっています。
また[Vaandrager et al., 2022] の実験でも、既存のアルゴリズムと比較して遜色ない性能が示されていました。
このように L # L^\# L # は今最も注目のオートマトン学習アルゴリズムなのではないかと思います。
準備
集合 A A A について、A ∗ A^\ast A ∗ は A A A の要素からなる (文字) 列の全体からなる集合を表します。
u ∈ A ∗ u \in A^\ast u ∈ A ∗ の長さは ∣ u ∣ |u| ∣ u ∣ と書きます。
ε \varepsilon ε は長さ 0 0 0 の列 (空列 、空文字列 ) を表し、文脈に応じて a ∈ A a \in A a ∈ A を長さ 1 1 1 の列と見做すこともあります。
2つの列 u 1 ∈ A ∗ , u 2 ∈ A ∗ u_1 \in A^\ast,\, u_2 \in A^\ast u 1 ∈ A ∗ , u 2 ∈ A ∗ について、u 1 u 2 u_1 u_2 u 1 u 2 を2つの文字列を並べたもの (連接) を表すものとします。
f : A ⇀ B f\colon A \rightharpoonup B f : A ⇀ B は A A A から B B B への部分関数です。
このとき a ∈ A a \in A a ∈ A について f ( a ) f(a) f ( a ) が定義されているとき f ( a ) ↓ f(a)\!\!\downarrow f ( a ) ↓ と書き、f ( a ) f(a) f ( a ) が定義されていないとき f ( a ) ↑ f(a)\!\!\uparrow f ( a ) ↑ と書きます。
L # L^\# L # は論文ではMealy機械を学習するアルゴリズムとして提案されています。
そこでMealy機械について定義します。
定義 (Mealy機械 ):
Mealy機械 M \mathcal{M} M は5タプル ( I , O , Q , q 0 , δ , λ ) (I, O, Q, q_0, \delta, \lambda) ( I , O , Q , q 0 , δ , λ ) のことで、それぞれ次のような値となります。
I I I は入力のアルファベット、O O O は出力のアルファベット、
Q Q Q は状態の有限集合、q 0 ∈ Q q_0 \in Q q 0 ∈ Q は初期状態、
δ \delta δ と λ \lambda λ はそれぞれ部分関数で、δ : Q × I ⇀ Q \delta\colon Q \times I \rightharpoonup Q δ : Q × I ⇀ Q は遷移関数を、δ : Q × I → O \delta\colon Q \times I \to O δ : Q × I → O は出力関数を表し、δ ( q , i ) ↓ ⟺ λ ( q , i ) ↓ \delta(q, i)\!\!\downarrow \iff \lambda(q, i)\!\!\downarrow δ ( q , i ) ↓ ⟺ λ ( q , i ) ↓ とします。
参照しているMealy機械を明示するために上付き文字を付けて Q M , q 0 M , δ M , λ M Q^\mathcal{M}, q_0^\mathcal{M}, \delta^\mathcal{M}, \lambda^\mathcal{M} Q M , q 0 M , δ M , λ M のように書くことがあります。
δ \delta δ がすべての q ∈ Q , i ∈ I q \in Q,\,i \in I q ∈ Q , i ∈ I について定義されているとき、M \mathcal{M} M はcomplete と言います。
δ \delta δ は文字列について δ ( q , ε ) = q , δ ( q , i u ) = δ ( δ ( q , i ) , u ) \delta(q, \varepsilon) = q,\,\delta(q, i u) = \delta(\delta(q, i), u) δ ( q , ε ) = q , δ ( q , i u ) = δ ( δ ( q , i ) , u ) (i ∈ I , u ∈ I ∗ i \in I,\, u \in I^\ast i ∈ I , u ∈ I ∗ ) として拡張されます。
加えて、λ \lambda λ は文字列について λ ( q , ε ) = ε , λ ( q , i u ) = λ ( q , i ) λ ( δ ( q , i ) , u ) \lambda(q, \varepsilon) = \varepsilon,\,\lambda(q, i u) = \lambda(q, i) \lambda(\delta(q, i), u) λ ( q , ε ) = ε , λ ( q , i u ) = λ ( q , i ) λ ( δ ( q , i ) , u ) として拡張されます。
状態 q ∈ Q q \in Q q ∈ Q について L ( q ) = { u ∈ I ∗ ∣ δ ( q , u ) ↓ } \mathcal{L}(q) = \{ u \in I^\ast \mid \delta(q, u)\!\!\downarrow \} L ( q ) = { u ∈ I ∗ ∣ δ ( q , u ) ↓ } と定義します。
さらに ⟦ q ⟧ : L ( q ) → O ∗ \llbracket q \rrbracket\colon \mathcal{L}(q) \to O^\ast [ [ q ] ] : L ( q ) → O ∗ を ⟦ q ⟧ ( w ) = λ ( q , u ) \llbracket q \rrbracket(w) = \lambda(q, u) [ [ q ] ] ( w ) = λ ( q , u ) と定義します。
2つの状態 q 1 , q 2 q_1, q_2 q 1 , q 2 について ⟦ q 1 ⟧ = ⟦ q 2 ⟧ \llbracket q_1 \rrbracket = \llbracket q_2 \rrbracket [ [ q 1 ] ] = [ [ q 2 ] ] のとき q 1 ≈ q 2 q_1 \approx q_2 q 1 ≈ q 2 と書きます。
定義 (Mealy機械の等価性 ):
2つのMealy機械 M , N \mathcal{M},\,\mathcal{N} M , N について、q 0 M ≈ q 0 N q_0^\mathcal{M} \approx q_0^\mathcal{N} q 0 M ≈ q 0 N のとき M \mathcal{M} M と N \mathcal{N} N は等価 である、と言います。
最後に、Mealy機械の学習 の問題について確認します。
次の2種類のクエリを考えます。
O U T P U T ( u ) \mathrm{OUTPUT}(u) OUTPUT ( u ) (output query ): 文字列 u ∈ I ∗ u \in I^\ast u ∈ I ∗ に対して、学習対象のMealy機械での出力列を返すクエリです。
E Q U I V ( H ) \mathrm{EQUIV}(\mathcal{H}) EQUIV ( H ) (equivalence query ): 仮説のMealy機械 H \mathcal{H} H が学習対象のMealy機械と等価か確認し、等価な場合は y e s \mathbf{yes} yes を、等価でない場合は反例となる文字列 v ∈ I ∗ v \in I^\ast v ∈ I ∗ (つまり、λ H ( q 0 H , v ) ≠ O U T P U T ( v ) \lambda^\mathcal{H}(q_0^\mathcal{H}, v) \ne \mathrm{OUTPUT}(v) λ H ( q 0 H , v ) = OUTPUT ( v ) ) を返します。
これらのクエリが与えられて、学習対象のオートマトンと等価なMealy機械 H \mathcal{H} H (つまり E Q U I V ( H ) = y e s \mathrm{EQUIV}(\mathcal{H}) = \mathbf{yes} EQUIV ( H ) = yes となる H \mathcal{H} H ) を求めるのがMealy機械の学習となります。
observation tree
まず L # L^\# L # で重要なデータ構造となるobservation treeについて説明します。
observation tree はMealy機械の一種として定義されます。
定義 (observation tree ):
Mealy機械 T = ( I , O , Q , q 0 , δ , λ ) \mathcal{T} = (I, O, Q, q_0, \delta, \lambda) T = ( I , O , Q , q 0 , δ , λ ) がtree であるとは、各状態 q ∈ Q q \in Q q ∈ Q についてユニークな文字列 u ∈ I ∗ u \in I^\ast u ∈ I ∗ が存在して δ ( q 0 , u ) = q \delta(q_0, u) = q δ ( q 0 , u ) = q を満たすことを言います。
このユニークな文字列 u u u を a c c e s s ( q ) \mathrm{access}(q) access ( q ) と書きます。
Mealy機械 M \mathcal{M} M に対して、すべての文字列 u ∈ L ( q 0 T ) u \in \mathcal{L}(q_0^\mathcal{T}) u ∈ L ( q 0 T ) について ⟦ q 0 T ⟧ ( u ) = ⟦ q 0 M ⟧ ( u ) \llbracket q_0^\mathcal{T} \rrbracket(u) = \llbracket q_0^\mathcal{M} \rrbracket(u) [ [ q 0 T ] ] ( u ) = [ [ q 0 M ] ] ( u ) であるとき、T \mathcal{T} T は M \mathcal{M} M のobservation tree であると呼びます。
次のようなMealy機械 M 1 \mathcal{M}_1 M 1 があったとします。
このMealy機械に対するobservation treeとして、例えば次のようなMealy機械 T 1 \mathcal{T}_1 T 1 が考えられます。
このとき a c c e s s ( q ) \mathrm{access}(q) access ( q ) の値は、例えば a c c e s s ( t 2 ) = a a , a c c e s s ( t 7 ) = b b a \mathrm{access}(t_2) = aa,\, \mathrm{access}(t_7) = bba access ( t 2 ) = aa , access ( t 7 ) = bba です。
observation treeはMealy機械の入力と出力を平坦に (状態の構造を忘れて) 記録したものだと考えられます。
つまり、observation treeは O U T P U T ( u ) \mathrm{OUTPUT}(u) OUTPUT ( u ) のキャッシュそのものと捉えられます。
同じ文字列に対して O U T P U T ( u ) \mathrm{OUTPUT}(u) OUTPUT ( u ) を呼び出すのは無駄なので、キャッシュするのは自然な考えです。
「自然に記録している値を用いて学習が出来る 」のが L # L^\# L # の強みの1つというわけです。
apartness relation
次に L # L^\# L # で重要となるapartness relation の概念について説明します。
apartness relation は構成主義の数学で用いられる道具で、Brouwer によって導入されHeyting によって公理化されました。
apartness relationは # \# # の記号で書かれ、通常の不等号 ≠ \ne = とは区別されます。
apartness relation # \# # は次の公理を見たす2項関係です。
¬ ( x # x ) \lnot (x \mathrel{\#} x) ¬ ( x # x ) (irreflexivity )
x # y ⇒ y # x x \mathrel{\#} y \Rightarrow y \mathrel{\#} x x # y ⇒ y # x (symmetricity )
x # y ⇒ x # z ∨ y # z x \mathrel{\#} y \Rightarrow x \mathrel{\#} z \lor y \mathrel{\#} z x # y ⇒ x # z ∨ y # z (co-transitivity )
Mealy機械 M \mathcal{M} M について、次のようなapartness relationを定義できます。
定義 (M \mathcal{M} M 上の (weak) apartness relation ):
Mealy機械 M \mathcal{M} M について、M \mathcal{M} M 上の (weak) apartness relation # M ⊆ Q M × Q M \#_\mathcal{M} \subseteq Q^\mathcal{M} \times Q^\mathcal{M} # M ⊆ Q M × Q M を次のように定義します。
q 1 # M q 2 ⟺ ∃ u ∈ L ( q 1 ) ∩ L ( q 2 ) . λ M ( q 1 , u ) ≠ λ M ( q 2 , u ) q_1 \mathrel{\#_\mathcal{M}} q_2 \iff \exists u \in \mathcal{L}(q_1) \cap \mathcal{L}(q_2).\ \lambda^\mathcal{M}(q_1, u) \ne \lambda^\mathcal{M}(q_2, u) q 1 # M q 2 ⟺ ∃ u ∈ L ( q 1 ) ∩ L ( q 2 ) . λ M ( q 1 , u ) = λ M ( q 2 , u ) 加えて、q 1 , q 2 ∈ Q M q_1, q_2 \in Q^\mathcal{M} q 1 , q 2 ∈ Q M について q 1 # M q 2 q_1 \mathrel{\#_\mathcal{M}} q_2 q 1 # M q 2 のとき、w i t n e s s ( q 1 , q 2 ) ∈ L ( q 1 ) ∩ L ( q 2 ) \mathrm{witness}(q_1, q_2) \in \mathcal{L}(q_1) \cap \mathcal{L}(q_2) witness ( q 1 , q 2 ) ∈ L ( q 1 ) ∩ L ( q 2 ) を λ ( q 1 , u ) ≠ λ ( q 2 , u ) \lambda(q_1, u) \ne \lambda(q_2, u) λ ( q 1 , u ) = λ ( q 2 , u ) となる文字列 u u u と定義します。
このapartness relationはirreflexivity とsymmetricity を満たしますが、co-transitivity を満たさない場合があります。
Mealy機械 M \mathcal{M} M がcompleteでない場合、q 1 # M q 2 q_1 \mathrel{\#_\mathcal{M}} q_2 q 1 # M q 2 でも δ ( q , w i t n e s s ( q 1 , q 2 ) ) ↑ \delta(q, \mathrm{witness}(q_1, q_2))\!\!\uparrow δ ( q , witness ( q 1 , q 2 )) ↑ のとき、q 1 # M q q_1 \mathrel{\#_\mathcal{M}} q q 1 # M q とも q 2 # M q q_2 \mathrel{\#_\mathcal{M}} q q 2 # M q とも言えない可能性があるからです1 。
例えば、上の T 1 \mathcal{T}_1 T 1 では t 1 # T 1 t 5 t_1 \mathrel{\#_{\mathcal{T}_1}} t_5 t 1 # T 1 t 5 で w i t n e s s ( t 1 , t 5 ) = b \mathrm{witness}(t_1, t_5) = b witness ( t 1 , t 5 ) = b ですが、δ ( t 2 , b ) ↑ \delta(t_2, b)\!\!\uparrow δ ( t 2 , b ) ↑ のため t 1 # T 1 t 2 t_1 \mathrel{\#_{\mathcal{T}_1}} t_2 t 1 # T 1 t 2 とも t 5 # T 1 t 2 t_5 \mathrel{\#_{\mathcal{T}_1}} t_2 t 5 # T 1 t 2 とも言えません。
Mealy機械 M \mathcal{M} M のobservation tree T \mathcal{T} T について、T \mathcal{T} T 上のapartness relation # T \#_\mathcal{T} # T は、M \mathcal{M} M と次のような関係があります。
補題1 :
Mealy機械 M \mathcal{M} M のobservation tree T \mathcal{T} T について t 1 # T t 2 t_1 \mathrel{\#_\mathcal{T}} t_2 t 1 # T t 2 (t 1 , t 2 ∈ Q T t_1, t_2 \in Q^\mathcal{T} t 1 , t 2 ∈ Q T ) の場合を考えます。
ここで q 1 = δ M ( q 0 M , a c c e s s ( t 1 ) ) , q 2 = δ M ( q 0 M , a c c e s s ( t 2 ) ) q_1 = \delta^\mathcal{M}(q_0^\mathcal{M}, \mathrm{access}(t_1)),\, q_2 = \delta^\mathcal{M}(q_0^\mathcal{M}, \mathrm{access}(t_2)) q 1 = δ M ( q 0 M , access ( t 1 )) , q 2 = δ M ( q 0 M , access ( t 2 )) とおくと、q 1 ≉ q 2 q_1 \not\approx q_2 q 1 ≈ q 2 が成り立ちます。
observation treeが (定義されている範囲で) 元のMealy機械の出力と等しいことから、このことはすぐに分かります。
この補題から、observation treeのapartness relationを考えることで、状態の組が少なくとも学習対象のMealy機械でも異なる状態の組を表している、ということが分かります。
Mealy機械 M \mathcal{M} M 上のapartness relationについて、co-transitivityを満たさない場合があると定義した際に述べました。
しかし、次のweak co-transitivity であれば常に成り立ちます。
補題2 (weak co-transitivity ): Mealy機械 M \mathcal{M} M の状態 q , t 1 , t 2 ∈ Q M q, t_1, t_2 \in Q^\mathcal{M} q , t 1 , t 2 ∈ Q M について、次の命題が成り立ちます。
t 1 # M t 2 ∧ δ M ( q , w i t n e s s ( t 1 , t 2 ) ) ↓ ⇒ t 1 # M q ∨ t 2 # M q t_1 \mathrel{\#_\mathcal{M}} t_2 \land \delta^\mathcal{M}(q, \mathrm{witness}(t_1, t_2))\!\!\downarrow
\Rightarrow t_1 \mathrel{\#_\mathcal{M}} q \lor t_2 \mathrel{\#_\mathcal{M}} q t 1 # M t 2 ∧ δ M ( q , witness ( t 1 , t 2 )) ↓⇒ t 1 # M q ∨ t 2 # M q
問題となる δ M ( q , w i t n e s s ( t 1 , t 2 ) ) ↑ \delta^\mathcal{M}(q, \mathrm{witness}(t_1, t_2))\!\!\uparrow δ M ( q , witness ( t 1 , t 2 )) ↑ の場合を潰した条件になっています。
weak co-transitivityは学習の際に、区別可能な (apartness relationに含まれる) 状態の組を増やすのに役に立ちます。
L # L^\# L # アルゴリズム
ここからは L # L^\# L # のアルゴリズム本体について解説していきます。
これまで説明してきたように L # L^\# L # ではobservation treeを主なデータ構造として利用します。
そして、observation treeはoutput queryのキャッシュとして振舞います。
L # L^\# L # の実行中に管理されるobservation tree T \mathcal{T} T について、output queryの呼び出しによって T \mathcal{T} T が更新されていくことを明示するために、そのようなoutput queryの呼び出しを O U T P U T T ( u ) \mathrm{OUTPUT}_\mathcal{T}(u) OUTPUT T ( u ) と書くことにします。
L # L^\# L # は T \mathcal{T} T に加えて、次の2つの集合と1つの関係 ( B , F , ⇝ ) (B, F, \rightsquigarrow) ( B , F , ⇝ ) を管理しながら実行されます。
B ⊆ Q T B \subseteq Q^\mathcal{T} B ⊆ Q T はbasis集合 で、学習対象のMealy機械と対応付いている状態の集合です。basis集合の2つの状態 t 1 , t 2 ∈ B t_1, t_2 \in B t 1 , t 2 ∈ B について t 1 # T t 2 t_1 \mathrel{\#_\mathcal{T}} t_2 t 1 # T t 2 が成り立ちます。
F ⊆ Q T ∖ B F \subseteq Q^\mathcal{T} \setminus B F ⊆ Q T ∖ B はfrontier集合 で、basis集合に含まれる状態から1文字で遷移できる状態を集めたものです。frontier集合の状態が、basis集合のすべての状態から区別できるようになったとき、その状態はfrontier集合からbasis集合へと移動します。
⇝ ⊆ F × B \rightsquigarrow \subseteq F \times B ⇝ ⊆ F × B はfrontier集合の状態から、まだ区別できていないbasis集合の状態への写像である関係です。⇝ = { ( s , t ) ∈ F × B ∣ ¬ ( s # T t ) } \rightsquigarrow = \{ (s, t) \in F \times B \mid \lnot (s \mathrel{\#_\mathcal{T}} t) \} ⇝ = {( s , t ) ∈ F × B ∣ ¬ ( s # T t )} を満たすように更新されています。
frontier集合の状態 s ∈ F s \in F s ∈ F について [ s ] ⇝ ⊆ B [s]_\rightsquigarrow \subseteq B [ s ] ⇝ ⊆ B を [ s ] ⇝ = { t ∈ B ∣ s ⇝ t } [s]_\rightsquigarrow = \{ t \in B \mid s \rightsquigarrow t \} [ s ] ⇝ = { t ∈ B ∣ s ⇝ t } と定義します。
仮説のオートマトンの構築
T \mathcal{T} T からの仮説のMealy機械 H \mathcal{H} H の構築の説明のために、いくつか用語を定義します。
定義 (isolated , identified , complete ):
observation tree T \mathcal{T} T と ( B , F , ⇝ ) (B, F, \rightsquigarrow) ( B , F , ⇝ ) について、
frontier集合の状態 s ∈ F s \in F s ∈ F について、∣ [ s ] ⇝ ∣ = 0 |[s]_\rightsquigarrow| = 0 ∣ [ s ] ⇝ ∣ = 0 のとき q q q はisolated であると呼び、∣ [ s ] ⇝ ∣ = 1 |[s]_\rightsquigarrow| = 1 ∣ [ s ] ⇝ ∣ = 1 のとき q q q はidentified であると呼びます。
basis集合の状態 t ∈ B t \in B t ∈ B について、すべての入力文字 i ∈ I i \in I i ∈ I について δ T ( q 0 , a c c e s s ( q ) i ) ↓ \delta^\mathcal{T}(q_0, \mathrm{access}(q)\;i)\!\!\downarrow δ T ( q 0 , access ( q ) i ) ↓ かつ δ T ( q 0 , a c c e s s ( q ) i ) ∈ B ∪ F \delta^\mathcal{T}(q_0, \mathrm{access}(q)\;i) \in B \cup F δ T ( q 0 , access ( q ) i ) ∈ B ∪ F のとき、t t t はcomplete であると呼びます。
frontier集合 F F F のすべての状態がidentifiedのとき F F F はidentified であると呼び、basis集合 B B B のすべての状態がcompleteのとき B B B はcomplete であると呼びます。
これらの用語について、もう少し補足の説明をします。
s ∈ F s \in F s ∈ F がisolated ということは、今学習対象のMealy機械と対応付いているすべての状態と区別されているということです。つまり、isolatedな s s s は新しいbasis集合の状態になれる状態ということです。
s ∈ F s \in F s ∈ F がidentified ということはこれまでに記録した限りでは basis集合の特定の状態と、学習対象のMealy機械上では同じ状態を表していると考えられます。つまり、T \mathcal{T} T で s s s に遷移する場合、仮説のMealy機械 H \mathcal{H} H では s ⇝ t s \rightsquigarrow t s ⇝ t となる t t t に対応する状態へと遷移することになります。
t ∈ B t \in B t ∈ B がcomplete ということは、仮説のMealy機械を構築する際に遷移先の状態が存在せず遷移できないということが起こらないことを意味しています。
例として、observation treeを上の T 1 \mathcal{T}_1 T 1 として B = { t 0 , t 1 } , F = { t 2 , t 3 , t 5 } B = \{ t_0, t_1 \},\, F = \{ t_2, t_3, t_5 \} B = { t 0 , t 1 } , F = { t 2 , t 3 , t 5 } とします。
次の図は、このときの様子を図にしたもので、赤いノードがbasis集合の状態を、緑のノードがfrontier集合の状態を表し、点線の矢印は ⇝ \rightsquigarrow ⇝ の関係を表します。
このとき、
[ t 2 ] ⇝ = { t 0 , t 1 } [t_2]_\rightsquigarrow = \{ t_0, t_1 \} [ t 2 ] ⇝ = { t 0 , t 1 } なので t 2 ∈ F t_2 \in F t 2 ∈ F はisolatedでもidentifiedでもない状態です。
[ t 3 ] ⇝ = { t 1 } [t_3]_\rightsquigarrow = \{ t_1 \} [ t 3 ] ⇝ = { t 1 } なので t 3 ∈ F t_3 \in F t 3 ∈ F はidentifiedな状態です。
[ t 5 ] ⇝ = ∅ [t_5]_\rightsquigarrow = \emptyset [ t 5 ] ⇝ = ∅ なので t 5 ∈ F t_5 \in F t 5 ∈ F はisolatedな状態です。
また、B = { t 0 , t 1 } B = \{ t_0, t_1 \} B = { t 0 , t 1 } は各入力文字 i ∈ { a , b } i \in \{ a, b \} i ∈ { a , b } について遷移先が定義されているため、B B B はcompleteです。
observation tree T \mathcal{T} T から仮説のMealy機械 H \mathcal{H} H の構築は、次のように行います。
定義 (仮説のMealy機械 ):
observation tree T = ( I , O , Q T , q 0 T , δ T , λ T ) \mathcal{T} = (I, O, Q^\mathcal{T}, q_0^\mathcal{T}, \delta^\mathcal{T}, \lambda^\mathcal{T}) T = ( I , O , Q T , q 0 T , δ T , λ T ) と ( B , F , ⇝ ) (B, F, \rightsquigarrow) ( B , F , ⇝ ) について、F F F がidentifiedかつ B B B がcompleteな場合を考えます。
このとき、仮説のMealy機械 H = ( I , O , Q H , q 0 H , δ H , λ H ) \mathcal{H} = (I, O, Q^\mathcal{H}, q_0^\mathcal{H}, \delta^\mathcal{H}, \lambda^\mathcal{H}) H = ( I , O , Q H , q 0 H , δ H , λ H ) は次のように定義されます。
Q H = B Q^\mathcal{H} = B Q H = B 、q 0 H = t 0 q_0^\mathcal{H} = t_0 q 0 H = t 0 、
δ H ( q , i ) = t \delta^\mathcal{H}(q, i) = t δ H ( q , i ) = t (t = δ T ( q , i ) t = \delta^\mathcal{T}(q, i) t = δ T ( q , i ) かつ t ∈ B t \in B t ∈ B の場合)、または δ H ( q , i ) = t ′ \delta^\mathcal{H}(q, i) = t' δ H ( q , i ) = t ′ (s = δ T ( q , i ) ∧ s ∈ F s = \delta^\mathcal{T}(q, i) \land s \in F s = δ T ( q , i ) ∧ s ∈ F かつ s ⇝ t ′ s \rightsquigarrow t' s ⇝ t ′ の場合)、
λ H ( q , i ) = λ T ( q , i ) \lambda^\mathcal{H}(q, i) = \lambda^\mathcal{T}(q, i) λ H ( q , i ) = λ T ( q , i ) 。
F F F がidentifiedかつ B B B がcompleteとしているので、仮説のMealy機械は正しく定義されます。
H \mathcal{H} H と T \mathcal{T} T の一貫性
仮説のMealy機械はfrontier集合までの状態を元に構築しているため、場合によっては H \mathcal{H} H と T \mathcal{T} T が一貫していない 、つまり、ある文字列で区別できる状態に遷移してしまう (δ H ( q 0 H , u ) # T δ T ( q 0 T , u ) \delta^\mathcal{H}(q_0^\mathcal{H}, u) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, u) δ H ( q 0 H , u ) # T δ T ( q 0 T , u ) となる文字列 u ∈ I ∗ u \in I^\ast u ∈ I ∗ が存在する) 場合があります。
このような場合、H \mathcal{H} H は明らかに学習対象のMealy機械と等価ではないので、事前にチェックしておきたいです。
具体的には、次のようなアルゴリズムで、H \mathcal{H} H が T \mathcal{T} T と一貫しているかチェックできます。
Algorithm 1 Check consistency between T \mathcal{T} T and H \mathcal{H} H
function CheckConsistency (H \mathcal{H} H )
q u e u e ← \mathit{queue} \gets queue ← new queue of Q T × Q H Q^\mathcal{T} \times Q^\mathcal{H} Q T × Q H
e n q u e u e ( q u e u e , ( q 0 T , q 0 H ) ) \mathrm{enqueue}(\mathit{queue}, (q_0^\mathcal{T}, q_0^\mathcal{H})) enqueue ( queue , ( q 0 T , q 0 H ))
while q u e u e \mathit{queue} queue is not empty do
( t , q ) ← d e q u e u e ( q u e u e ) (t, q) \gets \mathrm{dequeue}(\mathit{queue}) ( t , q ) ← dequeue ( queue )
if t # T q t \mathrel{\#_\mathcal{T}} q t # T q then
return a c c e s s ( t ) \mathrm{access}(t) access ( t )
else
for i ∈ I ∧ δ T ( t , i ) ↓ i \in I \land \delta^\mathcal{T}(t, i)\!\!\downarrow i ∈ I ∧ δ T ( t , i ) ↓ do
e n q u e u e ( q u e u e , ( δ T ( t , i ) , δ H ( q , i ) ) ) \mathrm{enqueue}(\mathit{queue}, (\delta^\mathcal{T}(t, i), \delta^\mathcal{H}(q, i))) enqueue ( queue , ( δ T ( t , i ) , δ H ( q , i )))
end for
end if
end while
return y e s \mathbf{yes} yes
end function
内容は T \mathcal{T} T の状態と H \mathcal{H} H の状態の組 ( t , q ) (t, q) ( t , q ) を、初期状態から幅優先探索で t # T q t \mathrel{\#_\mathcal{T}} q t # T q となっていないか探索しているだけです2 。
また、返り値は一貫している場合は y e s \mathbf{yes} yes 、一貫していない場合は δ H ( q 0 H , u ) # T δ T ( q 0 T , u ) \delta^\mathcal{H}(q_0^\mathcal{H}, u) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, u) δ H ( q 0 H , u ) # T δ T ( q 0 T , u ) となる文字列 u u u を返します。
こうすることで、比較的重いクエリであるequivalence queryを呼び出す回数を減らせます。
L # L^\# L # のアルゴリズム本体
L # L^\# L # は次のようにして、オートマトンを学習していきます。
T \mathcal{T} T を初期状態 t 0 t_0 t 0 のみのtree、B B B を { t 0 } \{ t_0 \} { t 0 } 、F F F と ⇝ \rightsquigarrow ⇝ を空集合で初期化します。
次の処理を繰り返します。
⇝ \rightsquigarrow ⇝ を T \mathcal{T} T と B , F B, F B , F に合わせて更新します。
promotion : F F F にisolatedな状態 s ∈ F s \in F s ∈ F がある場合、s s s を B B B に移動し、繰り返しをやり直します。
completion : B B B にcompleteでない状態 t ∈ B t \in B t ∈ B がある場合、δ T ( q , i ) ↑ \delta^\mathcal{T}(q, i)\!\!\uparrow δ T ( q , i ) ↑ または δ T ( q , i ) ∉ F \delta^\mathcal{T}(q, i) \notin F δ T ( q , i ) ∈ / F である i ∈ I i \in I i ∈ I について O U T P U T T ( a c c e s s ( t ) i ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(t)\;i) OUTPUT T ( access ( t ) i ) を呼び出し、δ T ( q , i ) \delta^\mathcal{T}(q, i) δ T ( q , i ) を F F F に追加し、繰り返しをやり直します。
identification : F F F にidentifiedでない状態 s ∈ F s \in F s ∈ F がある場合、2つのbasis集合の状態 t 1 , t 2 ∈ [ s ] ⇝ t_1, t_2 \in [s]_\rightsquigarrow t 1 , t 2 ∈ [ s ] ⇝ について O U T P U T T ( a c c e s s ( s ) w i t n e s s ( t 1 , t 2 ) ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(s)\;\mathrm{witness}(t_1, t_2)) OUTPUT T ( access ( s ) witness ( t 1 , t 2 )) を呼び出し、繰り返しをやり直します。
ここからequivalence checking : B B B がcompleteかつ F F F がidentifiedなので、仮説のオートマトン H \mathcal{H} H を構築します。
CheckConsistency ( H ) \text{\htmlClass{katex-ps-funcname}{CheckConsistency}}(\mathcal{H}) CheckConsistency ( H ) を呼び出します。
反例の文字列 x x x を返した場合、x x x を記憶しておきます。
y e s \mathbf{yes} yes を返した場合、E Q U I V ( H ) \mathrm{EQUIV}(\mathcal{H}) EQUIV ( H ) を呼び出します。
反例の文字列 y y y を返した場合、δ H ( q 0 H , x ) # T δ T ( q 0 T , x ) \delta^\mathcal{H}(q_0^\mathcal{H}, x) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, x) δ H ( q 0 H , x ) # T δ T ( q 0 T , x ) となる y y y の接頭辞で最小の x x x を探します。
これも y e s \mathbf{yes} yes を返した場合、H \mathcal{H} H は学習対象のMealy機械と等価なので、それを返して学習を終了します。
反例の文字列 x x x を T \mathcal{T} T に反映する手続き ProcCounterEx ( H , x ) \text{\htmlClass{katex-ps-funcname}{ProcCounterEx}}(\mathcal{H}, x) ProcCounterEx ( H , x ) を呼び出します (この手続きProcCounterEx については後で説明 します)。
つまり、F F F のisolatedな状態を B B B に移動しつつ (promotion)、B B B がcompleteかつ F F F がidentifiedとなるように処理を繰り返し、仮説のMealy機械が作れるようになったら、それを使って CheckConsistency ( H ) \text{\htmlClass{katex-ps-funcname}{CheckConsistency}}(\mathcal{H}) CheckConsistency ( H ) や E Q U I V ( H ) \mathrm{EQUIV}(\mathcal{H}) EQUIV ( H ) を呼び出し、返された反例を T \mathcal{T} T に反映していく、というのが L # L^\# L # の流れになります。
もう少し具体的な疑似コードで説明したものが、次のアルゴリズム (LSharp ) になります。
Algorithm 2 The L # L^\# L # algorithm
function LSharp ()
T ← \mathcal{T} \gets T ← a tree with an intial state t 0 t_0 t 0
B ← { t 0 } B \gets \{ t_0 \} B ← { t 0 } and F ← ∅ F \gets \emptyset F ← ∅
repeat
⇝ ← { ( s , t ) ∈ F × B ∣ ¬ ( s # T t ) } \rightsquigarrow \gets \{ (s, t) \in F \times B \mid \lnot (s \mathrel{\#_\mathcal{T}} t) \} ⇝ ← {( s , t ) ∈ F × B ∣ ¬ ( s # T t )}
if s ∈ F ∧ [ s ] ⇝ = ∅ s \in F \land [s]_\rightsquigarrow = \emptyset s ∈ F ∧ [ s ] ⇝ = ∅ then
B ← B ∪ { s } B \gets B \cup \{ s \} B ← B ∪ { s } and F ← F ∖ { s } F \gets F \setminus \{ s \} F ← F ∖ { s }
continue
end if
if t ∈ B ∧ i ∈ I ∧ ( δ T ( t , i ) ↑ ∨ δ T ( t , i ) ∉ B ∪ F ) t \in B \land i \in I \land (\delta^\mathcal{T}(t, i)\!\!\uparrow \lor \delta^\mathcal{T}(t, i) \notin B \cup F) t ∈ B ∧ i ∈ I ∧ ( δ T ( t , i ) ↑ ∨ δ T ( t , i ) ∈ / B ∪ F ) then
O U T P U T T ( a c c e s s ( t ) i ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(t)\;i) OUTPUT T ( access ( t ) i )
F ← F ∪ { δ T ( t , i ) } F \gets F \cup \{ \delta^\mathcal{T}(t, i) \} F ← F ∪ { δ T ( t , i )}
continue
end if
if s ∈ F ∧ t 1 , t 2 ∈ [ s ] ⇝ s \in F \land t_1, t_2 \in [s]_\rightsquigarrow s ∈ F ∧ t 1 , t 2 ∈ [ s ] ⇝ then
O U T P U T T ( a c c e s s ( s ) w i t n e s s ( t 1 , t 2 ) ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(s)\;\mathrm{witness}(t_1, t_2)) OUTPUT T ( access ( s ) witness ( t 1 , t 2 ))
continue
end if
H ← \mathcal{H} \gets H ← the hypothesis Mealy machine constructed from T \mathcal{T} T and ( B , F , ⇝ ) (B, F, \rightsquigarrow) ( B , F , ⇝ )
x ← x \gets x ← CheckConsistency (H \mathcal{H} H )
if x = y e s x = \mathbf{yes} x = yes then
y ← E Q U I V ( H ) y \gets \mathrm{EQUIV}(\mathcal{H}) y ← EQUIV ( H )
if y ≠ y e s y \ne \mathbf{yes} y = yes then
O U T P U T T ( y ) \mathrm{OUTPUT}_\mathcal{T}(y) OUTPUT T ( y )
x ← x \gets x ← the shortest prefix of y y y s.t. δ T ( q 0 T , x ) # T δ H ( q 0 H , x ) \delta^\mathcal{T}(q_0^\mathcal{T}, x) \mathrel{\#_\mathcal{T}} \delta^\mathcal{H}(q_0^\mathcal{H}, x) δ T ( q 0 T , x ) # T δ H ( q 0 H , x )
end if
end if
if x ≠ y e s x \ne \mathbf{yes} x = yes then
ProcCounterEx (H , x \mathcal{H}, x H , x )
end if
until E Q U I V ( H ) = y e s \mathrm{EQUIV}(\mathcal{H}) = \mathbf{yes} EQUIV ( H ) = yes
return H \mathbf{H} H
end function
promotionやcompletionでは B B B や F F F が変化するので、学習が進んでいることが分かります。
また、identificationではweak co-transitivity (補題2) により、このあとの ⇝ \rightsquigarrow ⇝ の更新で ∣ [ s ] ⇝ ∣ |[s]_\rightsquigarrow| ∣ [ s ] ⇝ ∣ が小さくなるため、同様に学習が進みます。
promotion、completion、identificationでの O U T P U T ( u ) \mathrm{OUTPUT}(u) OUTPUT ( u ) の呼び出し回数は、identificationでのものが支配的です。
k = ∣ I ∣ , n = ∣ B ∣ k = |I|,\, n = |B| k = ∣ I ∣ , n = ∣ B ∣ とすると、∣ F ∣ |F| ∣ F ∣ の大きさは k n k n kn で抑えられて、各 s ∈ F s \in F s ∈ F について [ s ] ⇝ [s]_\rightsquigarrow [ s ] ⇝ の大きさは高々 n n n のため、identificationでの O U T P U T ( w ) \mathrm{OUTPUT}(w) OUTPUT ( w ) の呼び出し回数は O ( k n 2 ) \mathcal{O}(k n^2) O ( k n 2 ) で抑えられます。
後述するように、 ProcCounterEx ( H , x ) \text{\htmlClass{katex-ps-funcname}{ProcCounterEx}}(\mathcal{H}, x) ProcCounterEx ( H , x ) は反例の文字列の長さ m = ∣ x ∣ m = |x| m = ∣ x ∣ について O ( log m ) \mathcal{O}(\log m) O ( log m ) 回の O U T P U T ( u ) \mathrm{OUTPUT}(u) OUTPUT ( u ) の呼び出し回数で実現できます。
ProcCounterEx ( H , x ) \text{\htmlClass{katex-ps-funcname}{ProcCounterEx}}(\mathcal{H}, x) ProcCounterEx ( H , x ) の呼び出し回数は高々 n n n 回なので、全体での O U T P U T ( w ) \mathrm{OUTPUT}(w) OUTPUT ( w ) の呼び出し回数は O ( k n 2 + n log m ) \mathcal{O}(k n^2 + n \log m) O ( k n 2 + n log m ) で抑えられます。
計算量についての詳細な解析は論文を参照してください。
反例の処理
最後に、反例の処理を行うProcCounterEx について説明します。
反例の処理は新しい状態が増えることを目標とします。
L # L^\# L # において新しい状態が増えるとは、F F F の状態が B B B へと移動する (promotion) ことを意味します。
そして、promotionが行なわれるためには、その F F F の状態がisolatedにならなければいけません。
仮説のオートマトンを構築した段階では、frontier集合の状態 s ∈ F s \in F s ∈ F はすべてidentifiedなのでs ⇝ t s \rightsquigarrow t s ⇝ t となる t ∈ B t \in B t ∈ B が1つ存在しています。
そのためProcCounterEx では、その中のO U T P U T T ( u ) \mathrm{OUTPUT}_\mathcal{T}(u) OUTPUT T ( u ) の呼び出しで、ある t ∈ F t \in F t ∈ F が s # T t s \mathrel{\#_\mathcal{T}} t s # T t となるように T \mathcal{T} T が更新されればいいわけです。
ProcCounterEx は次のようなアルゴリズムになります3 。
Algorithm 3
procedure ProcCounterEx (H , x \mathcal{H}, x H , x )
v ← v \gets v ← the unique prefix of x x x s.t. δ T ( q 0 T , v ) ∈ F \delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F δ T ( q 0 T , v ) ∈ F
while ∣ v ∣ < ∣ x ∣ |v| < |x| ∣ v ∣ < ∣ x ∣ do
q ← δ H ( q 0 H , x ) q \gets \delta^\mathcal{H}(q_0^\mathcal{H}, x) q ← δ H ( q 0 H , x ) and t ← δ T ( q 0 T , x ) t \gets \delta^\mathcal{T}(q_0^\mathcal{T}, x) t ← δ T ( q 0 T , x )
w ← w i t n e s s ( q , t ) w \gets \mathrm{witness}(q, t) w ← witness ( q , t )
ℓ ← ∣ v ∣ + ⌊ ∣ x ∣ − ∣ v ∣ 2 ⌋ \ell \gets |v| + \lfloor \frac{|x| - |v|}{2} \rfloor ℓ ← ∣ v ∣ + ⌊ 2 ∣ x ∣ − ∣ v ∣ ⌋
x 1 ← x [ 1 … ℓ ] x_1 \gets x[1 \dots \ell] x 1 ← x [ 1 … ℓ ] and x 2 ← x [ ℓ + 1 … ∣ x ∣ ] x_2 \gets x[\ell + 1 \dots |x|] x 2 ← x [ ℓ + 1 … ∣ x ∣ ]
q 1 ← δ H ( q 0 H , x 1 ) q_1 \gets \delta^\mathcal{H}(q_0^\mathcal{H}, x_1) q 1 ← δ H ( q 0 H , x 1 ) and t 1 ← δ T ( q 0 T , x 1 ) t_1 \gets \delta^\mathcal{T}(q_0^\mathcal{T}, x_1) t 1 ← δ T ( q 0 T , x 1 )
O U T P U T T ( a c c e s s ( q 1 ) x 2 w ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(q_1)\;x_2\;w) OUTPUT T ( access ( q 1 ) x 2 w )
if q 1 # T t 1 q_1 \mathrel{\#_\mathcal{T}} t_1 q 1 # T t 1 then
else
x ← a c c e s s ( q 1 ) x 2 x \gets \mathrm{access}(q_1)\;x_2 x ← access ( q 1 ) x 2
v ← v \gets v ← the unique prefix of x x x s.t. δ T ( q 0 T , v ) ∈ F \delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F δ T ( q 0 T , v ) ∈ F
end if
end while
end procedure
LSharp の中でProcCounterEx を呼び出す前に O U T P U T T ( x ) \mathrm{OUTPUT}_\mathcal{T}(x) OUTPUT T ( x ) を呼んでいるので δ T ( q 0 T , x ) ↓ \delta^\mathcal{T}(q_0^\mathcal{T}, x)\!\!\downarrow δ T ( q 0 T , x ) ↓ ですが、x x x の接頭辞のどこかで B B B の状態から F F F の状態へ遷移しているはずです。
そのような接頭辞をアルゴリズム中では v v v として、ProcCounterEx では次の不変条件を保ちながら、v v v 以降の x x x の文字列の長さを二分探索のように半分にしていきます。
δ H ( q 0 H , x ) # T δ T ( q 0 T , x ) \delta^\mathcal{H}(q_0^\mathcal{H}, x) \mathrel{\#_\mathcal{T}} \delta^\mathcal{T}(q_0^\mathcal{T}, x) δ H ( q 0 H , x ) # T δ T ( q 0 T , x )
v v v は x x x の接頭辞で δ T ( q 0 T , v ) ∈ F \delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F δ T ( q 0 T , v ) ∈ F であるもの (ちょうど1つしか存在しない)
ループが終わったとき x = v x = v x = v のため δ T ( q 0 T , x ) ∈ F \delta^\mathcal{T}(q_0^\mathcal{T}, x) \in F δ T ( q 0 T , x ) ∈ F となります。
さらに q = δ H ( q 0 H , x ) , t = δ T ( q 0 T , x ) q = \delta^\mathcal{H}(q_0^\mathcal{H}, x),\, t = \delta^\mathcal{T}(q_0^\mathcal{T}, x) q = δ H ( q 0 H , x ) , t = δ T ( q 0 T , x ) としたとき、不変条件から q # T t q \mathrm{\#_\mathcal{T}} t q # T t が言えます。
よって t t t がisolatedとなるため、新しい状態が生じるわけです。
次に、ループ中に不変条件が本当に保たれていることを確認していきます。
ProcCounterEx では、O U T P U T T ( a c c e s s ( q 1 ) x 2 w ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(q_1)\;x_2\;w) OUTPUT T ( access ( q 1 ) x 2 w ) を呼び出したあとに q 1 # T t 1 q_1 \mathrel{\#_\mathcal{T}} t_1 q 1 # T t 1 で分岐を行なっています。
q 1 # T t 1 q_1 \mathrel{\#_\mathcal{T}} t_1 q 1 # T t 1 が真の場合は x ← x 1 x \gets x_1 x ← x 1 としますが、この場合は接頭辞も変わらないため、明らかに不変条件を満たしています。
一方、¬ ( q 1 # T t 1 ) \lnot (q_1 \mathrel{\#_\mathcal{T}} t_1) ¬ ( q 1 # T t 1 ) の場合はどうでしょうか。
t 2 = δ T ( q 0 T , a c c e s s ( q 1 ) x 2 ) t_2 = \delta^\mathcal{T}(q_0^\mathcal{T}, \mathrm{access}(q_1)\;x_2) t 2 = δ T ( q 0 T , access ( q 1 ) x 2 ) とおきます。
q = δ H ( a c c e s s ( q 1 ) x 2 ) q = \delta^\mathcal{H}(\mathrm{access}(q_1)\;x_2) q = δ H ( access ( q 1 ) x 2 ) なので q # T t 2 q \mathrel{\#_\mathcal{T}} t_2 q # T t 2 が言えればよいです。
このとき w = w i t n e s s ( q , t ) w = \mathrm{witness}(q, t) w = witness ( q , t ) で O U T P U T T ( a c c e s s ( q 1 ) x 2 w ) \mathrm{OUTPUT}_\mathcal{T}(\mathrm{access}(q_1)\;x_2\;w) OUTPUT T ( access ( q 1 ) x 2 w ) を事前に呼び出していて δ T ( t 2 , w ) ↓ \delta^\mathcal{T}(t_2, w)\!\!\downarrow δ T ( t 2 , w ) ↓ となり、weak co-transitivity (補題2) より q # T t 2 ∨ t # T t 2 q \mathrel{\#_\mathcal{T}} t_2 \lor t \mathrel{\#_\mathcal{T}} t_2 q # T t 2 ∨ t # T t 2 が分かります。
そのため ¬ ( t # T t 2 ) \lnot (t \mathrel{\#_\mathcal{T}} t_2) ¬ ( t # T t 2 ) が言えれば、目的の命題が得られます。
ここで、次の補題を考えます。
補題3 :
Mealy機械 M \mathcal{M} M と状態 q 1 , q 2 ∈ Q q_1, q_2 \in Q q 1 , q 2 ∈ Q 、文字列 u ∈ I ∗ u \in I^\ast u ∈ I ∗ について、次の命題が成り立つ。
¬ ( q 1 # M q 2 ) ∧ δ ( q 1 , u ) ↓ ∧ δ ( q 2 , u ) ↓ ⇒ ¬ ( δ ( q 1 , u ) # M δ ( q 2 , u ) ) \lnot (q_1 \mathrel{\#_\mathcal{M}} q_2) \land \delta(q_1, u)\!\!\downarrow \land \delta(q_2, u)\!\!\downarrow
\Rightarrow
\lnot (\delta(q_1, u) \mathrel{\#_\mathcal{M}} \delta(q_2, u)) ¬ ( q 1 # M q 2 ) ∧ δ ( q 1 , u ) ↓ ∧ δ ( q 2 , u ) ↓⇒ ¬ ( δ ( q 1 , u ) # M δ ( q 2 , u ))
¬ ( q 1 # M q 2 ) \lnot (q_1 \mathrel{\#_\mathcal{M}} q_2) ¬ ( q 1 # M q 2 ) であれば、そこからの遷移が定義されているのであればその先でもapartness relationが成立しないことが維持されるということです。
ここで a c c e s s ( t ) = x 1 x 2 \mathrm{access}(t) = x_1\;x_2 access ( t ) = x 1 x 2 かつ a c c e s s ( t 2 ) = a c c e s s ( q 1 ) x 2 \mathrm{access}(t_2) = \mathrm{access}(q_1)\;x_2 access ( t 2 ) = access ( q 1 ) x 2 であることから、t t t および t 2 t_2 t 2 はそれぞれ x 1 x_1 x 1 と q 1 q_1 q 1 から文字列 x 2 x_2 x 2 で遷移した先の状態なことが分かります。
よって、分岐条件 ¬ ( q 1 # T t 1 ) \lnot (q_1 \mathrel{\#_\mathcal{T}} t_1) ¬ ( q 1 # T t 1 ) と上の補題より ¬ ( t # T t 2 ) \lnot (t \mathrel{\#_\mathcal{T}} t_2) ¬ ( t # T t 2 ) が分かり、q # T t 2 q \mathrel{\#_\mathcal{T}} t_2 q # T t 2 が示せます。
最後に、このアルゴリズムが正しく停止するのか考えます。
基本的には ∣ x ∣ − ∣ v ∣ |x| - |v| ∣ x ∣ − ∣ v ∣ は減少していくのですが ∣ x ∣ − ∣ v ∣ = 1 |x| - |v| = 1 ∣ x ∣ − ∣ v ∣ = 1 の場合 ⌊ ( ∣ x ∣ − ∣ v ∣ ) / 2 ⌋ = = 0 \lfloor (|x| - |v|) / 2 \rfloor == 0 ⌊( ∣ x ∣ − ∣ v ∣ ) /2 ⌋ == 0 のため、¬ ( q 1 # T t 1 ) \lnot (q_1 \mathrel{\#_\mathcal{T}} t_1) ¬ ( q 1 # T t 1 ) で分岐した場合 ∣ x ∣ − ∣ v ∣ |x| - |v| ∣ x ∣ − ∣ v ∣ が減少せず、一見すると問題になりそうです。
ですが ∣ x ∣ − ∣ v ∣ = 1 |x| - |v| = 1 ∣ x ∣ − ∣ v ∣ = 1 ということは v = x 1 v = x_1 v = x 1 となっていて t 1 ⇝ q 1 t_1 \rightsquigarrow q_1 t 1 ⇝ q 1 のため ∣ a c c e s s ( q 1 ) ∣ < ∣ x 1 ∣ |\mathrm{access}(q_1)| < |x_1| ∣ access ( q 1 ) ∣ < ∣ x 1 ∣ になるため x x x の文字数が減少します。
さらに、この分岐で x x x を a c c e s s ( q 1 ) x 2 \mathrm{access}(q_1)\;x_2 access ( q 1 ) x 2 としたときに x 2 x_2 x 2 が短すぎると、そのあと x x x の接頭辞で δ T ( q 0 T , v ) ∈ F \delta^\mathcal{T}(q_0^\mathcal{T}, v) \in F δ T ( q 0 T , v ) ∈ F となる v v v が見つからないという事態が起こりそうにも思えます。
しかし、実際にはそのようなことは起こりません。
なぜなら δ T ( q 0 T , a c c e s s ( q 1 ) x 2 ) ∈ B \delta^\mathcal{T}(q_0^\mathcal{T}, \mathrm{access}(q_1)\;x_2) \in B δ T ( q 0 T , access ( q 1 ) x 2 ) ∈ B だとすると q = t 2 q = t_2 q = t 2 のため、明らかに先程示した q # T t 2 q \mathrel{\#_\mathcal{T}} t_2 q # T t 2 と矛盾するからです。
よってProcCounterEx は正しく動作します。
実装
最後に、ここまで説明してきた L # 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なデータ構造としています。
basis
やfrontier
ではOTree
の状態 (部分木) を保持するのではなく、木の状態へとアクセスする文字列を保持するようにしています。
frontier
はfrontier集合に含まれる状態から、まだ区別できていないbasis集合の状態へのMap
になっています。つまり、解説の F F F と ⇝ \rightsquigarrow ⇝ を組み合わせたような値になっています。
あとは大体解説をそのままコードに落とし込んだようになっていると思います。
あとがき
今回は最新のオートマトン学習アルゴリズムである L # L^\# L # について説明しました。
ProcCounterEx についてが、自分にとっては引っ掛かりの多い部分だったように思います。
正しさ自体は理解できるのですが、Rivest-Schapireに対する線形探索のような、より単純な方法が結局最後までイメージできなかったのが悔しいところです。
相当賢いアイディアになっているのは分かるのですが、abstract counterexample analysis ([Isberner & Steffen, 2014] )のようなフレームワークを確立している L ∗ L^\ast L ∗ と比べると、それほど洗練されているわけではないということを感じます。
また、今回は省いたのですが、ADS (adaptive distinguish sequence) というものを用いてoutput queryの回数を減らす、といったアイディアも論文では説明しています。
observation treeを使ったオートマトン学習というアイディアは L # L^\# L # が初出というわけではなく[Soucha, 2020] が先行研究としてあるようです。
またVaandragerは L # 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