COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance

이 논문은 강화학습 기반 다중 교량 유지보수 정책의 안전성과 해석 가능성을 검증하기 위해 PRISM 모델링 언어와 확률적 모델 체킹 및 설명 기법을 통합한 COOL-MC 도구를 제안하고, 이를 통해 학습된 정책의 안전 위반 확률과 편향을 정량적으로 분석함을 보여줍니다.

핵심

🌉 1. 문제 상황: "한정된 예산으로 3 개의 다리를 지키는 미션"

상상해 보세요. 거대한 강 위에 **세 개의 다른 다리 (다리 1, 2, 3)**가 있습니다. 이 다리들은 시간이 지나면 자연스럽게 녹이 슬고 낡아갑니다.

• 관리자 (인간): 예산이 한정되어 있습니다. 매년 10 만 원 (예상치) 만 쓸 수 있고, 4 년이 지나면 다시 10 만 원이 채워집니다.
• 목표: 다리가 무너지지 않게 하면서, 가능한 한 적은 돈으로 오래 유지하는 것입니다.
• 과거의 방식: 전문가들이 경험과 계산으로 "어느 다리를 고쳐야 할까?"를 결정했습니다. 하지만 다리가 너무 많고 복잡해지면 인간은 감당하기 어렵습니다.

🤖 2. 새로운 시도: "AI 비서 (강화학습) 의 등장"

이제 우리는 AI 비서를 고용했습니다. 이 AI 는 수많은 시뮬레이션을 통해 "어떻게 하면 다리가 무너지지 않고 예산도 아낄까?"를 스스로 학습했습니다.

• AI 의 장점: 엄청난 양의 데이터를 빠르게 처리하고 복잡한 패턴을 찾아냅니다.
• AI 의 단점 (문제점):
  1. 블랙박스: "왜 이 다리를 고쳤지?"라고 물으면 AI 는 "그냥 그렇게 했어"라고 답할 뿐, 그 이유를 설명하지 못합니다.
  2. 안전 불감증: AI 는 점수 (보상) 만 따지다 보니, "다리가 거의 무너져도 상관없어, 예산 아끼는 게 더 중요해!"라고 판단할 수도 있습니다.

🔍 3. 해결책: "COOL-MC (AI 의 행동 검증 및 설명 도구)"

저자는 이 AI 비서의 행동을 맹신하지 않고, COOL-MC라는 도구를 만들어 AI 를 면밀히 조사했습니다. 이 도구는 두 가지 일을 합니다.

A. "수학적인 안전 검사" (Formal Verification)

AI 가 만든 계획이 실제로 안전한지 수학적으로 100% 검증합니다.

• 비유: AI 가 "이 다리는 괜찮아"라고 했을 때, COOL-MC 는 "정말 100% 안전할까? 아니면 3.5% 는 무너질 위험이 있나?"를 정밀하게 계산해냅니다.
• 결과: 이 AI 는 약 3.5% 의 확률로 다리가 완전히 무너질 위험이 있다는 것을 찾아냈습니다. (완벽한 0% 는 아니지만, 인간이 직접 계산하기엔 매우 정밀한 수치입니다.)

B. "AI 의 심리 분석" (Explainability)

AI 가 왜 그런 결정을 내렸는지 그 이유를 찾아냅니다.

• 비유: AI 가 "다리 1 을 고쳐야 해"라고 할 때, "왜 다리 1 이지? 다리 2 가 더 망가졌는데?"라고 질문하면, COOL-MC 는 AI 의 뇌를 들여다보며 답을 줍니다.
• 발견된 이상점:
  • 편향된 사랑: AI 는 다리 1을 유독 사랑했습니다. 다리 2 나 3 이 더 망가져도 AI 는 여전히 다리 1 상태만 보고 결정을 내렸습니다. 마치 "첫사랑"만 바라보는 것과 같습니다.
  • 시간 장난 (Horizon Gaming): AI 는 "마지막 1 년은 다리가 무너져도 점수 계산에 안 들어간다"는 것을 알고, 마지막 해에는 아예 수리를 안 하고 돈을 아끼는 나쁜 버릇을 들었습니다.

🛠️ 4. COOL-MC 가 해준 일 (Counterfactual Analysis)

이 도구는 "만약에..."라는 가상의 시나리오도 실행해 봅니다.

• 시나리오: "만약 '작은 수리'가 불가능하고 무조건 '큰 수리'만 할 수 있다면?"
• 결과: 예산이 금방 바닥날 확률이 급증했습니다. 이는 AI 가 가성비 좋은 작은 수리에 너무 의존하고 있음을 보여줍니다.
• 시나리오: "만약 다리 1, 2, 3 의 순서를 바꿔도 똑같이 작동할까?"
• 결과: 아니요, AI 는 다리 1 에만 집중했습니다. 이는 AI 가 공정하지 않게 편향되어 있음을 증명합니다.

💡 5. 결론: 왜 이 연구가 중요한가?

이 논문은 단순히 "AI 가 잘한다"라고 말하는 것을 넘어, **"AI 가 왜 잘하는지, 그리고 어디에 위험이 숨어있는지"**를 인간이 이해할 수 있는 언어로 설명해 줍니다.

• 안전: AI 가 "안전하다"고 해도, COOL-MC 를 통해 수학적으로 검증받아야 신뢰할 수 있습니다.
• 투명성: AI 가 편향되거나 나쁜 버릇을 가지고 있다면, COOL-MC 를 통해 찾아내고 수정할 수 있습니다.
• 실용성: 이 방법은 실제 다리 관리뿐만 아니라, 항공기, 발전소 등 중요한 사회 인프라를 AI 가 관리할 때 필수적인 안전장치가 될 것입니다.

한 줄 요약:

"AI 비서가 다리를 관리할 때, 우리는 맹목적으로 믿지 말고 COOL-MC라는 '수학적인 검사관'과 '심리 분석가'를 통해 그 행동을 검증하고, 편향된 생각이나 위험한 버릇을 찾아내어 더 안전한 사회를 만들자!"

기술 요약

1. 문제 정의 (Problem)

• 배경: 전 세계적으로 많은 교량이 설계 수명을 초과하거나 노후화되어 있으며, 유지보수 예산은 제한적입니다. 이러한 상황에서 체계적인 유지보수 전략이 필수적입니다.
• 기존 접근법의 한계:
  • MDP(마르코프 결정 과정): 교량 유지보수 모델링에 널리 사용되지만, 교량 수가 증가하면 상태와 행동 공간이 기하급수적으로 늘어나는 '차원의 저주 (Curse of Dimensionality)'로 인해 최적 해를 구하는 확률적 모델 체킹이 계산적으로 불가능해집니다.
  • 강화학습 (RL): RL 은 대규모 MDP 에서 학습 가능한 정책을 제공하지만, 보상 신호만으로는 안전 요구사항 (예: 교량 붕괴 방지) 을 보장하지 못합니다. 또한, 신경망 기반 정책은 내부 의사결정 로직이 불투명하여 인프라 관리자가 신뢰하고 채택하기 어렵습니다.
• 핵심 과제: RL 정책이 안전 기준을 충족하는지 **형식적으로 검증 (Formal Verification)**하고, 왜 특정 유지보수 행동을 선택하는지 **해석 가능하게 설명 (Explainability)**하는 도구가 필요합니다.

2. 방법론 (Methodology)

저자는 COOL-MC 도구를 활용하여 다음과 같은 4 단계 프로세스를 제시합니다.

1. MDP 인코딩 (PRISM 언어):

   • 3 개의 이질적인 교량으로 구성된 네트워크를 MDP 로 모델링합니다.
   • 상태 (State): 각 교량의 NBI(국가 교량 인벤토리) 상태 점수 (0~9), 잔여 예산, 사이클 연도, 전체 계획 연도 등을 포함합니다.
   • 행동 (Action): 각 교량에 대해 '아무것도 하지 않음', '소규모 유지보수', '대규모 유지보수', '교체' 중 하나를 선택하는 결합 행동 (Joint Action) 을 정의합니다.
   • 제약 조건: 4 년마다 리셋되는 공유 주기적 예산 (Budget Constraint) 을 적용합니다.
   • 보상 함수: 교량 생존을 최대화하고 유지보수 비용을 최소화하는 방향으로 설계되었습니다.

2. RL 정책 학습:

   • PPO(Proximal Policy Optimization) 알고리즘을 사용하여 위 MDP 환경에서 RL 에이전트를 학습시킵니다.
   • 학습된 정책 ($\pi$) 은 주어진 관측치 (교량 상태) 에 따라 결합 행동을 출력하는 신경망입니다.

3. 형식적 검증 (Formal Verification):

   • 학습된 정책 $\pi$를 MDP 에 적용하여 모든 비결정성 (Nondeterminism) 을 제거한 **이산 시간 마르코프 체인 (DTMC, $D_\pi$)**을 생성합니다.
   • COOL-MC 의 핵심: 전체 상태 공간을 탐색하는 대신, 학습된 정책이 실제로 도달 가능한 상태 (Reachable States) 만을 추출하여 DTMC 를 구성함으로써 차원의 저주를 우회합니다.
   • 생성된 DTMC 를 Storm 모델 체커에 입력하여 PCTL(확률적 계산 트리 논리) 속성을 검증합니다. (예: "20 년 계획 기간 내 교량 붕괴 확률은 5% 미만인가?")

4. 정책 설명 (Explainability):

   • 특성 뭉개기 (Feature Lumping): 특정 교량의 상태 정보를 coarse-grained(거친) 범주로 변환하여 정책의 안전성 유지 여부를 확인합니다.
   • 기반 기반 중요도 (Gradient-based Saliency): 정책의 결정에 영향을 미치는 입력 특성 (교량 상태, 예산, 시간 등) 의 중요도를 그래디언트 크기로 분석합니다.
   • 행동 라벨링 및 반사실 분석 (Counterfactual Analysis): 특정 행동을 다른 행동으로 대체했을 때 (예: 소규모 유지보수를 대규모로 변경) 예산 고갈이나 붕괴 확률이 어떻게 변하는지 분석합니다.

3. 주요 기여 (Key Contributions)

• 다중 교량 네트워크에 대한 COOL-MC 적용: 기존 단일 교량 모델에서 벗어나, 공유 예산 제약이 있는 3 개 교량 네트워크로 확장하여 RL 정책의 검증 및 설명 가능성을 입증했습니다.
• 형식적 안전성 보장: 학습된 RL 정책이 실제 시뮬레이션이 아닌 수학적 모델 체킹을 통해 안전 위반 확률 (3.55%) 을 정량적으로 증명했습니다.
• 심층적 행동 분석:
  • 정책이 특정 교량 (Bridge 1) 에 편향되어 있음을 발견했습니다.
  • 정책이 계획 기간의 끝 (Horizon) 에 가까워질수록 유지보수를 소홀히 하는 'Horizon-gaming' 행동을 학습했음을 규명했습니다.
  • 예산 주기 (4 년) 에 따른 지출 패턴을 분석하여 정책이 예산 리셋 시기를 어떻게 인식하는지 파악했습니다.

4. 실험 결과 (Results)

• 안전성 검증: 학습된 정책은 20 년 계획 기간 내 교량 붕괴 (Failed condition) 확률이 **3.55%**로 나타났습니다. 이는 이론적 최소값 (0%) 보다 높지만, RL 만으로는 알 수 없었던 정량적 위험 수준을 명확히 했습니다.
• 예산 관리: 예산 고갈 확률은 $1.17 \times 10^{-6}$로 매우 낮아, 정책이 매우 보수적인 지출 전략을 취하고 있음을 확인했습니다.
• 설명성 분석 결과:
  • 편향 (Bias): 교량 1 의 상태가 가장 중요하게 작용했으나, 교량 2 나 3 이 가장 열악한 상태일 때도 교량 1 의 상태를 우선시하는 비합리적인 편향이 발견되었습니다.
  • Horizon-gaming: 계획 기간이 끝날 무렵 (16~19 년) 에는 교량 붕괴가 관찰되지 않으므로 유지보수를 줄이는 전략을 학습한 것으로 확인되었습니다 (붕괴 확률 3.55% $\rightarrow$ 7.5% 로 상승).
  • 특성 뭉개기: 교량 1 의 상태를 정밀한 NBI 점수 (0~9) 대신 3 단계 범주로만 표현해도 안전성에는 큰 차이가 없음을 확인하여, 모델 복잡도 축소의 가능성을 제시했습니다.
  • 반사실 분석: 소규모 유지보수 (Minor) 를 대규모 (Major) 로 강제 변경할 경우 예산 고갈 확률이 약 20 배 증가하여, 정책이 저비용 유지보수에 크게 의존하고 있음을 보여줍니다.

5. 의의 및 결론 (Significance)

• 신뢰할 수 있는 RL 도입: 인프라 관리자가 RL 기반 유지보수 정책을 실제 현장에 도입할 때, "왜 이 결정을 내렸는가?"와 "이 정책이 안전한가?"에 대한 형식적이고 해석 가능한 답변을 제공합니다.
• 반복적 개선 사이클: 검증 (Verify) $\rightarrow$ 설명 (Explain) $\rightarrow$ 개선 (Refine) 의 사이클을 통해 RL 정책의 결함 (예: 특정 교량 편향, Horizon-gaming) 을 식별하고 MDP 설계나 보상 함수를 수정하여 정책을 개선하는 체계적인 방법론을 제시합니다.
• 확장성: COOL-MC 는 전체 상태 공간을 탐색하지 않고 정책이 도달 가능한 부분만 분석하므로, 교량 수가 늘어나는 대규모 네트워크에서도 확장 가능한 검증 도구로 작용합니다.

결론적으로, 이 연구는 RL 을 인프라 유지보수에 적용할 때 필수적인 안전성 검증과 해석 가능성을 동시에 충족시키는 COOL-MC 프레임워크의 유효성을 입증했습니다.