Verification of Unknown Dynamical Systems via Autoencoder Latent Space

기술적 요약: 오토인코더 잠재 공간을 통한 미지의 동적 시스템 검증

문제 정의
연속 공간 동적 시스템의 형식적 검증은 자율 시스템이 선형 시제 논리 (LTL) 로 종종 표현되는 안전성 및 생존성 명세를 만족하도록 보장하는 데 필수적입니다. 표준 접근법은 모델 검증을 가능하게 하기 위해 유한 상태 추상화를 구성하는 것을 포함합니다. 그러나 이러한 기법은 고차원 환경에서 심각한 확장성 문제에 직면합니다. 왜냐하면 추상화의 크기가 상태 공간 차원에 따라 기하급수적으로 증가하기 때문입니다. 이 문제는 신경망이 라이다 (LiDAR) 나 카메라 데이터를 처리하여 제어하는 등 동역학이 복잡하고, 부분적으로 미지이거나 블랙박스인 AI 기반 시스템에서 더욱 악화됩니다. 오토인코더와 같은 데이터 기반 차원 축소 기법이 확장성에 대한 잠재적 해결책을 제시하지만, 일반적으로 형식적 정확성 보장을 결여하고 있습니다. 구체적으로, 고차원 명세를 학습된 잠재 공간으로 매핑하고, 학습된 잠재 동역학이 (비결정성을 포함하여) 원래 시스템의 행동을 충실히 반영하도록 보장하는 것은 여전히 해결되지 않은 과제입니다. 기존 방법들은 종종 유연성을 위해 정확성을 희생하거나, 학습된 표현에는 적용되지 않는 시스템 동역학에 대한 강력한 가정에 의존합니다.

방법론
제안된 프레임워크는 차원 축소와 추상화 기반 검증을 결합하여 동역학이 미지인 고차원 시스템에 대한 형식적 보장을 제공함으로써 이러한 과제를 해결합니다. 이 접근법은 네 가지 주요 단계로 구성됩니다:

1. 볼록 오토인코더 아키텍처: 잠재 공간이 해석 가능하고 건전한 추론을 지원하도록 보장하기 위해, 저자들은 볼록 오토인코더를 사용합니다. 인코더는 특정 구조적 제약을 가진 입력 볼록 신경망 (ICNN) 으로 제한됩니다: 동형사상 (homeomorphisms) 으로 작용하기 위한 엄격하게 단조로운 활성화 함수, 단사적인 첫 번째 및 스킵 레이어, 그리고 풀랭크 (full-rank) 가중치 행렬입니다. 이 아키텍처는 "연결된 입력 - 연결된 출력 (CICO)" 네트워크라고 명명되며, 잠재 공간의 임의의 연결 집합의 전상 (pre-image) 이 원래 상태 공간의 연결 집합임을 보장합니다. 이 속성은 잠재 차원이 시스템의 최소 실현보다 낮을 때 매핑의 비단사성을 처리하는 데 중요합니다.

2. 포함 동역학 학습: 차원 축소로 인해 정보 손실이 발생할 수 있으므로, 잠재 공간에서의 진화는 결정론적 차분 방정식이 아닌 포함 동역학 (inclusion dynamics, 집합값) 으로 모델링됩니다. 저자들은 집합값 동역학을 위한 가우시안 프로세스 회귀 (GPR) 의 새로운 공식화인 "포함 가우시안 프로세스 (Inclusion GPs)"를 도입합니다. 이 방법은 동역학을 미관측 매개변수 $c$가 포함된 차분 방정식을 따르는 더 높은 차원의 공간으로 승격시킵니다. 이 미관측 좌표를 통합하는 딥 커널을 학습함으로써, 이 방법은 시스템의 진상을 집합 (구체적으로 잠재 공간 내의 공) 으로 예측하고 재현 커널 힐베르트 공간 (RKHS) 분석에 기반한 엄격한 오차 한계를 제공합니다.

3. 건전한 유한 추상화 구성: 학습된 포함 GP 를 사용하여 저자들은 잠재 공간에 비결정성 전이 시스템 (NTS) 을 구성합니다.

   • 영역 매핑: 고차원의 관심 영역 (안전, 위험, 목표 집합) 이 잠재 공간으로 매핑됩니다. 인코더의 볼록성으로 인해 이러한 집합에 대한 효율적인 샘플링 기반 하근사 및 확률적 상근사 ($\epsilon$-RandUp 사용) 가 가능합니다.
   • 전이 관계: 추상 상태 간의 전이는 회귀 오차와 미관측 매개변수 $c$를 고려하여 포함 GP 모델을 통해 영역을 전파함으로써 계산됩니다. 이는 추상화가 원래 시스템의 모든 가능한 행동을 보수적으로 포착하도록 보장합니다.
   • 정확성 보장: 이 프레임워크는 잠재 NTS 의 상태가 도달 - 회피 명세를 만족하면, 원래 고차원 시스템의 모든 해당 궤적이 높은 신뢰 수준 ($1-\delta$) 으로 명세를 만족함을 증명합니다.

4. 검증 및 디코딩: 표준 모델 검사 도구가 잠재 NTS 에 적용되어 명세를 만족하는 것이 보장된 상태 ($Q_{yes}$), 만족할 수 없는 상태 ($Q_{no}$), 그리고 불확실한 상태 ($Q_?$) 를 식별합니다. 인코더가 볼록하므로, 만족하는 잠재 상태는 볼록 최적화를 사용하여 원래 고차원 공간으로 효율적으로 디코딩되어 원래 시스템에서 안전이 보장된 초기 상태 집합을 식별할 수 있습니다.

주요 기여
이 논문은 네 가지 주요 기여를 합니다:

1. 증명 가능한 정확한 매핑: CICO 인코더를 사용하여 고수준 명세를 잠재 공간으로 매핑하는 방법으로, 형식적 보장을 유지하면서 압축된 표현에 대한 효율적인 추론을 가능하게 합니다.
2. 포함 GP: 명시적인 미관측 매개변수 지식이 필요 없이 차분 포함에 의해 지배되는 잠재 동역학을 학습할 수 있도록 하는 포함값 (집합값) 동역학을 위한 가우시안 프로세스 회귀의 새로운 공식화.
3. 건전한 추상화 프레임워크: 포함 GP 를 기반으로 잠재 공간에서 건전한 유한 추상화를 생성하는 완전한 프레임워크로, 원래 시스템으로의 만족 보장을 매핑하는 절차와 정확성 증명을 포함합니다.
4. 실증적 검증: 라이다 입력을 사용하는 신경망 제어기를 포함한 26 차원 시스템을 포함한 여러 시스템에 대한 접근법 시연으로, 기존 추상화 방법 대비 상당한 확장성 개선을 보여줍니다.

결과
이 접근법은 세 가지 사례 연구에서 평가되었습니다:

• 3D 에서 2D 로: 최소 실현 시스템으로, 이 방법은 전체 잠재 공간을 성공적으로 검증한 반면, 원래 3D 공간의 기존 데이터 기반 추상화는 느리게 움직이는 차원의 불확실성으로 인해 도달성 검증을 실패했습니다.
• 6D 에서 2D 로: 비선형 관측을 가진 과매개변수화 시스템입니다. 이 방법은 장애물이 없는 경우 잠재 공간의 100% 를 검증했고, 장애물이 있는 경우 59.78% 를 검증했습니다. 반면, 원래 6D 공간에서 추상화를 시도한 결과는 상태 폭발로 이어져 시간 제한 내에 목표 영역을 제외한 어떤 영역도 검증하지 못했습니다.
• 26D 에서 2D 로: 라이다 입력과 신경망 제어기를 가진 로봇 항법 작업입니다. 이 방법은 최소한의 비결정성으로 시스템의 동역학을 포착하는 2D 잠재 공간을 성공적으로 학습하여 잠재 공간의 50.0001% 를 검증했습니다. 이는 기존 방법들이 실현 불가능한 고차원 관측 공간을 처리할 수 있음을 보여주었습니다.

의의
이 논문은 차원 축소와 형식적 검증 사이의 중요한 간극을 메운다고 주장합니다. 명세 매핑과 학습된 잠재 동역학 모두에 대한 건전성 보장을 제공함으로써, 학습 기반 제어에서 흔한 문제인 검증 결과의 위양성을 제거합니다. 저자들은 이 접근법이 동역학이 미지인 고차원 시스템에 대한 확장 가능한 검증을 가능하게 한다고 강조하며, 이는 기존 형식적 방법으로는 이전까지 달성할 수 없었던 능력이라고 말합니다. 프레임워크는 건전하지만, 저자들은 볼록 인코더로 제한됨 (표현력 제한) 과 노이즈 통합 및 제어 합성에 관한 미해결 문제 등 한계를 겸손하게 지적하며, 이를 향후 연구 방향으로 식별했습니다.