기술 요약: 동적 시스템의 안전성 검증을 위한 신경 장벽 증명자의 집합 기반 훈련

1. 문제 제기

연속 시간 동적 시스템의 안전성 검증은 자율 주행 차량, 무인 항공기 (UAV), 로봇 매니퓰레이터와 같은 안전-중요 환경에서 자율 에이전트에게 필수적입니다. 초기 집합 $X_I$에서 시작하는 어떤 궤적도 비안전 집합 $X_U$에 진입하지 않는다면, 해당 시스템은 안전하다고 간주됩니다.

기존 검증 방법들은 다음과 같은 중대한 한계에 직면해 있습니다:

• 시뮬레이션 기반 방법은 시스템 차원에 비례하여 지수적으로 증가하는 실행 시간의 고통을 겪습니다.
• ** Reachability 분석 (Reachability analysis)** 은 지수적인 실행 시간을 피하기 위해 집합 기반 계산을 사용하지만, 계산 집약적일 수 있습니다.
• 장벽 증명자 (Barrier Certificates) 는 영수준 집합 (zero-level set) 을 통해 $X_I$와 $X_U$를 분리하는 스칼라 함수 $B$를 정의함으로써 안전성에 대한 형식적 증명을 제공합니다. 그러나 신경망 기반 장벽 증명자를 합성하는 최근 접근법들은 반복적인 훈련 - 검증 사이클에 의존합니다. 이 사이클에서 신경망은 상태 공간 샘플로 훈련된 후 외부 솔버 (예: SMT) 를 사용하여 형식적으로 검증됩니다. 검증이 실패하면 (반례가 발견되면) 네트워크가 재훈련됩니다. 이 과정은 비용이 많이 들며, 많은 사이클을 필요로 할 수 있고, 단일 절차 내에서 유효한 증명자로 수렴할 것을 보장하지 않습니다.

2. 방법론: 집합 기반 훈련

저자들은 별도의 검증 단계의 필요성을 제거하고 형식적 검증을 신경망 훈련 과정에 직접 통합하는 새로운 집합 기반 훈련 접근법을 제안합니다.

핵심 개념

이산 샘플로 훈련한 후 나중에 검증하는 대신, 이 방법은 정확한 집합 기반 손실 함수 (sound set-based loss function) 를 사용하여 신경망 $B_\theta$를 훈련합니다. 이 손실 함수는 개별 점 대신 상태 공간의 전체 집합 (enclosures) 에 대해 계산됩니다. 손실이 0 에 도달하면 장벽 증명자의 유효성이 구성에 의해 형식적으로 증명됩니다.

주요 기술 구성 요소

A. 정확한 집합 기반 손실 함수
손실 함수는 장벽 증명자에 필요한 세 가지 속성 (정리 1) 을 인코딩합니다:

1. 속성 P I (비안전 상태): $X_U$의 모든 상태는 양수 값으로 매핑되어야 합니다. 손실 $L_I$는 $X_U$의 집합 기반 이미지의 하한을 패널티합니다.
2. 속성 P II (초기 상태): $X_I$의 모든 상태는 음이 아닌 값으로 매핑되어야 합니다. 손실 $L_{II}$는 $X_I$의 집합 기반 이미지의 상한을 패널티합니다.
3. 속성 P III (영수준 집합 동역학): 리 미분 (Lie derivative) $L_f B_\theta$는 영수준 집합 $X_Z = \{x \mid B_\theta(x) = 0\}$에서 음수여야 합니다.
   • $X_Z$는 알려지지 않았고 비볼록하므로, 이 방법은 재귀적 분기 - 경계 전략 (입력 공간을 분할하고 영점이 없는 영역을 제거) 을 통해 zonotope 의 합집합을 사용하여 $X_Z$의 정밀한 enclosure를 계산합니다.
   • enclosure 의 각 zonotope 에 대해, 리 미분은 기울기 집합과 흐름 집합의 집합 기반 순방향 전파를 통해 enclosure 됩니다.
   • 손실 $L_{III}$는 이러한 리 미분 enclosure 들의 상한을 패널티합니다.

총 손실은 $L = L_I + L_{II} + L_{III}$입니다. $L=0$이면 시스템은 형식적으로 안전하다고 검증됩니다.

B. 집합 기반 순방향 전파
이러한 손실을 계산하기 위해 이 방법은 신경망 계층을 통해 zonotope(특정 유형의 볼록 다면체) 를 전파합니다:

• 선형 계층: 아핀 맵을 통해 정확하게 계산됩니다.
• 비선형 계층: 보수적인 오버-근사 (예: 범위 바운딩) 를 사용하여 enclosure 됩니다.
• 기울기와 리 미분: 기울기 집합이 역방향으로 전파되고, 리 미분은 기울기 집합과 흐름 집합의 내적으로 계산됩니다.

C. 알고리즘
훈련 루프 (알고리즘 1) 는 네트워크를 초기화하고, $P_I$, $P_{II}$, $P_{III}$에 대한 집합 기반 손실을 계산하며, 경사 하강법을 통해 매개변수를 업데이트한 후 총 손실이 0 이 되면 종료됩니다.

3. 주요 기여

1. 단일 절차 합성: 반복적인 훈련 - 검증 사이클을 제거하고 단일 집합 기반 훈련 절차에서 신경 장벽 증명자를 합성하는 새로운 접근법.
2. 정확한 손실 함수: 모든 장벽 증명자 속성을 정확하게 인코딩하는 집합 기반 손실. 영손실 값은 안전성에 대한 형식적 증명을 구성합니다.
3. 반복적 정제: 속성 P III 에 필요한 영수준 집합과 리 미분을 동적으로 enclosure 하는 반복 절차.
4. 광범위한 평가: 선형, 다항식, 비다항식 동역학을 포함하는 13 개의 벤치마크 (최대 9 차원 시스템 및 복잡한 집합 구성 포함) 에 대한 평가.

4. 실험 결과

이 접근법은 CORA 툴박스를 사용하여 구현되었으며, 최신 도구들과 비교되었습니다: SynNBC 및 FOSSIL(반복적 훈련 - 검증) 과 PRoTECT(합의 제곱 최적화).

• 성공률: 제안된 방법은 13 개 모든 벤치마크에서 100% 성공률을 달성했습니다.
  • 반면, SynNBC 와 PRoTECT 는 비다항식 동역학과 여러 초기/비안전 집합을 가진 벤치마크에서 실패했습니다.
  • FOSSIL 은 높은 성공률을 보였지만 고차원 시스템에서 성능이 저하되었습니다 (예: Peruffo 6D 에서 70%, Peruffo 8D 에서 80%).
• 실행 시간: 집합 기반 훈련 접근법은 FOSSIL 보다 훨씬 빨랐습니다. 예를 들어, Peruffo (8D) 벤치마크에서 제안된 방법은 평균 1.0 초가 소요된 반면, FOSSIL 은 47.7 초가 소요되었습니다.
• 훈련 효율성: 이 방법은 일반적으로 몇 개의 훈련 에포크 내에 수렴했습니다. 반면, FOSSIL 은 종종 여러 훈련 - 검증 사이클을 필요로 했는데, 각 사이클은 최대 1,000 개의 에포크를 포함할 수 있었습니다.
• 절대화 연구 (Ablation Studies):
  • 네트워크 아키텍처: 얕은 네트워크 (단일 선형 계층) 는 선형 시스템에는 충분했지만 비다항식 시스템에서는 실패했습니다. 복잡한 동역학에는 더 깊은 네트워크가 필요했습니다.
  • 영수준 집합 Enclosure: 더 복잡한 동역학은 속성 P III 를 만족시키기 위해 더 정교한 영수준 집합 enclosure(더 많은 분할/반복) 를 필요로 했습니다.

5. 중요성과 주장

이 논문은 훈련 및 검증 단계를 축소함으로써 안전성 검증의 패러다임 전환을 나타낸다고 주장합니다.

• 형식적 보장: 형식적 안전 보장을 제공하지 않는 표준 신경망 훈련과 달리, 이 방법은 영손실이 유효한 장벽 증명자를 의미하도록 보장합니다.
• 확장성: 연산은 효율적인 행렬 곱셈으로 축소되어 시스템 차원에 따라 잘 확장되는 다항식 복잡성을 제공합니다.
• 다용도성: 이 접근법은 시스템 동역학에 크게 무관하며, 구간 기반 방법들이 어려움을 겪는 복잡한 비선형 (비다항식) 동역학과 복잡한 집합 표현 (예: 집합의 합집합, 비볼록 영역) 을 자연스럽게 처리합니다.
• 효율성: 비용이 많이 드는 반복 사이클을 제거함으로써, 이 방법은 고차원 및 비선형 시스템에 대한 형식적 검증으로 가는 더 효율적인 경로를 제공합니다.

저자들은 그들의 집합 기반 합성이 후속 검증을 필요로 하지 않고 장벽 증명자를 효율적으로 생성할 수 있으며, 특히 고차원 및 비다항식 시스템에서 기존 작업들을 능가한다고 결론지었습니다.