Forward and Backward Reachability Analysis of Closed-loop Recurrent Neural Networks via Hybrid Zonotopes

이 논문은 ReLU 활성화 함수를 가진 폐루프 순환 신경망 (RNN) 시스템의 정확한 전방 및 후방 도달 가능 집합을 계산하기 위해 하이브리드 쥬노토프를 기반으로 한 새로운 접근법을 제시하고, 삼각형 면적 점수를 활용한 선택적 볼록 완화 기법을 통해 계산 복잡성과 근사 정확도 간의 균형을 조절하며 시스템 안전성을 검증하는 방법을 제안합니다.

핵심

🎬 비유: "미래를 예측하는 예언가 (RNN) 와 안전 검사관"

1. 문제 상황: 예언가의 불안정한 마음

우리가 사용하는 많은 AI(예: 자율주행차, 드론, 로봇) 는 과거의 데이터를 기억하며 미래를 예측하는 RNN이라는 두뇌를 가지고 있습니다.
하지만 이 두뇌는 때때로 매우 민감하게 반응합니다. 아주 작은 입력 변화에도 "어? 이거 위험해!"라고 갑자기 비명을 지르거나, 반대로 "아무 문제 없어!"라고 잘못 판단할 수 있습니다.

이런 AI 가 **안전한지 (Safety)**를 확인하려면, "지금 이 상태에서 시작해서 5 초 뒤, 10 초 뒤에 어디로 갈까?"를 미리 계산해봐야 합니다. 이를 **'도달 가능 영역 (Reachable Set)'**이라고 합니다.

• 앞으로의 도달 (Forward): 지금 여기서 출발하면 미래에 어디까지 갈 수 있을까?
• 뒤로 돌아보기 (Backward): 저 위험한 곳에 도달하려면, 출발점은 어디였을까?

2. 기존 방법의 한계: "과거를 모두 펼쳐보라"

기존에는 AI 의 예측을 검증할 때, 시간을 하나씩 쭉 펼쳐서 (Unrolling) 보았습니다. 마치 100 단계를 예측하려면 100 개의 AI 를 나란히 붙여놓고 계산하는 것과 같습니다.

• 단점: 시간이 지날수록 계산량이 기하급수적으로 불어나서, 컴퓨터가 미쳐버립니다 (계산 불가능).

3. 이 논문의 혁신: "하이브리드 존토프 (Hybrid Zonotopes)"라는 마법 상자

이 연구팀은 **"시간을 펼쳐보지 않고도, 과거와 미래의 관계를 한 번에 파악하는 마법 상자"**를 만들었습니다. 이를 **'하이브리드 존토프'**라고 부릅니다.

• 상태 쌍 (State-Pair Set) 비유:
  보통은 "시작점 A"와 "끝점 B"를 따로따로 봅니다. 하지만 이 연구팀은 **"시작점 A 와 끝점 B 가 짝을 이룬 상태"**를 하나의 덩어리로 묶어서 관리합니다.
  • 마치 **"출발지와 도착지를 한 장의 티켓에 모두 찍어두는 것"**과 같습니다. 이렇게 하면 AI 가 어떻게 움직였는지 (과거의 숨겨진 상태) 를 추적하면서도, 계산량을 폭발시키지 않고 정확한 경로를 그릴 수 있습니다.

4. 핵심 기술: "불안정한 부분만 골라 다듬기" (Tunable Relaxation)

AI 의 두뇌에는 ReLU라는 활성화 함수가 있는데, 이는 "0 이하면 0, 0 이하면 그대로"라는 식으로 작동합니다. 이 부분이 계산할 때 가장 복잡하고 까다롭습니다.

이 연구팀은 모든 복잡한 부분을 다 정확히 계산하면 컴퓨터가 버거워하므로, 중요하지 않은 부분만 살짝 둥글게 다듬는 (Relaxation) 전략을 썼습니다.

• 삼각형 점수 (Triangle-Area Score):
  "어디가 가장 불안정하고 계산이 많이 필요한가?"를 측정하는 점수입니다.
  • 점수가 높은 (위험한) 부분: 정확히 계산합니다. (안전이 최우선이니까요)
  • 점수가 낮은 (안전한) 부분: 계산이 쉬운 '삼각형' 모양으로 대충 근사합니다.
• 조절 가능한 스위치: 연구자는 "얼마나 정확한가?"와 "얼마나 빠르게 계산하는가?" 사이에서 스위치를 조절할 수 있습니다.
  • "완벽한 안전이 필요하다?" → 모든 부분을 정확히 계산 (비쌈).
  • "빠른 대략적인 확인이 필요하다?" → 위험한 부분만 정확히, 나머지는 대충 계산 (빠름).

5. 안전 검증: "위험한 길 찾기"

이 방법을 사용하면 두 가지 중요한 일을 할 수 있습니다.

1. 안전 확인: "이 출발점에서 시작하면, 절대 위험한 구역 (예: 벽, 다른 차) 에 닿지 않는다"는 것을 수학적으로 증명합니다.
2. 위험 경로 찾기: "만약 위험한 곳에 닿았다면, 출발점은 어디였을까?"를 역추적하여, 어떤 입력이 AI 를 망가뜨렸는지 찾아냅니다.

📝 요약: 이 논문이 왜 중요한가?

1. 시간을 거꾸로 거슬러도 가능: 과거와 미래를 동시에 정확히 추적할 수 있는 새로운 수학적 도구를 개발했습니다.
2. 계산량 조절 가능: "정확함"과 "빠름" 사이에서 사용자가 원하는 대로 균형을 잡을 수 있습니다. (필요할 때는 완벽하게, 급할 때는 대략적으로)
3. 실제 적용 가능: 자율주행차나 로봇처럼 안전이 생명인 분야에서 AI 가 실수하지 않도록 검증하는 데 쓸 수 있습니다.

한 줄 평:

"이 연구는 복잡한 AI 의 미래를 예측할 때, 시간을 쭉 펼치지 않고도 '시작과 끝을 짝지어' 계산하며, 중요한 부분만 꼼꼼히, 나머지는 대충 처리해서 안전하고 빠른 검증을 가능하게 한 혁신적인 방법입니다."

기술 요약

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

• 배경: 순환 신경망 (RNN) 은 은닉 상태 (hidden state) 구조를 통해 시간적 의존성을 자연스럽게 포착하여 복잡한 동적 시스템 모델링, 상태 추정, 제어 등에 널리 사용됩니다. 특히 폐루프 (closed-loop) 시스템에서 RNN 기반 제어기는 안전-중요 (safety-critical) 응용 분야에 적용되고 있습니다.
• 문제점:
  • RNN 은 입력 교란에 민감하고 폭발적인 기울기 문제 등 이론적 특성이 아직 완전히 규명되지 않았습니다.
  • 기존 RNN 검증 연구는 주로 전방 도달 가능성 (Forward Reachability) 분석에 집중되었으며, 후방 도달 가능성 (Backward Reachability) 분석 (예: 적대적 입력 시퀀스 식별, 안전한 제어 합성) 은 거의 다루지 않았습니다.
  • 기존 방법론인 '언롤링 (Unrolling, 시계열을 피드포워드 네트워크로 확장)'은 시간 단계가 증가함에 따라 네트워크 크기가 급격히 커져 확장성이 떨어집니다. 반면 '불변성 추론 (Invariant Inference)'은 오차 누적로 인해 불확실한 결과를 초래할 수 있습니다.
• 목표: ReLU 활성화 함수를 사용하는 폐루프 RNN 시스템에 대해 정확한 (Exact) 전방 및 후방 도달 가능 집합 (Reachable Sets) 을 계산하고, 이를 통해 시스템의 안전성을 검증할 수 있는 확장 가능한 방법론을 제안하는 것입니다.

2. 제안된 방법론 (Methodology)

이 논문은 **하이브리드 존토프 (Hybrid Zonotopes, HZ)**를 기반으로 한 새로운 집합 기반 접근법을 제시합니다.

가. 하이브리드 존토프 (Hybrid Zonotopes)

• 연속 생성자 (continuous generators) 와 이진 생성자 (binary generators) 를 모두 사용하여 집합을 표현합니다.
• 선형 변환, 일반화된 교집합 (generalized intersection), ReLU 함수의 그래프 등을 정확히 표현할 수 있는 강력한 수학적 도구입니다.

나. 상태 쌍 집합 (State-Pair Sets) 및 정밀 도달 가능성 계산

• 핵심 아이디어: RNN 의 시간적 의존성 (과거 상태와 현재 상태의 연결) 을 해결하기 위해 '언롤링' 없이 **상태 쌍 집합 (State-Pair Set, $S_x$)**을 정의합니다. 이는 초기 상태 $x_1$과 $t$단계 상태 $x_t$ 사이의 관계를 하이브리드 존토프로 직접 표현합니다.
• 알고리즘 1 (정밀 계산):
  1. 각 시간 단계와 레이어에서 은닉 상태 쌍 집합 (Hidden-state-pair set) 을 구성합니다.
  2. ReLU 함수의 그래프를 하이브리드 존토프로 정확히 표현합니다 (Lemma 2).
  3. 선형 매핑과 일반화된 교집합 연산을 통해 전체 시스템의 상태 쌍 집합을 전파합니다.
  4. 이를 통해 **정확한 전방 도달 가능 집합 (FRS)**과 **후방 도달 가능 집합 (BRS)**을 하이브리드 존토프 형태로 도출합니다 (Theorem 1).

다. 확장성을 위한 조절 가능한 완화 기법 (Tunable Relaxation Scheme)

• 문제: 정확한 ReLU 그래프 표현은 이진 생성자 (binary generators) 를 증가시켜 계산 복잡도가 급증합니다.
• 해결책:
  • 삼각형 면적 점수 (Triangle-Area Score): 불안정한 ReLU 단위 (입력 구간이 0 을 포함하는 경우) 에 대해, ReLU 그래프와 삼각형 완화 (convex relaxation) 사이의 '삼각형 영역' 크기를 점수로 매깁니다.
  • 선택적 완화: 점수가 높은 (영향이 큰) ReLU 는 정확한 그래프로 유지하고, 점수가 낮은 (영향이 작은) ReLU 만 삼각형 완화 (이진 생성자 제거) 를 적용합니다.
  • 이진 제한 파라미터 ($N_b$): 완화된 ReLU 의 수를 제한하여 계산 복잡도와 정확도 사이의 균형을 조절합니다. $N_b$가 충분히 크면 정확한 도달 가능성과 동일해집니다.
• 알고리즘 2: CROWN 등을 사용하여 입력 구간을 추정하고, 점수에 따라 ReLU 를 순위 매겨 완화 여부를 결정합니다.

라. 안전성 검증 (Safety Verification)

• 전방 접근: 초기 집합에서 시작하여 도달 가능한 집합이 위험 영역 (Unsafe set) 과 교차하는지 확인합니다.
• 후방 접근: 위험 영역에서 역으로 도달 가능한 초기 상태 집합을 계산하여, 초기 집합과 교차하는지 확인합니다.
• 충분 조건: 계산된 도달 가능 집합이 위험 영역과 교차하지 않으면 시스템이 안전하다고 보장할 수 있습니다 (Proposition 3).

3. 주요 기여 (Key Contributions)

1. 정밀한 도달 가능성 계산: 언롤링 없이 하이브리드 존토프를 사용하여 폐루프 RNN 의 전방 및 후방 도달 가능 집합을 정확하게 계산하는 방법을 최초로 제안했습니다.
2. 확장성 있는 조절 완화 기법: 삼각형 면적 점수를 기반으로 불안정한 ReLU 를 순위 매겨 선택적으로 완화하는 기법을 도입했습니다. 이를 통해 계산 복잡도와 근사 정확도 사이의 명시적인 트레이드오프를 가능하게 했으며, 정확한 도달 가능성을 특수한 경우로 포함합니다.
3. 안전성 검증 프레임워크: 계산된 도달 가능 집합을 활용하여 폐루프 RNN 시스템의 안전성을 검증하고, 위험한 시퀀스를 식별할 수 있는 충분 조건을 유도했습니다.

4. 실험 결과 (Results)

• 시뮬레이션 환경: 질량 - 스프링 - 댐퍼 시스템 (2 대의 카트) 을 대상으로 MPC 제어기를 RNN 으로 근사화하고, 이를 다시 RNN 으로 모델링한 폐루프 시스템을 구성했습니다.
• 정확성: 제안된 방법 (알고리즘 2) 으로 계산된 근사 도달 가능 집합은 정확한 집합을 완전히 포함하는 것으로 확인되었습니다.
• 확장성 및 조절성:
  • 이진 제한 파라미터 ($N_b$) 를 증가시킬수록 근사 도달 가능 집합의 크기가 감소하며 정확도가 향상됨을 보였습니다 (그림 3).
  • $N_b$를 충분히 크게 설정하면 정확한 도달 가능 집합과 일치함을 확인했습니다.
• 후방 도달 가능성 활용: 특정 위험 영역에 도달할 수 있는 초기 상태 집합 (BRS) 을 계산하고, 이를 통해 위험한 상태 시퀀스를 명시적으로 구성하는 데 성공했습니다 (그림 5).

5. 의의 및 결론 (Significance)

• 이론적 기여: RNN 기반 제어 시스템의 안전성 분석에 있어 전방뿐만 아니라 후방 도달 가능성 분석을 체계적으로 수행할 수 있는 첫 번째 방법론을 제시했습니다. 이는 적대적 공격 탐지 및 안전한 제어 합성에 중요한 기여를 합니다.
• 실용적 가치: 기존 언롤링 방식의 확장성 한계를 극복하고, 하이브리드 존토프의 정밀함과 완화 기법의 효율성을 결합하여 실제 제어 시스템에 적용 가능한 검증 도구를 제공합니다.
• 향후 전망: 비선형 식물 모델이나 다른 신경망 아키텍처 (FNN, CNN) 로의 확장이 가능하며, 계산 효율성 향상이 향후 연구 과제로 제시되었습니다.

요약하자면, 이 논문은 하이브리드 존토프를 활용하여 폐루프 RNN 시스템의 전방/후방 도달 가능성을 정밀하게 분석하고, 계산 복잡도를 조절 가능한 완화 기법을 통해 실용적인 안전성 검증을 가능하게 한 획기적인 연구입니다.