확률적 월드 모델로 비전 기반 신경 피드백 시스템을 검증한다

무엇인가

이 논문이 다루는 문제는 비전 기반 신경 피드백 시스템의 형식 검증이다. 카메라가 만든 고차원 관측을 신경망이 제어 명령으로 바꾸고 그 명령이 다시 상태를 움직이는 폐루프에서, 안전성을 증명하려면 먼저 센서와 장면을 대신할 모델이 필요하다. 상태 기반 시스템 검증은 성숙했지만 비전 기반은 대부분 미해결로 남아 있었고, 기존 연구는 카메라를 조건부 GAN으로 대체했다. 그러나 GAN은 파라미터가 크고 복잡한 장면의 구조를 잘 재현하지 못하며 검증기가 다루기 어렵다. 게다가 검증 결과의 의미는 서로게이트가 실제 카메라를 얼마나 충실히 대표하는지에 그대로 의존한다.

어떻게 동작하나

저자들의 형식화는 비전 기반 시스템을, 센서가 생성 모델인 상태 기반 시스템으로 다시 쓴다. 원래 센서 h(상태, 환경요인)를 생성 모델 g: R^n × Z → R^d로 바꾸고 환경요인 자리에 잠재변수 z를 넣는다. 이 틀에서 상태 기반 경우는 센서가 항등사상인 특수 케이스가 되므로, 상태 기반 검증 기법이 비전 기반으로 확장된다. 명세는 목표 집합에 언젠가 도달하고(도달) 어떤 스텝에서도 위험 집합과 교차하지 않는다(회피)는 reach-avoid 형태다.

무엇과 다른가

제안하는 월드 모델은 DCGAN 생성기와 DreamerV3 이미지 디코더 계열의 디컨볼루션 디코더다. 선형층이 상태를 거친 특징맵으로 올리고, L개의 전치합성곱 단계가 해상도를 두 배씩 키운다. 잠재변수는 FiLM(feature-wise linear modulation)으로 주입되며, 마지막 특징맵과 출력 비선형성 직전 이미지에 각각 한 번씩, 서로 다른 사영으로 적용된다. 두 사영은 0으로 초기화해 훈련이 상태만 쓰는 디코더에서 시작하고 잠재 변조가 그 위에 학습되게 한다. 이 구조는 선형, 합성곱, 배치정규화, ReLU, tanh만 쓰므로 표준 검증기가 바운드할 수 있고, FiLM의 곱만 두 유계량의 곱에 대한 표준 McCormick 완화로 처리한다. 잠재변수는 각각 물리량 구간을 가지므로 Z는 물리적 조건의 박스가 되고, 어떤 상태에서 관측 가능한 이미지 집합은 그 조건들 아래 찍힌 이미지 집합이 된다. 훈련은 제어기가 참 상태에 작용하는 폐루프 롤아웃에서 수집한 시뮬레이션 카메라 이미지에 대한 지도 회귀로 이루어지며, 잠재변수는 롤아웃 내에서는 고정하고 롤아웃 간에는 바꿔 Z를 덮는다. 손실은 픽셀 단위 L1과 SSIM 항을 같은 가중치로 더한 것이고, 단일 H100에서 1분 이내에 학습된다.

어떻게 쓰나

검증 절차는 초기 집합을 균일한 셀로 나누고 각 셀을 반증, 전방 분석, 적응적 세분화, 기호 분석, 후방 분석으로 해결한다. 반증이 가장 저렴한 단계로, 초기 상태와 잠재변수를 조밀하게 샘플링해 서로게이트·제어기·동역학을 시뮬레이션하고 위험 집합에 들어간 궤적을 고정밀 산술로 재확인한다. 반증된 셀은 안전한 상태를 포함할 수 있지만 셀 전체를 위험으로 표시해 검증 영역이 안전집합의 건전한 하위근사가 되게 한다. 전방 분석은 각 셀에서 도달 가능한 상태의 스텝별 바운드를 계산하는데, 이를 위해 서로게이트가 낼 수 있는 관측, 그 관측에 대한 제어기 행동, 그 행동 아래 벡터장이 도달하는 상태를 모두 바운드한다. 과대근사가 명세를 만족하면 셀이 검증되고, 아니면 미해결로 남는다. 여기에 ReLU 완화 기울기 같은 추상화의 자유 파라미터를 조정하는 추상화 최적화를 적용하고, 입력 분할·뉴런 분할·인클로저 세분화를 결합한 적응적 세분화로 도메인을 줄인다. 세분화는 정해진 깊이까지 수행하고 남은 부분문제는 기호 분석으로 넘긴다. 기호 분석은 폐루프를 여러 스텝 펼쳐 궤적을 한 번에 바운드해 스텝마다 쌓이는 근사 오차를 줄이지만 비싸므로 이전 분석이 못 푼 셀에만 쓴다. 후방 분석은 위험 집합에 도달하는 상태 집합을 과대근사하는데, 전방 바운드를 중간 스텝까지 가져간 뒤 그 스텝의 전방 집합이 남은 지평선 안에 위험 집합에 닿을 수 없음을 후방 계산으로 보여주는 방식으로 전방 분석만으로는 못 푸는 셀을 해결한다.

전제와 한계

모델링 품질 실험에서 월드 모델은 두 사례 연구 모두에서 GAN 서로게이트보다 보류된 프레임을 충실히 재현했다. 항공기 지상 활주에서는 50k 파라미터의 가장 작은 월드 모델조차 2.76M 파라미터 DCGAN과 그로부터 증류한 232k 파라미터 MLP GAN보다 장면을 잘 그렸고, 모델이 커질수록 충실도가 올랐다. 비상제동(AEBS)에서는 14배에서 130배 많은 파라미터를 가진 GAN보다 높은 충실도를 기록했고, 격차는 장면 구조 보존을 재는 SSIM에서 가장 컸다(월드 모델 0.713과 0.823 대 GAN 0.449와 0.489). GAN은 장면의 평균 밝기는 맞추지만 구조를 잃는다.

검증 결과에서 그레이스케일 AEBS 벤치마크는 상태 공간 전체가 해결됐다. 저자들은 3,464개 셀을 반증했는데 이는 비교 대상 방법보다 하나 많은 수치다. 검증한 6,536개 셀 중 전방 분석이 2,208개, 추상화 최적화와 적응적 세분화가 551개, 기호 분석이 3개, 후방 분석이 3,774개를 처리했고 여기에는 비교 방법이 검증한 2,669개가 모두 포함된다. 벤치마크 검증 비용은 1,043 GPU-hours였고 그중 약 1,030이 비교 방법이 해결하지 못한 셀에 쓰였다. 비교 방법이 검증한 2,669개 셀은 10 GPU-hours 미만이 걸렸다. 비교 논문은 벤치마크 전체에 374 GPU-hours를 보고했지만 하드웨어는 명시하지 않았다. RGB 버전에서는 이전에 검증 결과가 보고된 바 없는데, 월드 모델 서로게이트로 550 GPU-hours에 상태 공간의 80% 이상을 해결했다. 미해결 1,825개 중 1,822개는 아직 분석하지 않은 셀이다. 그레이스케일에서 80%를 160 GPU-hours에 해결하고 나머지 20%에 880을 쓴 패턴을 따르면 RGB 전체 검증에 약 3,600 GPU-hours가 걸릴 것으로 추정한다. 한편 어텐션 기반 지각 헤드 검증은 여전히 어렵다. RGB 결과는 릴리스된 어텐션 헤드 대신 합성곱 헤드를 쓴 것인데, 10 GPU-hours 안에 합성곱 헤드는 비슷한 크기 어텐션 헤드의 두 배가 넘는 120개 셀을 검증한 반면(어텐션 55개), 릴리스 크기인 1.73M 파라미터 어텐션 헤드는 같은 예산에서 10개 셀만 검증됐다. 다만 그 큰 헤드는 보류 프레임에서 거리를 두 배 이상 정확히 읽는다.

저자들이 밝힌 한계는 분명하다. 보장은 서로게이트 시스템에 대한 것이고, 그 보장을 실제 시스템으로 옮길 수 있는지는 서로게이트의 충실도에 달려 있다. 월드 모델은 시뮬레이션 프레임으로만 훈련·평가됐고, 서로게이트와 그것이 대체하는 카메라 사이의 관계를 정하는 형식적 보장은 없다. RGB 결과는 합성곱 지각 헤드에 대한 것이며 릴리스된 어텐션 헤드로는 벤치마크를 검증하지 못했다. 또한 기호 분석의 기여가 미미한데(그레이스케일 3개 셀, RGB는 아직 0개) 그 이유를 아직 규명하지 못했다. 향후 계획으로는 어텐션에 대한 더 타이트한 추상화, 실제 카메라 데이터로 훈련한 월드 모델, 기호 분석의 효용 규명, 더 비선형적인 벤치마크와 더 풍부한 명세 연구가 제시된다.

실무 관점에서 이 논문이 주는 신호는 두 가지다. 첫째, 비전 제어기의 안전 검증에서 병목은 검증 알고리즘이 아니라 지각 서로게이트의 설계이며, 잠재변수를 물리량에 묶고 검증기가 바운드할 수 있는 연산만으로 모델을 구성하면 충실도와 검증 가능성을 동시에 얻을 수 있다. 둘째, 검증 파이프라인을 도입할 때는 보장 범위가 서로게이트에 국한된다는 전제, 셀 단위로 위험을 표시해 안전 영역을 하위근사한다는 점, GPU 비용이 미해결 셀에 집중된다는 점, 그리고 어텐션 헤드가 아직 실용적 비용으로 검증되지 않는다는 점을 먼저 확인해야 한다.