技術要約：離散システムにおける遷移偏差に対するニューロシンボリック・ロバストネス解析

問題提起

離散イベントシステム（DES）の監視制御において、コントローラはプラントモデルに対して仕様を強制するように合成される。古典的な手法は「構成による正当性（correct-by-construction）」の保証を提供するが、これらの保証はプラントモデルの正確性に厳密に依存している。実際には、未モデル化のダイナミクス、センサノイズ、または抽象化エラーに起因する不一致により、実システムが公称モデルから逸脱し、安全性を損なう可能性がある。

近年の研究では、**離散的ロバストネス（discrete robustness）**を、スーパーバイザが安全性を維持できるすべての可能な遷移偏差（公称プラントに追加される追加の遷移）の集合として定義することで、この問題に対処してきた。しかし、この遷移ベースのアプローチには、主に2つの決定的な限界がある：

1. スケーラビリティ: 可能な偏差の空間は状態空間とアクション空間に応じて指数関数的に増大するため、全列挙を行うことは、極めて小さなシステムを除いて計算量的に困難である。
2. 保守性（Conservatism）: 数学的に可能な偏差の大部分は、物理的に実行不可能である（例：入力なしに機械が自発的に部品を出力するなど）。これらの実行不可能な偏差を含めると、探索空間が膨張し、現実世界のシステム挙動を正確に反映しないロバストネス結果をもたらす。

$P_{sys}$ を用いて実行不可能な偏差をフィルタリングしようとする既存の試みは、ドメインエキスパートが物理法則を形式的な仕様へと手動でエンコードする必要があり、これが大きな負担となり、解析パイプラインにオーバーヘッドを加えることになる。

手法

本論文は、これらのスケーラビリティと実現可能性の課題に対処するために、ニューロシンボリック・コンピューティング・フレームワークを提案する。このアプローチは、物理的な実現可能性に関する推論と、ロバストネス保証の形式的な計算を分離し、以下の2段階のプロセスを利用する：

1. ニューラル実現可能性フィルタリング（LLMレイヤー）

第1段階では、大規模言語モデル（LLM）を活用して、物理的に実現可能な偏差遷移のサブセット（$D$）を推論する。

• 入力: フレームワークは、プラントとスーパーバイザの形式的なLTSモデル、システムの状態とイベントの自然言語記述、安全仕様、および物理法則に関するドメイン知識（例：「部品は同時に2箇所に存在することはできない」）を取り込む。
• プロセス: 構造化されたプロンプトテンプレートが、LLMによるこれらの入力の推論を導く。LLMは、システムのセマンティクスおよび物理的制約と整合する、現実的な故障または偏差を表す遷移を特定するようタスクを与えられる。
• 出力: 公称遷移空間 $(Q_E \times Act_E \times Q_E) \setminus R_E$ よりも大幅に小さい、実現可能な偏差の縮小された集合 $D$。

2. シンボリック・ロバストネス検証（シンボリックレイヤー）

第2段階では、縮小された集合 $D$ に対して形式検証を行う。

• プロセス: ブルートフォース・アルゴリズム（Algorithm 1）が、実現可能な偏差 $D$ のすべての部分集合を反復処理する。各候補偏差セット $d$ について、標準的なモデル検査を用いて、偏差したシステム $E_d$ がスーパーバイザ $S$ によって制御された際に安全特性 $P$ を満たすか（すなわち、$E_d/S \models P$）を検証する。
• 洗練（Refinement）: アルゴリズムは、最終的なロバストネス集合 $\Delta_f$ を形成するために、極大なロバスト偏差（他のロバスト偏差に含まれないもの）のみを抽出する。
• 保証: 検証は形式的に定義された遷移システム上でシンボリックに行われるため、得られるロバストネス保証は、推論された集合 $D$ に対して数学的に正しい状態を維持する。

主な貢献

本論文は、主に2つの貢献を述べている：

1. ニューロシンボリック・フレームワーク: LLMを用いて物理的に実現可能な偏差モデルを推論し、シンボリック手法を用いてロバストネス保証を計算する、新しいアーキテクチャ。このアプローチは、自然言語とドメイン知識から物理的制約を抽出することを自動化し、$P_{sys}$ の手動による形式的エンコードの必要性を排除する。
2. プロトタイプと評価: プロトタイプツールの実装と、製造システム、Therac-25放射線治療インターフェース、およびAlternate Bit Protocol (ABP) の3つの異なるケーススタディを用いた実験的評価。

実験結果

フレームワークは、実現可能性フィルタリングにLLM（GPT-5.2およびClaude 3.5 Sonnet）を、Pythonベースのシンボリック検証器を用い、3つのケーススタディで評価された。

• 製造システム: LLMは18個の実現可能な偏差を特定した（理論的な空間は108）。シンボリックレイヤーは1つの極大ロバスト偏差セットを見つけ、システムが15の特定の遷移に対してはロバストであるが、特定のバッファアンローディング故障に対しては脆弱であることを確認した。
• Therac-25: 分析により9個の実現可能な偏差が特定された。システムは操作者の繰り返しの「enter」押下に対してはロバストであったが、電子線治療の選択に関わる特定のレースコンディションに対しては脆弱であり、歴史的な設計上の欠陥を正確に捉えた。
• ABPプロトコル: LLMは16個の実現可能な偏差を特定した。分析により、メッセージの消失、重複、および破損に対してロバストであることが確認され、プロトコルの設計意図と一致した。

定量的知見:

• 実現可能性の削減: LLMは探索空間を大幅に削減した。削減率は、全遷移空間と比較して、Ther-25の67%からABPの99%に及んだ。
• 実現可能性の精度: 製造システムの例では、GPTが生成した遷移の89%が物理的に実現可能であったのに対し、Claudeは54%であった。ABPのようなより複雑なシステムでは、両モデルとも実現可能性率が低下した（それぞれ63%と36%）。これは、プロンプトエンジニアリングやドメイン・オントロジーの改善が必要であることを示唆している。
• ロバストネスの等価性: 縮小された偏差セットで動作しているにもかかわらず、本フレームワークは、評価されたケースにおいて全空間ベースの分析から得られたものと同等のロバストネス保証を生み出した。

重要性と主張

本論文は、このニューロシンボリック・アプローチが、離散的ロバストネス解析におけるスケーラビリティと、実行不可能な偏差の包含というトレードオフをうまく解決していると主張している。物理的な理解に基づくセマンティックおよび物理的なフィルタリングにLLMを使用することで、本手法は、全列挙が不可能なシステムにおいてもロバストネス解析を現実的なものにしている。

著者らは、LLMコンポーネントが実現可能な偏差を特定する際に確率的な要素を導入する一方で、その後のシンボリック検証によって、最終的なロバストネス保証が形式的に正しいことが保証されることを強調している。本研究は、大幅に縮小された、物理的に意味のある偏差のサブセットを用いて、全空間手法に匹敵するロバストネス解析を実現できることを示している。

論文は、現在のブルートフォース・アルゴリズムの実装には、より大きなシステムのための最適化が必要であること、また今後の課題として、プロンプトエンジニアリングの向上、LLMの精度を高めるためのドメイン・オントロジーの組み込み、およびシンボリックな結果がLLMへのクエリを導くインタラクティブな洗練ループの調査に焦点を当てることを述べ、控えめに結論づけている。