비정상 연속 제어를 위한 베이지안 망각 기반 구간별 강건 강화학습 (BAPR)

실제 세계의 제어 시스템은 역학(dynamics)이 장기간 안정적으로 유지되다가 갑작스러운 체제 변화(regime changes)를 겪는 '구간별 정적(piecewise stationary)' 조건에서 작동하는 경우가 많습니다. 표준적인 강건 강화학습 (Robust RL) 방법론은 근본적인 딜레마에 직면합니다. 즉, 전역적으로 보수적인 정책(globally conservative policy)은 안정적인 기간 동안 성능을 낭비하며, 국소적으로 적응적인 정책(locally adaptive policy)은 체제 변화를 감지하지 못했을 때 치명적인 실패의 위험을 초래합니다. 본 논문에서는 베이지안 온라인 변화 탐지 (Bayesian Online Change Detection, BOCD)와 강건 앙상블 강화학습 (Robust Ensemble RL)을 통합한 BAPR (Bayesian Amnesic Piecewise-Robust SAC)을 제안합니다. 고정된 신념 분포 (frozen belief distribution)에 의해 가중치가 부여된 모드 조건부 벨만 연산자 (mode-conditional Bellman operators)의 볼록 결합 (convex combination)인 BAPR 연산자는 $\gamma$-수축 ($\gamma$-contraction) 성질을 갖습니다. Lean4를 통해 기계 검증된 상호 보완적인 반례는 '날카로운 경계 (sharp boundary)'를 설정합니다. 즉, 신념이 Q-함수에 의존할 때 수축 계수는 $\gamma + \lambda\Delta$ (여기서 $\Delta$는 모드 보상 격차)가 되며, $\gamma + \lambda\Delta \geq 1$일 때 정확히 수축이 실패합니다. 우리는 추상 연산자에 대한 '성분별 (component-wise)' 형식적 오차 예산 (formal error budget)을 도출하였으며, 이는 모든 성분이 기계 검증되어 전환 후 회복을 제한합니다. 이 예산은 추상적 모드 혼합 연산자 (abstract mode-mixture operator)에 적용되며, 고정 파라미터 설계 직관을 통해서만 구현된 공유 비평가 (shared-critic) 알고리즘으로 상속됩니다. 모든 결과는 sorry 없이 형식적으로 검증되었습니다 (3개의 Lean4 파일에 걸친 1,145행, 22개의 기계 검증된 정리). BOCD는 적응형 보수성 메커니즘을 구동합니다. 정책은 변화 지점(change-points)이 감지된 후 최대한 보수적으로 변하며, 신뢰도가 높아짐에 따라 부드럽게 완화됩니다. 이때 탐지 지연은 $O(\log(1/\delta))$입니다. RMDM 손실을 통해 학습된 컨텍스트 조건화 모듈 (context-conditioning module)은 학습 시 시뮬레이터가 제공하는 모드 ID로부터 모드 인식 표현 (mode-aware representations)을 제공하며, 배포 시에는 모드 라벨이 필요하지 않습니다.