기술 요약: 강화 학습의 생동성 보존형 차폐를 위한 적응형 GR(1) 명세 수리 (Adaptive GR(1)-Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning)

문제 정의

안전이 중요한 도메인에서의 강화 학습(RL) 에이전트는 자신의 행동이 논리적 명세를 준수한다는 공식적인 보증을 필요로 한다. **차폐(Shielding)**는 대표적인 기술로, 런타임 컨트롤러(차폐기)가 에이전트가 제안한 행동을 모니터링하고, 공식 명세를 위반할 가능성이 있는 행동만을 억제하는 방식이다. 그러나 기존의 차폐 접근 방식은 정적인 환경 추상화와 고정된 논리 명세에 의존한다.

본 연구가 다루는 핵심 문제는 이러한 정적 차폐기가 환경에 대한 가정이 항상 옳다고 가정한다는 점이다. 배포된 환경이 이러한 가정을 위반할 경우(오설계 또는 예상치 못한 변화로 인해), 차폐기는 지나치게 보수적으로 변하여 유용한 행동을 차단하거나, 생동성(liveness)(결국 목표에 도달할 수 있는 능력)을 유지하지 못할 수 있다. 또한, 가정이 암시적일 경우, 왜 명세가 실현 불가능해졌는지 또는 왜 차폐기가 작업 완료를 방해하는지 진단하기 어렵다. 적응을 시도하는 기존 방법들은 주로 고정된 구조 내에서 전이 확률을 학습하거나, 보증을 제공하기 위해 충분한 모델 수렴이 필요하다는 점에 초점을 맞추고 있으며, 논리적 구조 자체를 동적으로 수리하는 데에는 미치지 못한다.

방법론: RepairRL 프레임워크

저자들은 반응형 합성(reactive synthesis)과 강화 학습을 결합한 하이브리드 프레임워크인 RepairRL을 제안한다. 이 시스템은 네 가지 주요 구성 요소와 함께 폐쇄 루프(closed loop)로 작동한다:

1. RL 에이전트: 마르코프 결정 과정(MDP) 내에서 보상을 최대화하도록 훈련된 에이전트.
2. 반응형 차폐기 (Reactive Shield): GR(1) (Generalized Reactivity of rank 1) 명세로부터 합성된다. GR(1)은 가정-보증(assume-guarantee) 구조($\Phi = \langle A, G \rangle$)를 사용하는 선형 시간 논리(LTL)의 다루기 쉬운 파편으로, 여기서 $A$는 환경 가정을, $G$는 시스템 보증을 나타낸다. 차폐기는 에이전트의 행동을 안전한 상태의 "승리 영역(winning region)"으로 제한함으로써 안전성을 강제하고 생동성을 보존한다.
3. 환경 검사기 (Environment Checker): 시스템 궤적(trace)을 관찰하는 런타임 모니터이다. 시스템 궤적이 환경 가정($A$)을 위반하는 전이를 감지하면 환경 실패를 알린다.
4. SpecRepair 모듈: 위반이 감지되면, 이 모듈은 **귀납 논리 프로그래밍(ILP)**을 사용하여 온라인으로 GR(1) 명세를 자동으로 수리한다.

수리 과정

수리 절차는 카운터예제 유도 학습(counterexample-guided inductive learning) 방식(즉, "학습자-오라클" 프레임워크)을 따른다:

• 학습자 (Learner): ILP 학습기(구체적으로 ILP/ILASP)가 위반된 궤적 $\tau$를 분석한다.
• 오라클 (Oracle): GR(1) 합성기(구체적으로 Spectra)가 실현 가능성(realizability)을 확인한다.
• 알고리즘:
  1. 학습자는 관찰된 위반 궤적과 일치하도록 가정($A$)을 약화시키려고 시도한다.
  2. 오라클은 새로운 명세 $\langle A', G \rangle$가 실현 가능한지 확인한다.
  3. 실현 가능하다면, 새로운 컨트롤러를 합성한다.
  4. 실현 불가능하다면, 오라클은 반례 전략(counter-strategy)을 제공하고, 학습자는 실현 가능성을 복구하기 위해 보증($G$)을 최소한으로 약화시킨다.
• 재합성 (Re-synthesis): 수리된 명세 $\Phi' = \langle A', G' \rangle$는 업데이트된 차폐기를 합성하는 데 사용되며, 이를 통해 에이전트가 교정된 환경 이해 하에서 계속 운영될 수 있도록 한다.

이 프레임워크는 새로운 명세가 **건전(sound)**함을 보장한다. 즉, 위반된 궤적이 새로운 가정과 일치하게 되고, 명세가 실현 가능성을 유지하며, 새로운 가정/보증이 기존의 것보다 논리적으로 약하거나 동일하여 시스템이 필요 이상으로 제한되지 않도록 한다.

주요 기여

1. 적응형 차폐 프레임워크: ILP 기반의 명세 수리 절차를 폐쇄 루프 온라인 차폐-RL 시스템 내에 삽입하였다. 고정된 그래프 상의 확률을 추정하는 방법과 달리, 이 방법은 환경 추상의 논리적 구조 자체를 변경한다.
2. 생동성 보존: 이 접근 방식은 안전성과 생동성 사이의 트레이드오프를 명시적으로 관리한다. 명세를 수리함으로써, 시스템은 환경 가정이 위반되더라도 생동성 목표가 달성 가능한 상태로 유지되도록 하며, 단순히 모든 행동을 차단하지 않는다.
3. 해석 가능성: 수리 과정은 어떤 가정이 또는 보증이 왜 약화되었는지에 대한 인간이 읽을 수 있는 설명을 생성한다. 이는 일부 적응형 안전 메커니즘의 "블랙박스" 특성을 해결한다.
4. 공식적 보증: 저자들은 수리 절차가 실현 가능성을 유지하고 수리 후에도 에이전트가 데드락(deadlock)으로부터 자유로움을 입증하는 공식적 증명(정리 3 및 코롤러리 4)을 제공한다.

실험 결과

프레임워크는 Minepump(확률적 MDP 벤치마크)와 Atari Seaquest(산소 제약이 있는 고차원 시각적 작업)의 두 도메인에서 평가되었다. 두 경우 모두, 에이전트는 명목 명세 하에서 훈련되었으며, 환경 가정을 위반하는 섭동된 역학(perturbed dynamics) 하에서 평가되었다.

• Minepump:

  • 정적 컨트롤러: 명목 명세로부터 합성된 컨트롤러는 환경 가정이 위반되었을 때 배포 시 완전히 실패(성공률 0%)했다. 수리된 명세(Static Ctrl. 2)로 합성된 컨트롤러는 100% 성공률을 유지했으나, 적응형 접근 방식에 비해 현저히 낮은 보상(-1018.29)을 기록하여 고정된 심볼릭 정책의 비용을 보여주었다.
  • Safe RL 베이스라인: CPO 및 PPO-Lagrangian과 같은 방법들은 훈련 중에는 제약 조건을 만족했으나, 환경 가정이 위반되었을 때 일반화에 실패했다(성공률 0.01).
  • 적응형 차폐 (본 연구): 훈련 및 배포 모두에서 100% 성공을 달하며, 동시에 높은 보상(-764.98)을 유지했다. 이는 메탄의 부재 여부에 따라 펌핑 요구 사항을 조건화함으로써 명세를 성공적으로 수리했음을 보여준다.

• Atari Seaquest:

  • 섭동: 산소가 일정한 속도로 감소한다는 가정을 위반하여, 특정 임계값 이후에는 산소가 두 배 빠르게 감소하는 환경에서 평가되었다.
  • 결과: unshielded PPO는 대부분의 에피소드에서 실패했다. 정적 차폐기(Standard 및 Static)는 잘못된 모델로부터 승리 영역을 계산했기 때문에 평가에서 실패했다.
  • 적응형 차폐: 낮은 오버라이드 비율(0.06)과 함께 100% 평가 성공률을 유지했다. 역학이 어려워짐에 따라 보상은 감소했지만, 적응형 차폐는 수정된 모델을 사전에 알 필요 없이 논리적 준수를 유지했다.
  • 비교: CPO 및 PPO-Lag는 완벽한 안전성을 달 확보했으나, 차폐된 PPO 에이전트들에 비해 상당히 낮은 보상을 가진 매우 보수적인 정책을 학습했다.

의의 및 주장

본 논문은 적응형 GR(1) 명세 수리가 런타임에 환경 가정이 위반될 때, 딥 RL 에이전트가 안전하면서도 효과적으로 유지될 수 있게 하는 실용적인 접근 방식임을 주장한다.

• 최소한의 간섭: 이 방법은 차폐기가 점진적으로 진화하도록 하여 생동성을 달성 가능한 상태로 유지하고, 엄격히 필요한 경우에만 목표를 약화시킨다.
• 투명성: ILP를 통해 가정을 명시하고 이를 수정함으로써, 접근 방식의 해석 가능성과 신뢰도를 높인다. 실현 가능성을 뒷받침하는 가정은 더 이상 합성된 컨트롤러 안에 숨겨져 있지 않고, 노출되어 필요할 때 가시적으로 약화된다.
• 한계: 저자들은 두 가지 한계를 언급했다:
  1. GR(1)에 대한 의존성은 유한하고 이산적인 상태 추상을 요구하며, 이는 풍부한 연속 역학을 가진 도메인에서 어려울 수 있다(Signal Temporal Logic에 대한 향후 연구 동기).
  2. 반복적인 학습자-오라클 루프(ILASP + Spectra)는 규모가 큰 명세나 빈번한 수리 시 계산 병목 현상이 될 수 있어, 확장을 위한 더 빠른 수리 알고리즘이 필요하다.

본 연구는 정적 심볼릭 컨트롤러가 보조적 보상 최적화에 있어 종종 최적이 아님을 보여주며, 적응형 차폐를 갖춘 RL 에이전트가 환경 역학이 변하더라도 정적 차폐기에 비해 높은 보상과 완벽한 논리적 준수를 유지할 수 있음을 입증한다.