기술 요약: 노이즈가 있는 양자 강화 학습 정책의 형식 검증

문제 정의

양자 강화 학습(QRL)은 중첩 및 얽힘과 같은 양자 현상을 활용하여 클래식 대응 모델보다 잠재적으로 더 뛰어난 순차적 의사결정 정책을 개발합니다. 그러나 클래식 강화 학습(RL)과 달리, QRL 정책은 변분 양자 회로(VQC)를 통해 구현되며 본질적으로 추가적인 불확ability(uncertainties)에 노출됩니다. 여기에는 양자 측정으로부터 발생하는 확률적 결과와 비트 플립(bit-flip), 위상 플립(phase-flip), 탈분극(depolarizing), 진폭 감쇠(amplitude damping)와 같은 하드웨어 결함(노이즈)이 포함됩니다.

이러한 불확실성은 행동 선택을 왜곡하여, 표준 보상 함수가 포착하지 못하는 안전하지 않은 에이전트 행동(예: 충돌)을 초래할 수 있습니다. 확률적 모델 체킹(probabilistic model checking)과 같은 형식 검증 방법이 클래식 RL 및 양자 통신 프로토콜에는 존재하지만, 훈련된 QRL 정책이 특정 양자 노이즈 조건 하에서 안전 요구 사항을 충족하는지 검증하는 체계적인 접근 방식은 부족한 실정입니다. 또한, 물리적인 양자 하드웨어에 대한 접근은 비용이 매우 많이 들기 때문에, 배포 전 검증은 안전이 중요한 애플리케이션에서 필수적입니다.

방법론: QVerifier

본 논문은 훈련된 QRL 정책을 양자 측정 불확실성과 모델링된 하드웨어 노이즈를 명시적으로 고려하여 안전 속성에 대해 엄격하게 분석하도록 설계된 형식 검증 방법인 QVerifier를 소개합니다. 이 접근 방식은 Storm 모델 체커를 통한 확률적 모델 체킹을 활용합니다.

방법론은 두 가지 주요 단계로 진행됩니다:

1. 유도된 이산 시간 마르코프 체인(DTMC) 구축:

   • 환경을 나타내는 마르코프 결정 과정(MDP)과 훈련된 메모리리스(memoryless) 확률 정책 $\pi$가 주어지면, QVerifier는 정책-환경 상호작 작용의 형식 모델을 점진적으로 구축합니다.
   • 이 방법은 정책 하에서 도달 가능한 모든 상태를 확장합니다. 각 상태 $s$에 대해, 0이 아닌 확률을 가진 모든 행동 $a$를 고려합니다.
   • 전이 확률 $P^\pi(s, s')$은 행동에 대해 주변화(marginalizing)하여 계산됩니다: $P^\pi(s, s') = \sum_{a} \pi(a|s) \cdot Tr(s, a, s')$.
   • 노이즈 통합: 노이즈 하에서의 검증 시, 정책 $\pi_\theta$는 노이즈가 있는 정책 $\pi^E_\theta$로 대체됩니다. 행동 확률은 유니터리 진화 $U_\theta$에 양자 노이즈 채널 $E$를 적용한 후의 최종 밀도 행렬 $\rho'$로부터 분석적으로 도출됩니다. 이를 통해 경험적 샘플링에 의존하지 않고 게이트 수준의 노이즈가 어떻게 전이 역학을 변화시키는지 캡처할 수 있습니다.
   • 구축 과정은 안전 속성에 관련된 모든 상태가 방문될 때까지 종료되어 불필요한 확장을 방지합니다.

2. 확률적 모델 체킹:

   • 생성된 DTMC는 Storm 모델 체커의 입력값으로 사용됩니다.
   • 안전 요구 사항은 도달 가능성($P_{\sim p}(F \phi)$) 및 "until" 속성($P_{\sim p}(\phi U \psi)$)을 지원하는 확률적 계산 트리 로직(PCTL)을 사용하여 정형화됩니다.
   • Storm은 속성이 충족되는지 검증하고, 충족 또는 위반의 정확한 확률을 계산합니다.

범위 및 한계: 이 방법은 이산 상태 및 행동 공간을 가진 메모리리스 확률 정책을 대상으로 합니다. 또한 노이즈 모델이 알려져 있다고 가정합니다. 만약 알려지지 않은 노이즈 특성을 가진 물리적 하드웨어에서 정책이 훈련되었다면, 검증은 가정된 노이즈 모델에 기반한 이상적인 근사치가 됩니다.

핵심 기여

1. QVerifier 프레임워크: 명시적인 양자 노이즈 모델(비트 플립, 위상 플립, 탈분극, 진폭 감쇠) 하에서 훈련된 QRL 정책을 검증하기 위해 확률적 모델 체킹을 적용한 첫 사례입니다.
2. 정확한 분석적 모델링: 샘플링에 의존하는 방법과 달리, QVerifier는 밀도 행렬로부터 직접 행동 확률을 계산하여 정확한 전이 확률과 연속적인 노이즈 파라미터 스윕(sweep)을 가능하게 합니다.
3. 비교 분석: 안전 속성에 관한 QRL과 클래식 RL의 성능 및 검증 오버헤드를 정확하게 비교하는 접근 방식을 제공합니다.
4. 배포 전 안전성: 고가의 양자 하드웨어에 정책을 배포하기 전에 안전 위반 및 유익한 노이즈 영역을 식별할 수 있는 방법을 제공합니다.

실험 결과

저자들은 세 가지 환경(Frozen Lake, Ski, Freeway)과 여섯 가지 정책(세 가지 QRL 및 세 가지 클래식 RL 베이스라인)을 사용하여 QVerifier를 평가했습니다.

• 성능 비교 (노이즈 없음): 이상적인 노이즈 없는 조건에서는 클래식 REINFORCE 정책이 도달 가능성 확률 측면에서 QRL 정책보다 일관되게 우수한 성능을 보였습니다. QRL 정책 또한 각 상태에서 양자 회로를 시뮬레이션하는 계산 오버헤드로 인해 검증 시간이 더 길게 나타났습니다.
• 양자 노이즈의 영향:
  • 성능 저하: 비트 플립 및 탈분극 노이즈는 모든 작업에서 일관되게 정책 성능을 저하시켰습니다. 특히 탈분극 노이즈는 양자 상태를 최대 무작위성으로 몰아넣음으로써 가장 심각한 성능 저하를 일으켰습니다.
  • 예상치 못한 개선: 특정 노이즈 모델이 성능을 향상시킬 수 있음이 밝혀졌습니다. Ski 환경에서 낮은 수준의 진폭 감쇠 노이즈는 QRL 정책의 목표 도달 확률을 클래식 RL 베이스라인 대비 27% 향상시켰습니다. 이러한 유익한 효과는 노이즈 수준이 높아짐에 따라 사라졌습니다.
  • 위상 플립: QRL Ski 정책에 대해 약간의 성능 향상을 보였습니다.
• 안전 위반: QRL 정책은 Frozen Lake 환경에서 클래식 정책보다 "until" 안전 속성(특정 경로를 통과하는 동안 위험 요소에 부딪히지 않음)을 더 자주 위반했습니다.

의의 및 주장

본 논문은 QVerifier가 안전이 중요한 양자 머신러닝의 배포 과정에서 발생하는 핵심적인 공백을 메우고 있다고 제안합니다. 클래식 하드웨어에서 배포 전 엄격한 검증을 가능하게 함으로써, 비용이 많이 들고 가용성이 제한적인 양자 하드웨어 테스트 문제를 완화합니다.

저자들은 QVerifier가 클래식과 양자 계산 사이의 "스윗 스팟(sweet spot)"을 타겟팅한다고 주장합니다. 즉, 검증을 위해 클래식하게 모델링할 수 있을 만큼 충분히 작으면서도, 실제로는 양자 하드웨어에서 실행되도록 의도된 훈련된 QRL 정책을 분석합니다. 결과는 노이즈가 보편적으로 해로운 것만은 아니며, 특정 노이즈 영역이 정규화제(regularizer) 역할을 하여 정책 성능을 향상시킬 수 있음을 보여줍니다. 결과적으로 QVerifier는 단순히 안전 위반을 탐지하는 도구일 뿐만 아니라, 특정 QRL 작업에 대한 최적의 하드웨어 노이즈 특성을 식별하여 하드웨어 선택 및 에러 예산 할당을 가이드하는 도구로서 기능합니다.