Glass Box at Orbit: A Constitutional AI Verification Framework for Trustworthy Autonomous CubeSat Intelligence

技術要約：Glass Box at Orbit

問題提起
本論文は、軌道上コンピューティング分野において台頭している重大なガバナンスの空白（ガバナンス・ギャップ）を取り上げている。宇宙産業が、人間の介入なしに数千もの自律的なAIワークロードを実行する「軌道上データセンター」（MicrosoftやAWS、Starcloudによるイニシアチブなど）へと移行する中で、AIの決定を物理的な安全制約に対して検証するための既存のランタイム・メカニズムが存在しない。現在の安全パラダイムは不十分である：

• デプロイ前の形式検証（モデル検査、定理証明）：学習済みAIシステムに対しては不完全である。なぜなら、放射線によって破損した重みや、食（エクリプス）への進入時の電力状態といった、分布外（out-of-distribution）の条件を考慮できないためである。
• デプロイ後の故障検知（FDIR）：これは事後的なものである。ハードウェアの故障が発生した後にのみそれを特定するため、不可逆的な損傷（例：食の期間中にバッテリーを深放電閾値以下まで消耗させること）を引き起こす前に、AIが生成したコマンドを阻止することができない。

核心となる問題は、AIの行動が宇宙機の各サブシステムに到達する前にインターセプトし、その決定が軌道上の物理学の範囲内に留まることを保証できる**ランタイム憲法検証レイヤー（runtime constitutional verification layer）**の欠如である。

手法：Glass Boxフレームワーク
著者らは、CubeSat向けの5層自律型軌道インテリジェンス・アーキテクチャである「Project October」に統合されたランタイム検証レイヤー、Glass Boxを提案している。Glass Boxは、AIポリシーと宇宙機のサブシステムの間のゲートキーパーとして機能する。

1. 軌道デジタルツイン（ODT）：Glass Boxは、OrekitおよびNASA GMATを用いた物理的に正確なデジタルツインに依存しており、これが軌道、電力、熱、放射線、および姿勢力学に関するリアルタイムの状態ベクトルを提供する。
2. 憲法制約文法（Constitutional Constraint Grammar）：AIポリシーからのすべての候補アクション（$a_t$）は、6つの閉じた形式の物理に基づいた制約（$C_1$から$C_6$）に対して評価される：
   • C1（電力安全マージン）：発電量が負荷と安全バッファを上回ることを保証する。
   • C2（熱境界）：$[-20^\circ\text{C}, +70^\circ\text{C}]$の範囲内での動作を検証する。
   • C3（衝突回避）：衝突確率を$10^{-4}$以上に高める操縦を拒否する。
   • C4（バッテリーフロア）：充電状態（SOC）が$20\%$未満の場合、非必須の動作を停止する。
   • C5（放射線フォルトゲート）：シングルイベントアップセット（SEU）率が閾値を超えた場合、三重冗長化（TMR）を義務付ける。
   • C6（ベイズ信頼性ゲート）：予測エントロピー（モンテカルロ・ドロップアウト経由）が閾値を超えた場合、放射線によって破損したモデル出力を検出し、アクションをブロックする。
3. LTL安全不変量：時間経過に伴う振る舞いのシーケンスを検証するために、7つの線形時相論理（LTL）不変量が定義されている（例：「異常がフラグ立てされた場合、2軌道周期以内にダウンリンクが行われなければならない」）。これらはZ3およびNuSMVモデルチェッカーを用いて検証される。
4. 検証ロジック：検証器は、APPROVE（アクションは安全、説明可能性スコアと共にログに記録）、FLAG（違反が検出されたが深刻度は低い、ダウンリンクをキューに入れ、安全なデフォルト値に置換）、BLOCK（深刻度が高い、コマンドをキャンセルし、セーフモードをトリガー）の3つの状態を出力する。
5. 説明可能性：承認されたすべての決定には、重み付きの説明可能性スコア $E(a_t) \in [0, 1]$ と、どの制約が満たされたか、あるいは違反したかを詳細に示す完全な監査ログが付与される。

主な貢献
本論文は、以下の5つの具体的な貢献を行っている：

• C1. 憲法制約文法：電力、熱、衝突、バッテリー、放射線、および信頼性をカバーする6つの制約を、ライブな軌道物理学上の述語として定式化した。
• C2. LTL安全仕様：瞬時的な制約を、軌道上のトラジェクタリにわたる行動保証へと拡張する7つの時相論理不変量。
• C3. $O(N_c)$ 検証複雑性定理：Glass Boxの検証オーバーヘッドが、憲法ルールの数（$N_c$）に対して線形であり、AIモデルのサイズや宇宙機の状態次元とは独立していることの形式的な証明。
• C4. 説明可能性アーキテクチャ：接触フリー（通信なし）のウィンドウ期間中における、すべての自律的決定に対する重み付きスコアと完全な監査ログを提供するメカニズム。
• C5. 実例：食への進入直前に、不安全な推論リクエストをGlass Boxがインターセプトする様子を示す詳細なシミュレーション。これにより、ミッションの生存性を維持するためのタスクの延期を実証している。

結果と検証
本論文は、完全にシミュレートされた環境（Project October フェーズI）に基づく結果を提示している：

• 複雑性：検証プロセスは$O(N_c)$であることが証明されており、ルールの追加がサブワット級の組み込みプロセッサ（例：ARM Cortex-M4）のタイミング・ボトルネックにならないことを保証している。
• シミュレーション・ケーススタディ：バッテリー残量が減少した状態で、食への進入3分前に火災の推論リクエストが提案されたシナリオにおいて、Glass Boxは正しく電力違反（$c_1 = \bot$）を特定した。ミッション全体をブロックするのではなく、アクションをFLAG（フラグ立て）し、太陽光発電が回復するまで推論を6分間延期した。これにより、バッテリーの深放電を防ぎつつ、ミッション目標の達成を可能にした。
• 形式検証：7つのLTL不変量が、Z3およびNuSMVを用いて制約文法に対して機械的に検証され、安全ロジックの一貫性が確認された。

意義と主張
本論文は、軌道上コンピューティングがデータセンター・インフラストラクチャへとスケールアップするにつれ、ランタイムの憲法検証が研究上の珍しい手法から、ミッションクリティカルな安全インフラへと移行すると主張している。

• ガバナンスの空白：著者らは、現在の軌道上ベンチャーにはAIの決定に対するランタイム・ガバナンスが欠如しており、単一の計算ミスが地上での介入なしにノードやコンステレーションを破壊するという「存亡に関わるアーキテクチャ上のリスク」を生み出していると主張している。
• アーキテクチャ上の必要性：Glass Boxは、OSレベルのリソースマネージャーと同等の役割を軌道上で果たすものであり、AIワークロードが安全な制限を超えて物理的リソースを消費することを防ぐものである。
• スケーラビリティ：$O(N_c)$ の複雑性の保証により、宇宙機の制御ループに求められる決定論性を損なうことなく、ミッションの複雑さに応じてフレームワークをスケールさせることが可能であると主張されている。

著者が認める限界事項
論文では、すべての結果が現在シミュレーションのみであることを明示している。特定のシリコン（例：Google Coral TPU、ARM Cortex-M4）上での実機による測定結果は、本シリーズの今後の論文に取っておかれている。また、制約文法は現在、Project Octoberのプロファイルに特化した静的なものであり、ミッション固有の制約の自動合成は今後の課題として特定されている。マルチサテライト間のコンセンサスによるコンステレーションレベルのガバナンスについても、将来の出版物に委ねられている。