makenowjust-labs/blog

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

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

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

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

Angluinの $L^\ast$ はオートマトン学習 (automata learning) のアルゴリズムとして最も有名なものです。 以前、このブログでもAngluinの $L^\ast$ について説明しました。

$L^\ast$ は歴史のあるアルゴリズムのため、派生アルゴリズムがいくつか存在します。 この記事ではAngluinの $L^\ast$ について簡単に説明した上で、派生アルゴリズムとしてRivest-SchapireとKearns-Vaziraniを紹介します。

• Rivest-Schapireは $L^\ast$ の反例 (counterexample) の解析手法の提案で、二分探索を用いて反例の中のobservation tableに追加すべき接頭辞を探すことで、計算量を改善します。
• Kearns-Vaziraniはobservation tableを置き換えるデータ構造としてdiscrimination treeというデータ構造を提案するものです。

これらの手法により $L^\ast$ の様々な効率が改善できます。

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

Immerman-Szelepcsényiの定理は $s(n) \ge \log n$ の場合に $\mathbf{NSPACE}(s(n))$ (テープ長に上限のある非決定性チューリングマシンが受理できる言語のクラス) が、否定について閉じていることを示す定理です。 Neil ImmermanとRóbert Szelepcsényiが1987年にそれぞれ独立して示し、この成果により両者は1995年にGödel賞を受賞しました。 このように、Immerman-Szelepcsényiの定理は、計算量複雑性の理論上とても重要な定理となっています。

Immerman-Szelepcsényiの定理の証明は、テープ長に上限のある非決定性有限チューリングマシン (NTM) の様相 (configuration) の総数が入力の長さとそのNTMの大きさで抑えられることを活かして、次のようなNTMを構成することで実現されます。

• ある様相から到達可能な様相の総数を数え上げた上で、
• その総数のステップ中に、受理状態に到達可能かを判定する。

この記事ではImmerman-Szelepcsényiの定理を[Uezato, 2024]を参考に証明したいと思います。 方針は論文に書いてある通りで特に目新しい部分はありません。自分の備忘録として残しておきます。

想定読者: 情報科学の基本的な部分を理解しており、計算量複雑性の理論などに関心があることを想定しています。

時相論理 (Temporal Logic) は時間に関する作用素を追加した論理の体系です。 例えば、時相論理では「ボタンを押したら、3秒以内に明かりが点く」のような時間による状況の変化を含めた文を表現することができます。

時間に関する論理的な文は、プログラムやシステムの満たすべき性質を考える際に頻繁に現れます。 そのため、時相論理は形式検証 (Formal Verification) の分野で重要な道具の一つとなっています。

モニタリングとは、入力として与えられた時系列に沿ったイベント列が、時相論理などの形で与えられた仕様を満たすかどうか判定する問題です。 線形時相論理 (LTL) やMetric Temporal Logic (MTL)、Signal Temporal Logic (STL) といった時相論理では、このモニタリングを効率的に行う方法が知られています。 モニタリングは、システムが仕様通りのふるまいをしているかを実行時に確認する、実行時検証の実現方法の1つでもあります。

この記事では、時相論理のモニタリング実装や、その背景にあるアイディアについて整理します。

正規表現マッチングの実装手法の1つとしてPike VMと呼ばれるものがあります。 これはGo言語の正規表現実装やRustのregex crateで使われている手法であり、正規表現$r$と入力文字列$w$に対して$O(|r| \times |w|)$の計算量でマッチングができるのが特徴です。

Earley法はJay Earleyの提案した文脈自由文法 (CFG) の構文解析手法の1つです。 すべてのCFGを構文解析できる手法で最悪計算量は$O({|w|}^3)$ですが、無曖昧であれば$O({|w|}^2)$で、決定的であれば$O({|w|})$で構文解析ができます。

実装してみると分かりますが、Pike VMとEarley法には類似している点があり、Earley法をPike VMの発展系のように考えることができます。 この記事ではPike VMとEarley法のRubyでの実装を通じて、それらの関係を解説します。

想定読者: 形式言語や構文解析についての基本的な知識がある (NFAやCFGなどを知っている) ことを想定しています。