技術的サマリー：重み付きオートマトンの SMT ベースのアクティブ学習

問題定義

Angluin の$L^\star$アルゴリズムによって先駆されたアクティブオートマトン学習は、形式検証において未知のコンポーネントのモデルを推論するための標準的な技術となっている。$L^\star$スタイルの手法はブーリアンオートマトン（決定性と非決定性）に対して確立されているが、**重み付き有限オートマトン（WFA）**への拡張は、はるかに困難であることが証明されている。WFA は、半環からの重みを遷移に割り当てることでブーリアンオートマトンを一般化し、コスト、確率、リソース消費などの定量的性質のモデル化を可能にする。

WFA の学習に対する既存のアプローチは、Hankel 行列や観測テーブルの一般化（例：$WL^\star$）に依存している。これらの手法は、基礎となる半環の代数構造に関する推論を必要とする。その結果、停止性と最小性の証明は微妙であり、しばしば特定の代数クラス（例：体、主イデアル整域）に制限される。トロピカル半環やボトルネック半環など、多くの実用的に関連する半環に対しては、停止性の保証が不明であるか、最小オートマトンを保証しない。さらに、既存のアルゴリズムはしばしば非最小なモデルを生成するか、無限半環上で効果的にスケーリングできない。

手法

著者は、学習問題を直接SMT（Satisfiability Modulo Theories）ソルバーで解決可能な充足可能性問題として定式化する、新しい制約ベースのアクティブ学習アルゴリズムを提案する。

中核的なアプローチ

観測テーブルを精緻化する代わりに、このアルゴリズムは与えられた半環$S$上の方程式系を反復的に構築する。この方程式系の解は、観測されたすべての問い合わせに対して「教師」（対象言語）と一致する非決定性 WFAに正確に対応する。

学習プロセスは、標準的なアクティブ学習ループ（アルゴリズム 1）に従う：

1. 仮説生成：アルゴリズムは、現在の観測セット$O$と整合する$n$状態の WFA を見つけようとする。これはサブルーチン getAutomaton に委譲される。
2. 同等性問い合わせ：整合する仮説$H$が見つかった場合、$H$が対象言語$L$を認識するか確認するために教師に問い合わせる。
3. 反例処理：教師が反例$w$（$H(w) \neq L(w)$）を提供した場合、$w$を$O$に追加し、強化された制約でループを繰り返す。

getAutomaton サブルーチン

本論文は、getAutomaton の 2 つの実装を提示する：

1. 単純なベースライン：WFA の意味論を直接符号化する。初期重み、遷移行列、最終重みを未知変数として扱い、すべての$w \in O$に対して$out(w) = \text{semantics}(w)$という方程式を解く。
2. 最適化版（SWAL）：コ代数の視点と状態言語の概念を利用する。グローバルな言語を直接解くのではなく、各状態から受け入れられる言語を表す中間変数を導入する。これにより、以下のような方程式系が得られる：
   • 安定化制約：状態言語が遷移重みと整合していることを保証する。
   • 張り制約：初期重みが状態言語を正しく結合して対象出力と一致することを保証する。
   • 重要な洞察：この符号化はより多くの変数と方程式を導入するが、観測間の共有部分構造（接尾辞）を露出させる。これにより、SMT ソルバーは中間結果を再利用でき、単純なアプローチに比べてスケーラビリティが大幅に向上する。

決定性と半環

このアルゴリズムは半環に対してパラメトリックである。著者は、決定可能な半環（有限方程式系の充足可能性が決定可能なもの）に対しては、getAutomaton サブルーチンを健全かつ完全に実装できることを特定している。

• 有限半環：総当たりまたは SMT によって自明に決定可能。
• 無限半環：本論文は、トロピカル半環（$\min, +$）、有界トロピカル半環、およびボトルネック半環（$\max, \min$）を、Quantifier-Free Linear Integer Arithmetic (QF-LIA) や Quantifier-Free Bit-Vectors (QF-BV) などの決定可能理論へ符号化する手法を提供する。

主要な貢献

1. 新しいアルゴリズム：半環に対してパラメトリックな、非決定性 WFA のための新しい SMT ベースのアクティブ学習アルゴリズム。
2. 最小性の保証：特定の代数構造の外では最小性の保証が欠如していることが多い$L^\star$スタイルの手法とは異なり、このアルゴリズムは停止時に最小の WFA を生成することが保証される（半環に関わらず）。
3. 停止条件：著者は部分正しさを証明し、停止のための十分条件を提供する。具体的には、すべての有限半環に対してアルゴリズムが停止することを証明する。無限半環については、同じ濃度の議論による停止の理論的保証はないが、実装は実用的な成功を示している。
4. 制約ベースの合成：本論文は、WFA に対する最初の制約ベースの生成アルゴリズムを導入し、SMT ベースの合成を可能にする。また、結果として生じる制約系が決定可能となる特定の半環を特定する。
5. 実験的評価：提案手法（SWAL）を単純なベースラインおよび最先端の$WL^\star$アルゴリズムと比較した包括的な評価。

実験結果

著者は OCaml で Z3 ソルバーを使用してアルゴリズム（SWAL）を実装し、ブーリアン、トロピカル、有界トロピカル、およびボトルネック半環にわたる 5,000 以上のランダム生成されたベンチマークで評価を行った。

• 単純なベースラインとの比較：SWAL は、実行時間とスケーラビリティの両面で単純な符号化を大幅に上回る。単純なアプローチは半環に応じて 2〜6 状態を超えるオートマトンの学習に苦しむのに対し、SWAL は最大 8 状態の最小オートマトンの学習に成功する。最適化された符号化（状態言語）は、タイムアウト/メモリ不足エラーの数を桁違いに減少させる。
• $WL^\star$との比較：主イデアル整域向けの最先端アルゴリズムである$WL^\star$と比較すると：
  • 最小性：SWAL は一貫して最小のオートマトンを生成するのに対し、$WL^\star$は最大 10 倍大きなオートマトンを生成することが多い。
  • 効率性：SWAL は$WL^\star$よりも少ない出力問い合わせ（教師との相互作用）を必要とする。
  • 実行時間：SWAL は実行時間において競争力があり、$WL^\star$よりも頻繁に高速に終了し、リソース失敗（TO/OOM）が少ない。
• 増分性：増分的な SMT 解決を有効にすると、学習時間とリソース使用量が劇的に減少し、増分学習に対する制約ベースのアプローチの適合性が確認される。

意義と主張

本論文は、特に検証指向の環境において、重み付きオートマトンに対する従来の Hankel/$L^\star$スタイルの手法に対する実用的かつ堅牢な代替手段として、制約ベースの学習を位置づけている。

• 堅牢性：このアプローチは、$L^\star$スタイルの手法に対する代数停止証明が困難または存在しない、より広範な半環（トロピカルなどの無限半環を含む）を処理する。
• 最小性：最小モデルは効率的な検証と抽象化に不可欠であるため、最小性の保証は重要な利点である。
• スケーラビリティ：実験結果は、SMT ベースの合成が、既存のアルゴリズムでは現在到達不可能な複雑で最小の重み付きオートマトンを学習するまでスケーリングできることを示している。

著者は、すべての無限半環に対する一般的な停止証明を提供していないこと（既知の未解決問題）を認めつつも、その手法は、以前の手法が失敗するか、最適でないモデルを生成するシナリオにおいて最小の WFA を学習する実用的な解決策を提供すると結論付けている。今後の課題には、より増分的な仮説更新の探求と、確率オートマトンへのアプローチの拡張が含まれる。