Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis

1. 연구 배경 및 문제 정의 (Problem)

• 배경: 자율 시스템의 퍼셉션 기반 (perception-based) 제어기가 현실 세계에 널리 적용되고 있지만, 센서 노이즈, 학습 오류, 환경적 요인 (예: 터널 내 GPS 신호 손실) 등으로 인한 지각 불확실성 (perceptual uncertainty) 이 존재합니다.
• 문제: 이러한 불확실성 하에서도 시스템의 안전성과 성능을 형식적으로 검증 (formal verification) 하는 것은 매우 어렵습니다.
  • 기존 접근법 (NNV 등) 은 신경망 (NN) 검증 도구와 근사 도달 집합 (approximate reachable set) 방법을 결합하지만, 과도한 보수성 (overly conservative) 을 보이거나 특정 클래스의 시스템/제어기에만 제한되는 단점이 있습니다.
  • 기존의 해밀턴 - 야코비 (HJ) 도달성 분석은 비선형 시스템에 대한 최적 도달 집합을 계산할 수 있으나, 제어기가 완벽한 상태 정보를 가진다고 가정하여, 지각 불확실성이 있는 시스템에는 직접 적용하기 어렵습니다.
• 목표: 지각 불확실성 (worst-case perceptual errors) 을 고려하더라도, 자율 시스템 (예: 항공기, 로버) 이 안전 영역을 벗어나지 않음을 형식적으로 보장할 수 있는 검증 프레임워크를 개발하는 것.

2. 제안 방법론: RoVer-CoRe (Methodology)

저자들은 RoVer-CoRe (Robust Verification of Controllers via HJ Reachability) 라는 새로운 프레임워크를 제안합니다. 이는 지각 불확실성 하의 시스템을 검증하기 위해 HJ 도달성 분석을 확장한 첫 번째 프레임워크입니다.

핵심 아이디어: 폐루프 시스템 추상화 (Closed-Loop System Abstraction)

기존 HJ 분석은 제어기가 실제 상태 $x$를 알고 있다고 가정하지만, RoVer-CoRe 는 다음과 같이 시스템을 재구성합니다.

1. 연결 (Concatenation): 제어기 ($\pi$), 관측 함수 ($p$), 상태 추정기 ($q$) 를 하나의 통합된 폐루프 동역학으로 결합합니다.
   • 새로운 동역학: $h(x, d, e) := f(x, \pi(q(p(x), e)), d)$
   • 여기서 $d$는 외부 교란, $e$는 지각 오차 (perceptual error) 입니다.
2. 입력 변환: 이 추상화를 통해 시스템의 외부 입력은 오직 교란 $d$와 지각 오차 $e$만 남게 되며, 이는 기존 HJ 도달성 도구로 처리 가능한 형태로 변환됩니다.

해밀토니안 (Hamiltonian) 계산 및 경계 설정

폐루프 시스템의 해밀토니안 계산이 주요 기술적 난제입니다. 제어기의 복잡도 (비선형성, 블랙박스 등) 에 따라 두 가지 방법을 제안합니다.

1. 정확한 계산 (Exact Computation):
   • 제어기가 선형 피드백이거나 이산적 (grid-based) 인 경우, 최적화 문제를 정확히 풀어 해밀토니안을 계산합니다.
   • 이 경우 보수성 없이 정확한 안전 보장을 제공합니다.
2. 하한 경계 설정 (Lower Bounding):
   • 신경망 (NN) 등 복잡한 제어기의 경우, 해밀토니안을 정확히 풀기 어렵습니다.
   • 대신, 지각 불확실성 하에서 제어기 출력의 하한과 상한 ($\underline{U}(x), \overline{U}(x)$) 을 구합니다 (예: $\alpha,\beta$-CROWN 같은 NN 검증 도구 사용).
   • 이를 통해 보수적이지만 안전한 (sound) 하한 해밀토니안을 계산하여 검증합니다.
   • 주의: 이 방법의 보수성은 출력 공간의 과대 추정 (over-approximation) 정도에 비례합니다.

강인한 제어기 설계 (Robust Controller Design)

검증 결과를 활용하여 제어기를 개선합니다.

• 하이퍼파라미터 최적화: 다양한 제어기 파라미터 ($\alpha$) 에 대해 RoVer-CoRe 를 실행하여, 안전 마진 (safety margin) 이 최대가 되는 파라미터를 선택합니다.
• 안전 가이드 설계: 불확실성이 증가하는 시나리오 (예: 로버의 헤드라이트 끄기) 에서 안전을 유지할 수 있는 운영 전략을 수립합니다.

3. 주요 기여 (Key Contributions)

1. RoVer-CoRe 프레임워크: 지각 불확실성 하의 퍼셉션 기반 시스템을 검증하기 위한 최초의 HJ 도달성 기반 프레임워크를 제안했습니다.
2. 검증 및 설계 방법론: 불확실성 하에서 형식적 안전 검증을 수행하고, 이를 통해 강인한 제어기를 설계하는 새로운 방법론을 제시했습니다.
3. 실증 사례 및 오픈 소스: 항공기 택싱 (aircraft taxiing) 과 NN 기반 로버 항법 (rover navigation) 사례를 통해 프레임워크의 유효성을 입증했으며, 관련 코드를 오픈 소스로 공개했습니다.

4. 실험 결과 (Results)

두 가지 사례 연구를 통해 RoVer-CoRe 의 성능을 입증했습니다.

사례 1: 항공기 택싱 (Aircraft Taxiing)

• 상황: 카메라 기반 DNN 이 횡방향 오차와 heading 오차를 추정하여 제어하는 항공기.
• 결과:
  • 지각 오차의 커버리지 (coverage) 가 0.9968 까지 증가해도 초기 상태의 안전성을 형식적으로 검증할 수 있음을 보였습니다.
  • 기존 제어기 (안전하지 않음) 와 RoVer-CoRe 로 최적화된 제어기 (안전) 를 비교하여, 최적화된 제어기가 최악의 지각 오차 하에서도 안전을 유지함을 시각화했습니다.
  • 실패 모드 분석을 통해 특정 게인 (gain) 이 과잉 보정 (over-correction) 을 유발하는 원인을 규명했습니다.

사례 2: NN 기반 로버 항법 (NN-Based Rover Navigation)

• 상황: NASA 의 달 탐사 개념 (Endurance) 에서 영감을 받아, 어두운 환경에서 헤드라이트를 끄고 주행할 때 발생하는 누적 오차를 고려한 로버.
• 결과:
  • MPC vs NN: 그리드 기반 MPC 와 이를 모방한 NN 제어기를 비교했습니다. NN 의 경우 $\alpha,\beta$-CROWN 을 사용하여 경계를 구했고, 결과적으로 MPC 보다 더 보수적이지만 안전한 도달 튜브 (BRT) 를 계산했습니다.
  • 정확성 비교: 무작위 몬테카를로 시뮬레이션 (10,000 회) 과 비교했을 때, RoVer-CoRe 는 몬테카를로가 놓친 많은 위험 상태를 정확히 식별했습니다.
  • 에너지 효율적 안전 설계: 헤드라이트를 켜야 하는 시점을 계산하여, 불필요한 에너지 소모를 줄이면서도 안전을 보장하는 정책을 자동 생성했습니다. NN 제어기는 MPC 보다 더 일찍 헤드라이트를 켜야 함을 발견하여, 제어기의 강인성 차이를 정량화했습니다.

5. 의의 및 결론 (Significance)

• 보수성 극복: 기존 근사 도달 집합 방법 (Set-based methods) 이 가진 과도한 보수성을 해결하고, HJ 도달성 분석을 통해 더 정밀하고 최적에 가까운 안전 보장을 제공합니다.
• 범용성: 비선형, 비볼록, 학습 기반 (NN) 인 블랙박스 제어기를 포함하는 복잡한 시스템에도 적용 가능합니다.
• 실용적 가치: 단순히 "안전하다/아니다"를 판단하는 것을 넘어, 어떤 조건에서 실패하는지 (failure modes) 를 진단하고, 이를 바탕으로 강인한 제어기를 설계할 수 있게 합니다.
• 미래 전망: 확률적 불확실성 모델 통합, 학습 기반 도달성 도구를 통한 확장성 개선, 더 풍부한 지각 파이프라인 적용 등을 향후 과제로 제시했습니다.

요약하자면, 이 논문은 자율 시스템의 지각 불확실성을 수학적으로 엄밀하게 다루어, 기존 방법론보다 더 정밀하고 실용적인 안전 검증 및 제어기 설계 도구를 제공한다는 점에서 큰 의의가 있습니다.