技術的概要：再帰的多項式代理三値論理ゲートネットワークの安定性と実現可能性

1. 問題定義

信号時相論理（STL）を用いたリアルタイムの安全性仕様監視は、根本的な「因果的ギャップ」に直面します。標準的なオフライン STL モニタは、有界時相演算子（例：$\square_{[0,5]} \mu$）を評価するために将来の信号値を必要としますが、因果的・オンラインのモニタはこれにアクセスできません。LSTM や GRU などの再帰型ニューラルネットワーク（RNN）は、部分的な軌跡から判決を予測するために時空間パターンを学習することでこのギャップを埋めるために用いられてきましたが、入力劣化に関する構造的保証は欠如しています。

安全性クリティカルなシステムでは、センサー入力が劣化したり利用不可能になったりする可能性があります。連続領域で動作する標準的な RNN は、「決定された」状態と「不確実な」状態を区別するメカニズムを提供しません。その結果、入力 dropped や不確定な述語が発生すると、RNN は「不明」状態へ優雅に劣化するのではなく、判決を「安全」から「不安全」（またはその逆）へ静かに反転させる可能性があります。神経ネットワークの予測能力と、部分情報下での形式的論理に内在する保守的な不確実性伝播を組み合わせる、学習されたモニタが必要です。

2. 手法：R-DTLGN アーキテクチャ

著者は、$0$ が明示的に「未知」を表す Kleene の三値論理領域 $\mathbb{T} = \{-1, 0, +1\}$ でネイティブに動作する再帰型アーキテクチャである**再帰型微分可能三値論理ゲートネットワーク（R-DTLGN）**を提案します。

中核コンポーネント

• 三値論理領域: ネットワークは Kleene の強三値論理を利用し、論理結合子（AND, OR, NOT）は「未知」の値を保守的に伝播させます。例えば、$True \land Unknown = Unknown$ です。
• 多項式代理トレーニング（PST）: 離散論理ゲートの微分可能トレーニングを可能にするため、ネットワークは PST を採用します。各ニューロンは、9 つの学習可能係数を持つ次数 $(2,2)$ の多項式として表現されます。これにより、ネットワークは $[-1, 1]$ の連続値に対する勾配降下法でトレーニング可能になります。
• 再帰セル構造: R-DTLGN セルは、現在の述語値と前の隠れ状態を取り込み、$L$ 層の三値 PST ゲートを通じて処理し、更新された隠れ状態と出力判決を生成します。隠れ状態は「すべて未知」の状態 $(0, \dots, 0)$ で初期化されます。
• 硬化と蒸留: 推論時、ソフトな多項式ネットワークは離散的な三値論理回路に「硬化」されます。著者は再帰設定のための軌道蒸留法を導入します。これは、ニューロンを独立して丸める（これによりグローバルな不整合を引き起こす）のではなく、較正セットにおける判決の不一致を最小化するために、ゲートの目標語彙上で貪欲な座標降下を行うものです。

ゲート語彙と順序付け

分析は、三値領域上の 2 つの部分順序に依存します：

1. 数値的順序（$\leq$）: $-1 \leq 0 \leq +1$。この順序に対して単調なゲート（NM）は、トレーニング中の安定した再帰的ダイナミクスを保証します。
2. 情報順序（$\sqsubseteq$）: $0 \sqsubseteq -1$ かつ $0 \sqsubseteq +1$（$-1$と$+1$ は比較不可能）。この順序に対して単調なゲート（IM）は、原理的な劣化を保証します。決定された入力を未知に置き換えることは、出力をより決定しにくくするだけであり、間違った値に反転させることはありません。

著者は、安定性と劣化保証の両方を満たす 17 の非定数ゲート（AND や OR を含む）を含む交差語彙（$NM \cap IM$）を特定しました。

3. 主要な貢献

A. アーキテクチャと硬化

R-DTLGN は、学習された時相予測と三値論理に根ざした形式的劣化保証を結合した最初の再帰型アーキテクチャです。著者は、2 フェーズ硬化ルーチンを導入します：

1. フェーズ 1: 安定したダイナミクスを確保するために、数値的単調（NM）ゲートの全セットを使用した蒸留。
2. フェーズ 2: 劣化保証を拡張するために、NM のみのゲートを $NM \cap IM$ の候補に置き換える試行。精度低下が最小限の場合にのみ交換を承認します。

B. 劣化保証

本論文は、情報単調（IM）ゲートで構成された R-DTLGN セルが 2 つの重要な性質を満たすことを証明します：

1. 原理的棄権: すべてが入力未知の場合、出力も未知となります。モニタは欠如した証拠から判決を捏造しません。
2. 入力確実性単調性: 決定された入力を未知に置き換えることは、出力をより決定しにくくする（または同じに保つ）だけであり、決定された判決を反対の値に反転させることはできません。
   これらの保証は、トレーニングの産物ではなく、アーキテクチャの構造的不变量です。

C. 実現可能性の境界

著者は、ネットワークの隠れ状態次元に関する数式駆動の仕様を導出しました。有界 STL 式 $\varphi$ が与えられた場合、時相演算子の区間とネストの深さに基づく状態複雑性 $B(\varphi)$ を定義します。

• 定理: $\varphi$ を監視できる任意の R-DTLGN は、隠れ状態次元 $S \geq B(\varphi)$ を必要とします。
• これは、ハイパーパラメータ探索を、STL 式の構造に基づく直接計算に置き換えます。例えば、幅 $w$ の区間における「Until」演算子は、$2w$ ビットの状態ビットを必要とします。

D. ラベル構築パイプライン

本論文は、2 つのラベル構築戦略を評価します：

• 計算後量子化（CtQ）: 連続信号上で頑健性を評価し、その後量子化します。真の判決を目標としますが、ネットワークに不十分な情報に基づいてコミットすることを強制する可能性があります。
• 量子化後計算（QtC）: 述語をまず三値に量子化し、その後頑健性を評価します。構造的に回復可能な判決のみを目標とし、トレーニング目的を劣化保証と整合させます。

4. 実験結果

R-DTLGN は、D4RL PointMaze ナビゲーション環境からの 816 軌道と、6 つの有界 STL 仕様に対して評価されました。

• 因果的ギャップの埋め: R-DTLGN は、因果的ベースライン（利用可能なデータに制限された STLCG++）を大幅に上回り、特定のタスクで 33〜38 パーセントポイントの精度向上を達成しました。6 つの仕様のうち 4 つにおいて、バニラ RNN（Elman ネットワーク）の性能と同等かそれ以上でした。
• 硬化性能: 2 フェーズ蒸留は、ソフトなネットワークを離散回路へ成功裡に変換しました。いくつかの仕様では「硬化ギャップ」（精度低下）が見られましたが、他の仕様では硬化された回路がソフト版を上回っており、蒸留が正則化として機能することを示唆しています。
• 劣化挙動:
  • 判決保持: 述語ドロップアウト下において、QtC 硬化された R-DTLGN は、判決の符号の完全またはほぼ完全な保持（一部の仕様では 100%）を維持しましたが、RNN は着実な劣化を示しました。
  • 格子単調性: QtC パイプラインは、すべての述語サブセットにわたり、入力確実性単調性に対して 93.0% の平均適合率を達成しました。CtQ パイプラインは 85.4% であり、精度と構造的安全性の間のトレードオフを反映しています。
  • 棄権: QtC 回路は、入力が除去されるにつれて正しく「未知」（棄権）へ遷移しましたが、RNN と CtQ 回路は棄権できず、しばしば誤った決定値を生成しました。

5. 意義と主張

本論文は、R-DTLGN が、学習された時相予測と三値論理に根ざした形式的劣化保証を結合した最初の再帰型アーキテクチャであると主張します。

• 構造的保証: 標準的な RNN では劣化挙動が学習された重みとトレーニング拡張（例：ドロップアウト）に依存するのに対し、R-DTLGN の入力不確実性に対する頑健性は、そのアーキテクチャ（IM ゲートの選択）によって保証されます。
• 相補的機能: このシステムは、2 つの重複しない機能を提供します。(1) 学習されたパターンを用いて因果的ギャップを埋める予測能力、および (2) 入力情報が失われた際の頑健性を確保する劣化保証。
• 設計効率: 実現可能性の境界により、ネットワークサイズを STL 式から直接導出でき、隠れ状態次元に関する広範なハイパーパラメータ探索の必要性を排除します。

著者は限界を認め、2 フェーズ蒸留がすべての仕様に対して硬化ギャップを完全に埋めるわけではないこと、および劣化保証が厳密に情報単調ゲートを必要とすることを指摘しています。今後の研究として、より長い時間範囲やマルチトリット符号化のためのゲート付き変種が提案されています。