技術要約: dtControl2+ε: MDPにおける説明可能性のための決定木を用いた取引最適性

問題定義

マルコフ決定過程（MDP）におけるコントローラ合成は、多くの場合、大規模で非構造的な状態-行動テーブルとして表される最適コントローラを生成する。これらのテーブルは数学的には正確であるが、リソース制約のあるデバイスへの実装には不向きであり、説明可能性にも欠けるため、検証や認証の妨げとなる。既存のツール（dtControl2など）は、これらのコントローラを決定木（DT）として表現することで解釈性を向上させようと試みている。しかし、大規模なシステムや多くのコーナーケースが存在する場合、これらのDTでさえも人間が理解するには複雑になりすぎてしまうことがある。

決定木のサイズを削減することは容易ではない。なぜなら、一つの重要な決定を取り除くだけで、コントローラが不正確になる可能性があるからである。さらに、多くのスケーラブルな合成手法は、$\epsilon$-最適（最適値から$\epsilon$以内の性能）なコントローラしか提供しないが、既存のDT構築ツールは通常、厳密な（$\epsilon=0$の）表現を目指しており、簡略化のために許容される不正確さを活用できていない。

手法

本論文では、$\epsilon$機能を導入することで、最先端のdtControl2を拡張したツールであるdtControl2+$\epsilon$を提示する。コアとなるワークフローは、確率的モデルチェッカーであるStormと密接に統合されており、結果として得られるコントローラが$\epsilon$-最適であることを保証しながら、より小さく説明可能なDTを構築する。

手法は以下の3つのステップで進行する。

1. モデル解決とデータセット構築

決定論的な最適コントローラから開始する代わりに、本ツールは**許容的（permissive）なデータセット（状態を許可された行動の集合にマッピングするもの）、または結合された（combined）**データセット（許容的な行動を到達可能な状態に制限するもの）を生成する。

• 許容的戦略: ツールは、最適であるか、あるいは同じ値をもたらす行動を特定し、これによりDTが状態を「統合」することを可能にする。
• 削減ヒューリスティック: DTの学習を行う前に、ツールは特定の行動の選択が結果に影響を与えない、あるいは導入される誤差が$\epsilon$未満である状態を特定し、除去する。主な削減テクニックには以下が含まれる：
  • AllOpt: すべての利用可能な行動が最適である状態の除去。
  • Agency: 最良の行動と最悪の行動の差が$\epsilon$未満である状態の除去。
  • Dominance: どのような一貫したコントローラの下でも、他の状態からほぼ確実に到達される状態の除去。
  • Unreach: 初期状態からどのような一貫したコントローラの下でも到達不可能な状態の除去。

2. 決定木学習

本ツールは、標準的なヒューリスティックベースの決定木構築アルゴリズム（アルゴリズム1）の修正版を採用しており、いくつかの拡張機能を備えている。

• 述語抽出: 高レベルのモデル記述（例：PRISM言語の遷移ガード）から関連する述語を自動的に抽出する。これは、従来のツールの半自動的なテンプレート・アプローチよりも優れている。
• 不純度指標: 不純度の計算にモデル固有の重み付けを導入する。一様な重み付けではなく、以下を使用する：
  • Imp_Simulation: 状態を訪問頻度によって重み付けする（$\epsilon$-最適性を確保するための安全なフロアを設ける）。
  • Imp_Agency: 状態をそのエージェンシー（潜在的な誤差）によって重み付けする。
  • Imp_CoE (Cost of Error): 特定の状態において最悪の行動を選択した場合の影響力によって、状態を重み付けする。
• 検証を伴う積極的なヒューリスティック: ツールは、早期停止（Early-Stopping）（不純度が閾値を下回った場合に分割を終了する）および強欲な枝刈り（Greedy Pruning）（部分木を崩壊させる）を採用している。以前の「積極的」なアプローチは健全性を損なうリスクがあったが、dtControl2+$\epsilon$は、これらのステップの後にStormを使用して生成された木の$\epsilon$-最適性を検証することで、健全性を担保している。もし精度制約が違反された場合、ツールはヒューリスティックを緩和して再試行する。

3. 検証ループ

Stormとの緊密な結合による事後構築検証は、本ツールのユニークな特徴である。ツールは生成されたDTの精度をチェックする。もし最適値からの偏差が$\epsilon$を超えた場合、ツールはバックトラックしてヒューリスティックの積極性を下げ（例：停止閾値を上げる、または枝刈りを無効にする）、最終的な出力が$\epsilon$-最適であることが保証されるようにする。

主な貢献

1. dtControl2+$\epsilon$ ツール: $\epsilon$による不正確さを利用して、より小さなDTを構築するためにdtControl2を拡張した、自己完結型のツール。
2. 安全なヒューリスティック vs 積極的なヒューリスティック: 「安全な」削減（定義により$\epsilon$-最適性を保持するもの）と、「積極的な」ヒューリスティック（モデルチェッキングによって検証されるもの）を明確に分離するフレームワーク。
3. 自動述語抽出: 決定述語をモデルの遷移ガードから直接導出する方法であり、述理の選択における手動のドメイン知識の必要性を排除する。
4. 多様な目的へのサポート: 標準的な目的（到達可能性、安全性、到達・回避、報酬ベース）をカバーし、さらにメモリベースのコントローラを扱うことで、一意に**線形時相論理（LTL）**プロパティをサポートする。

結果

著者らは、38のベンチマーク（最大500,000の状態を持つPRISMモデルを含む）を用いて、dtControl2+$\epsilon$をdtControl2、dtPaynt、dtNESt、およびCAV15のアプローチの再実装と比較評価した。

• サイズ削減: 厳密な表現（$\epsilon=0$）の場合でも、dtControl2+$\epsilon$は、改善された初期データセットと安全なヒューリスティックにより、dtControl2よりも数桁小さいDTを生成する。
• $\epsilon$の影響: $\epsilon = 10^{-2}$を許容した場合、本ツールはベンチマークのほぼ半分に対して単一ノードのDTを生成した。これは、単一の行動（一様なランダム・フォールバックを伴う）が$\epsilon$-最適性にとってしばしば十分であることを示している。
• 比較:
  • vs. dtControl2: dtControl2+$\epsilon$は、一貫してより小さな木を生成する。
  • vs. dtPaynt: dtPayntはほとんどのベンチマークでタイムアウトし、成功した場合でもより大きな木を生成した。
  • vs. dtNESt: dtNEStは$\epsilon=0$において強力な競合相手であるが、dtControl2+$\epsilon$は38件中23件のベンチマークでdtNEStの最大半分のサイズであり、10件では1桁小さい木を生成した。注目すべきは、dtNEStは$\epsilon > 0$の際に失敗するか、より大きな木を生成することが多いのに対し、dtControl2+$\epsilon$は不正確さを活用することに長けている点である。
• スケーラビリティ: 本ツールは20分のタイムアウト制限内で、1つを除いたすべてのベンチマークを解決しており、大規模で複雑なモデルに対する実現可能性を示している。

重要性

本論文は、dtControl2+$\epsilon$が説明可能なコントローラ合成における最先端技術の重要な進歩であることを主張している。制御可能な程度の最適性をトレードオフにすることで、本ツールは、以前は解釈が複雑すぎた、人間が理解可能なコントローラの生成を可能にする。構造的な洞察（例：$\epsilon$-最適性のために単一のルールが十分であることを特定するなど）を自動的に導出し、LTLプロパティをサポートできる能力は、既存のツールと一線を画している。著者らは、彼らのアプローチが、以前のヒューリスティックベースの枝刈り手法が正当性を損なう可能性があったのと異なり、$\epsilon$-最適性の保証を提供することを強調している。