기술 요약: 강화 학습 정책 검증에 관한 조사 연구

1. 문제 정의

강화 학습(Reinforcement Learning, RL)은 자율 주행 및 에너지 시스템과 같은 안전 필수 영역(safety-critical domains)에 점점 더 많이 배치되고 있습니다. 그러나 고위험 환경에서 RL 에이전트를 배포하는 것은 엄격한 행동 보증(behavioral guarantees)의 부재로 인해 어려움을 겪고 있습니다. RL 정책은 일반적으로 복잡하고 비선형적인 결정 경계를 가진 심층 신경망(Deep Neural Networks, DNN)으로 구현되며, 이는 희귀한 조건, 분포 변화(distribution shifts) 또는 상호작作用 효과 하에서 불안전한 동작을 보일 수 있습니다.

고정된 분포에서의 입력-출력 강건성(robustness)으로 올바름을 정의하는 지도 학습과 달리, RL의 올러름은 근본적으로 실행 중 발생하는 상호작용, 피드백, 그리고 분포 변화에 달려 있습니다. RL 정책은 폐쇄 루프 제어(closed-loop control)를 통해 자신이 마주할 상태 분포를 능동적으로 형성합니다. 이는 오차 누적, 희귀 이벤트 실패, 그리고 장기적인 관점에서 나타날 수 있는 안전 위반(예: 매 시간 단계마다 강건한 정책이라 할지라도 누적된 오차로 인해 실패할 수 있음)을 초导致합니다. 결과적으로, RL의 검증 목표는 정적인 입력-출력 분석으로 축소될 수 없으며, 시간적 의존성, 정책-환경 간의 결합, 그리고 배포 시점의 불확실성을 반드시 고려해야 합니다.

현재 RL 검증에 관한 문헌은 개념적으로 파편화되어 있습니다. 방법론들이 서로 다른 가정하에 개발되고, 서로 다른 정당성(correctness) 개념을 목표로 하며, 서로 다른 시간적 범위(temporal scopes)에서 작동하기 때문에, 접근 방식들을 비교하거나 그들의 근본적인 관계를 이해하기 어렵습니다.

2. 방법론 및 분류 체계

본 논문은 훈련된 신경망 기반 정책에 대한 기존의 사후 검증(post-training verification) 방법들을 정리하기 위해 **통합된 분류 체계(unified taxonomy)**를 도입합니다. 이 분류 체계는 세 가지 주요 축을 따라 접근 방식들을 분류합니다:

1. 검증 패러다임 (Verification Paradigm): 형식적(Formal) 방법(충족 가능성(satisfiability) 또는 도달 가능성(reachability)을 통해 건전하고 결정론적인 보증을 제공)과 확률적(Probabilistic) 방법(리스크를 정량화하고 확률적 환경에서 높은 신뢰도의 보증을 제공)을 구분합니다.
2. 시간적 범위 (Temporal Scope):
   • 단계별 (Step-wise): 미래의 역학(dynamics)을 추상화하여 주어진 상태에서의 단일 정책 결정을 분석합니다. 이는 가장 성숙한 도구 클래스입니다.
   • 다단계 (Multi-step): 정책과 환경 사이의 상호작용을 포착하여, 유한 또는 무한한 호라이즌(horizon) 동안의 궤적 수준 또는 폐쇄 루프 동작을 추론합니다.
3. 보증 강도 (Guarantees Strength): 건전하고 완전함(Sound & Complete) (정확한 검증)에서부터 건전함(Sound) (과대 근사/over-approximations), 그리고 확률적(Probabilistic) (통계적 경계)에 이릅니다.

또한, 이 분류 체계는 방법론이 상당한 추상화나 재구성 없이 훈련된 RL 정책에 직접 적용될 수 있는지 여부를 나타내는 "RL 준비도(RL Readiness)" 축을 포함합니다.

주요 검증 정식화

• 단계별 검증 (Step-wise Verification): 정책이 주어진 국소 입력 영역 $X$ 내에서 안전하지 않은 행동을 선택하는지 확인하는 것으로 정식화됩니다. 이는 주로 다음과 같은 신경망 검증 문제로 매핑됩니다:
  • 충족 가능성 (SAT): 반례가 되는 입력을 탐색 (NP-hard).
  • 도달 가능성 (Reachability): 추상 해석(Abstract Interpretation) 또는 선형 완화(Linear Relaxation) 등을 통해 도달 가능한 출력 집합의 과대 근사치를 계산.
  • 확률적 (Probabilistic): 특정 노이즈 모델을 가정하지 않고 안전하지 않은 행동의 발생 가능성을 추정 (예: PT-LiR lipschitz-based approach 등).
• 다단계 검증 (Multi-step Verification): 폐쇄 루프 궤적이 안전하지 않은 상태에 도달하는지 판단하는 것으로 정식화됩니다. 접근 방식에는 다음이 포함됩니다:
  • 레이블된 MDP 및 템포럴 로직 (Labeled MDPs & Temporal Logic): 선형 템포럴 로직(LTL)을 사용하여 궤적 속성을 명시하고, 이를 정책에 의해 유도된 MDP와 오토마톤(automaton)의 곱 위에서 검증.
  • 뉴로-심볼릭 인증서 (Neuro-Symbolic Certificates): 학습된 정책을 제어 이론적 인증서(예: 제어 장벽 함수(Control Barrier Functions), 리아푸노프 함수(Lyapunov functions))와 결동하여 런타임 시 안전성을 강제.
  • 확률적 다단계 (Probabilistic Multi-step): 샘플링 또는 확률적 경계 전파를 통해 궤적에 대한 템포럴 속성 만족 확률을 추정.
• 열거 기반 검증 (Enumeration-based Verification): 안전하지 않은 행동으로 이어지는 모든 입력의 집합(preimage)을 계산하는 신흥 패러다임입니다. 이는 디버깅 및 리스크 평가를 위한 영역 수준의 정보를 제공하지만, 정확한 열거는 #P-hard 문제입니다.

3. 주요 기여

1. 통합 분류 체계: 본 논문은 패러다임, 시간적 범위, 보증 강도의 축을 따라 RL 검증 방법들을 조직하는 최초의 포괄적인 분류 체계를 제공하며, 표현력(expressivity)과 확장성(scalability) 사이의 트레이드오프를 명확히 합니다.
2. 정식화: 일관된 표기법을 사용하여 RL 검증 문제의 이론적 토대를 통합함으로써, 암묵적인 가정과 한계를 명시적으로 드러냅니다.
3. 비판적 분석: 기존 방법론의 한계, 특히 다단계 검증의 확장성 병목 현상과 단계별 도구를 순환형(recurrent) 또는 다중 에이전트 시스템에 적용할 때의 어려움을 분석합니다.
4. 도구 벤치마킹: RL 벤치마크(ACAS Xu, CartPole, LunarLander, Dubin's Rejoin)에서 검증 도구들(VNN-COMP 참가 도구 및 preimage 근사 방법 포함)을 경험적으로 비교하며, 경계 전파(bound-propagation) 방법이 단계별 작업에는 잘 확장되지만, 다단계 검증은 상태 공간 폭발로 인해 여전히 큰 병목 구간임을 강조합니다.

4. 결과 및 관찰

• 확장성 vs. 정밀도 (Scalability vs. Precision): 근본적인 트레이드오프가 존재합니다. 정확한 방법(SAT, 전수 열거)은 대규모 네트워크나 긴 호라이즌에 대해 실행 불가능한 경우가 많습니다. 과대 근사 및 확률적 방법은 더 나은 확장성을 제공하지만, 절대적 안전보다는 보수적이거나 확률적인 보증을 제공할 수 있습니다.
• 단계별 검증의 성숙도: 단계별 검증은 가장 성숙한 분야이며, $\alpha,\beta$-CROWN 및 NNV 2.0과 같은 도구들이 유망한 확장성을 보여줍니다. 그러나 이러한 방법들은 폐쇄 루프 실행이나 장기적 효과를 추론할 수 없습니다.
• 다단계 검방의 과제: 다단계 검증은 역학(dynamics) 모델링과 템포럴 명세(temporal specifications)를 다룰 때 "차원의 저주"에 의해 제한됩니다. 뉴로-심볼릭 접근 방식은 강력한 보증을 제공하지만, 일반성을 제한하는 추가적인 모델링 가정(예: 알려진 역학 또는 학습 가능한 인증서)에 의존합니다.
• 열거의 유용성: 열거 기반 접근 방식은 계산 비용이 많이 들지만, 상태 공간의 안전하지 않은 영역을 특징짓는 방식으로 정책 디버깅, 타겟 데이터 수집, 잔여 리스크의 심각성 정량화에 독특한 가치를 제공합니다.

5. 개방형 과제 및 향후 방향

본 논문은 고전적인 신경망 검증과 현대적인 RL 시스템 사이의 몇 가지 중요한 격차를 식별합니다:

• 순환 정책 (RNNs): 부분 관측 가능 환경에서 이력 의존적(history-dependent) 정책의 검증은 어려운 과제입니다. 왜냐하면 안전성이 실현 가능한 은닉 상태 궤적(feasible hidden-state trajectories)에 의존하기 때문입니다. 현재의 방법들은 실현 가능한 은닉 상태와 허구적인 은닉 상태를 구분하는 데 실패하는 경우가 많아, 지나치게 보수적인 보증을 제공하거나 허구적인 반례를 생성할 수 있습니다.
• 다중 에이전트 RL (MARL): MARL에서의 안전성은 상호작용으로부터 창발됩니다. 분산된 정책을 검증하려면 결합된 상태-행동 공간과 암묵적 협업을 추론해야 하며, 이는 지수적인 복잡성과 에이전트 단위 대 팀 단위 안전성에 관한 새로운 의미론적 과제를 도입합니다.
• 환경 불확실성: 대부분의 방법은 알려지거나 정확하게 근사된 역학을 가정합니다. 실제 시스템은 모델 불일치(model mismatch)와 비정상성(non-stationarity)에 직면하며, 이는 불확실성 하에서의 폐쇄 루프 시스템에 대해 어떻게 실행 가능한 보증을 제공할 것인가라는 문제를 제기합니다.
• 현대적 아키텍처: Transformer 및 어텐션 기반 모델을 검증하는 것은 어렵습니다. 어텐션 메커니즘은 조각별 선형(piecewise-linear) 가정을 위반하며, 이러한 모델은 가변 길이의 이력을 바탕으로 추론하기 때문에 시간적 추상화를 복잡하게 만듭니다.

6. 의의

본 논문은 RL 검증이 단순히 규모의 문제가 아니라 개념적인 문제라고 주장합니다. RL에서의 올바름은 정적인 입력-출력 강건성이 아니라 상호작용, 시간적 의존성, 그리고 분산된 결정의 관점에서 정의되어야 합니다. 제안된 분류 체계는 파편화된 문헌을 탐색하기 위한 통합된 관점을 제공하며, 실무자들이 자신의 특정 검증 목표(예: 국소적 강건성 vs. 장기적 안전성)와 RL 시스템의 구조적 제약에 따라 적절한 도구를 선택할 수 있도록 돕습니다. 저자들은 향-후의 발전이 RL 실행 의미론(execution semantics)과 더 잘 부합하면서도 건전성과 확장성 사이의 균형을 맞추는 프레임워크를 요구한다고 강조합니다.