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

기술 요약: Glass Box at Orbit

문제 정의
본 논문은 궤도 컴퓨팅(orbital computing) 분야에서 나타나고 있는 중대한 거버넌스 공백을 다룹니다. 우주 산업이 인간의 개입(human-in-the-loop) 없이 수천 개의 자율 AI 워크로드를 실행하는 "궤도 데이터 센터"(예: Microsoft, AWS, Starcloud의 이니셔티브)로 전환됨에 따라, AI의 결정을 물리적 안전 제약 조건에 대해 검증할 수 있는 기존의 런타임 메커니즘이 존재하지 않습니다. 현재의 안전 패러다임은 불충분합니다:

• 사전 배포 정형 검증(Pre-deployment formal verification) (모델 체킹, 정리 증명)은 학습된 AI 시스템에 대해 불완전합니다. 이는 방사선으로 인해 왜곡된 가중치나 일식 진입 시의 전력 상태와 같은 분포 외(out-of-distribution) 조건을 고려할 수 없기 때문입니다.
• **사후 배포 결함 탐지(FDIR)**는 사후 대응적입니다. 이는 하드웨어 고장이 발생한 후에 이를 식당할 뿐, AI가 생성한 명령이 돌이킬 수 없는 손상(예: 일식 기간 동안 배터리를 심방전 임계값 이하로 방전시키는 것)을 일으키기 전에 차단하지 못합니다.

핵심 문제는 AI의 행동이 우주선 액추에이터에 도달하기 전에 이를 가로채어, 결정이 궤도 물리학의 범위 내에 머물도록 보장할 수 있는 **런타임 헌법적 검증 계층(runtime constitutional verification layer)**의 부재입니다.

방법론: Glass Box 프레임워크
저자들은 CubeSat을 위한 5계층 자율 궤도 지능 아키텍처인 "Project October"에 통합된 런타임 검증 계층인 Glass Box를 제안합니다. Glass Box는 온보드 AI 정책과 우주선 서브시스템 사이의 게이트키퍼 역할을 수행합니다.

1. 궤도 디지털 트윈 (Orbital Digital Twin, ODT): Glass Box는 궤도, 전력, 열, 방사선 및 자세 역학에 대한 실시간 상태 벡터를 제공하는 물리적으로 정확한 디지털 트윈(Orekit 및 NASA GMAT 사용)에 의존합니다.
2. 헌법적 제약 문법 (Constitutional Constraint Grammar): AI 정책으로부터 도출된 모든 후보 행동($a_t$)은 여섯 가지 폐쇄형(closed-form) 물리 기반 제약 조건($C_1$ ~ $C_6$)에 대해 평가됩니다:
   • C1 (전력 안전 마진): 발전량이 부하와 안전 버퍼를 초과하는지 확인합니다.
   • C2 (열 경계): $[-20^\circ\text{C}, +70^\circ\text{C}]$ 범위 내에서 작동하는지 검증합니다.
   • C3 (충돌 회피): 합병 확률(conjunction probability)을 $10^{-4}$ 이상으로 높이는 기동을 거부합니다.
   • C4 (배터리 하한선): 충전 상태(SOC)가 $20\%$ 미만인 경우 비필수 운영을 중단합니다.
   • C5 (방사선 결함 게이트): 단일 이벤트 업셋(SEU) 발생률이 임계값을 초과하면 삼중 모듈 중복(TMR)을 강제합니다.
   • C6 (베이지안 신뢰도 게이트): 예측 엔트로피(Monte Carlo Dropout을 통한)가 임계값을 초과하여 방사선으로 오염된 모델 출력이 감지되면 행동을 차단합니다.
3. LTL 안전 불변성 (LTL Safety Invariants): 시간 경과에 따른 행동 시퀀스를 검증하기 위해 7개의 선형 시제 논리(LTL) 불변성이 정의됩니다 (예: "이상 징이 플래그된 경우, 두 궤도 주기 내에 다운링크가 수행되어야 한다"). 이는 Z3 및 NuSMV 모델 체커를 사용하여 검증됩니다.
4. 검증 로직: 검리기는 세 가지 상태 중 하나를 출력합니다: APPROVE(행동이 안전함, 설명 가능성 점수와 함께 로그 기록), FLAG(위반이 감지되었으나 심각도가 낮음, 다운링크 대기열에 추가, 안전한 기본값으로 대체), BLOCK(심각도가 높음, 명령 취소, 세이프 모드 트리거).
5. 설명 가능성 (Explainability): 승인된 모든 결정에는 가중치가 부여된 설명 가능성 점수 $E(a_t) \in [0, 1]$와 전체 감사 로그가 할당되며, 이는 접촉이 없는 기간 동안의 모든 자율적 결정에 대한 상세 내용을 포함합니다.

주요 기여
본 논문은 다섯 가지 구체적인 기여를 합니다:

• C1. 헌법적 제약 문법: 전력, 열, 충돌, 배터리, 방사선 및 신뢰도를 다루는 6가지 제약 조건을 구성하며, 이는 실시간 궤도 물리학에 대한 술어(predicate)로 정식화되었습니다.
• C2. LTL 안전 명세: 순간적인 제약을 궤도 궤적에 따른 행동 보장으로 확장하는 7개의 시제 논리 불변성을 제시합니다.
• C3. $O(N_c)$ 검증 복잡도 정리: Glass Box의 검증 오버헤드가 헌법 규칙의 수($N_c$)에 선형적이며, AI 모델의 크기나 우주선 상태 차원과는 독립적이라는 것을 입증하는 정식 증명을 제공합니다.
• C4. 설명 가능성 아키텍처: 접촉이 없는 시간 동안의 모든 자율적 결정에 대해 가중치 점수와 완전한 감사 로그를 제공하는 메커니즘입니다.
• C5. 작업 예시: 일식 진입 전 불충고한 추론 요청을 Glass Box가 차단하는 상세 시뮬레이션을 통해, 미션 생존성을 보존하기 위해 작업을 유예하는 과정을 보여줍니다.

결과 및 검증
논문은 완전히 시뮬레이션된 환경(Project October Phase I)을 바탕으로 한 결과를 제시합니다:

• 복잡도: 검증 프로세스가 $O(N_c)$임이 증명되어, 규칙을 추가하더라도 서브 와트급 임베디드 프로세서(예: ARM Cortex-M4)의 타이밍 병목 현상을 일으키지 않음을 보장합니다.
• 시뮬레이션 사례 연구: 배터리 여유량이 고갈된 상태에서 일식 진입 3분 전 산불 관련 추론 요청이 제안된 시나리오에서, Glass Box는 전력 위반($c_1 = \bot$)을 정확히 식별했습니다. 미션 전체를 차단하는 대신, 태양광 발전이 회복될 때까지 6분간 추론을 유예하도록 FLAG 처리를 했습니다. 이를 통해 배터리 심방전 이벤트를 방지하면서도 미션 목표를 달착할 수 있었습니다.
• 정형 검증: 7개의 LTL 불변성이 Z3 및 NuSMV를 사용하여 제약 문법에 대해 기계적으로 검증되었으며, 이를 통해 안전 로직의 일관성을 확인했습니다.

의의 및 주장
본 논문은 궤도 컴퓨팅이 데이터 센터 인프라로 확장됨에 따라, 런타임 헌법적 검증이 연구적 참신함을 넘어 미션 크리티컬 안전 인프라로 전환된다고 주장합니다.

• 거버넌스 공백: 저자들은 현재의 궤도 벤처들이 AI 결정에 대한 런타임 거버넌스가 결여되어 있으며, 이는 단 한 번의 계산 착오가 지상 개입 없이 노드나 군집(constellation)을 파괴할 수 있는 "존립적 아키텍처 리스크"를 생성한다고 주장합니다.
• 아키텍처적 필요성: Glass Box는 AI 워크로드가 물리적 자원을 안전한 한계 이상으로 소비하는 것을 방지하는, 궤도 상의 OS 레벨 리소스 관리자와 같은 역할을 하도록 제시됩니다.
• 확장성: $O(N_c)$ 복잡도 보장은 프레임워크가 우주선 제어 루프에 필요한 결정론을 해치지 않으면서 미션 복잡성에 따라 확장될 수 있음을 주장합니다.

저자가 인정한 한계점
논문은 모든 결과가 현재 시뮬레이션 전용임을 명시적으로 밝히고 있습니다. 특정 실리콘(예: Google Coral TPU, ARM Cortex-M4)에서의 측정된 하드웨어 결과는 시리즈의 후속 논문을 위해 남겨두었습니다. 또한, 제약 문법은 현재 정적이며 Project October 프로필에 특화되어 있습니다. 미션별 제약 조건의 자동 합성을 향후 과제로 식별하였으며, 군집 수준의 거버넌스를 위한 다중 위성 합의 역시 차기 출판물로 미루어 두었습니다.