기술적 요약: 신경망 검증기 $\alpha,\beta$-CROWN 을 통한 제어와의 연결

문제 제기

학습 기반 신경망 (NN) 제어기는 자율 주행, 로봇 공학, 전력 시스템과 같은 안전-중요 분야에서 높은 표현력과 강력한 경험적 성능을 입증해 왔습니다. 그러나 이러한 설정에서의 배포를 위해서는 경험적 성능만으로는 부족합니다. 안정성 (예: 라야푸노프 안정성), 안전성 (예: 배리어 함수), 도달 가능성과 같은 폐루프 특성에 대한 형식적 검증이 시급히 필요합니다.

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

1. 확장성: SMT 솔버 (예: dReal, Z3), 혼합 정수 선형 계획법 (MILP), 볼록 최적화 (SDP, SOS) 와 같은 전통적인 방법들은 GPU 가속 및 병렬화를 활용할 수 있는 능력이 제한적이어서, 고차원 시스템이나 심층 신경망의 경우 확장성이 매우 낮습니다.
2. 구조적 경직성: 많은 방법들은 ReLU 활성화 함수를 가진 얕은 조각별 선형 네트워크나 다항식 시스템과 같은 특정 구조적 가정에 묶여 있어, 다른 제어 설정이나 증명서 (certificate) 클래스 간에 전이가 어렵습니다.
3. 증명서 특이성: 최근 제어 지향 검증 방법들은 종종 증명서 특이적 구조 (예: 심볼릭 경계 전파) 를 활용하는데, 이는 다양한 클래스의 증명서에 대한 직접적인 적용성을 제한합니다.

방법론

본 논문은 제어 이론과 최첨단 신경망 검증기 $\alpha,\beta$-CROWN을 연결하는 통합 프레임워크를 소개합니다. 핵심 방법론은 제어 문제를 계산 그래프 상의 검증 또는 최적화 작업으로 취급하는 데 기반합니다.

1. $\alpha,\beta$-CROWN 검증기

$\alpha,\beta$-CROWN 은 계산 그래프로 표현된 비선형 함수를 위한 범용 경계 추정 엔진입니다. 그 작동 방식은 다음과 같습니다:

• 계산 그래프: 이 프레임워크는 시스템 동역학 $f$, 제어기 $\pi$, 그리고 증명서 (예: 라야푸노프 함수 $V$) 를 아핀 맵, ReLU, sin, 곱셈과 같은 기본 연산으로 구성된 방향성 비순환 그래프 (DAG) 로 모델링합니다.
• 자동 선형 완화 (auto LiRPA): 검증기는 계산 그래프를 통해 역방향으로 타당한 선형 상계 (bounds) 를 전파합니다. 임의의 입력 영역 $B$에 대해, 이 과정은 아핀 하계 $F(x) \geq a^\top x + b$를 계산합니다. 이 과정은 완전히 미분 가능하며 매우 벡터화되어 있어 GPU 에서 효율적으로 실행될 수 있습니다.
• 분할 - 바운드 (Branch-and-Bound, BaB): 선형 경계가 결론을 내리지 못하는 경우를 처리하기 위해, 이 프레임워크는 입력 영역 분할 - 바운드를 사용합니다. 입력 영역을 부분 영역으로 재귀적으로 분할합니다. 영역이 축소됨에 따라 국소 선형 완화는 더 엄격해지고, 상계 추정 오차는 감소합니다.
• 야코비안 처리: 연속 시간 시스템에서 기울기 경계 (예: $\nabla V \cdot f$) 가 필요한 경우, 이 프레임워크는 연쇄 법칙을 통해 기울기 계산을 명시적으로 인코딩하도록 계산 그래프를 확장하여 야코비안 계산을 또 다른 연산자로 취급합니다.

2. 제어 문제의 재구성

이 튜토리얼은 고전적 제어 이론적 문제들을 상자 (box) 영역에 대한 $\alpha,\beta$-CROWN 친화적 만족도 또는 최적화 문제로 어떻게 재구성하는지 보여줍니다:

• 도달 가능성 분석: 입력 상자 상에서 폐루프 맵 $g(x)$의 출력을 경계 짓는 것을 통해 도달 가능 집합의 타당한 상계 추정을 계산합니다.
• 안정성 검증 (라야푸노프): 라야푸노프 함수가 궤적을 따라 감소한다는 요구사항을 만족도 문제로 변환합니다. 이산 시간 시스템의 경우, 주변 상자에 대한 논리적 함의로 재구성된 부분 레벨 집합에서 $(V(g(x)) - (1-\kappa)V(x) \leq 0)$와 같은 조건을 검증합니다. 연속 시간 시스템의 경우 상자 경계에서의 forward 불변성을 처리하는 것과 유사한 재구성이 제공됩니다.
• 안전성 검증 (배리어 함수): 배리어 함수의 도함수에 대한 조건을 확인함으로써 안전한 집합이 forward 불변인지 검증합니다. 제어-아핀 시스템의 경우, 제어 입력에 대한 상한은 다면체 꼭짓점에서의 최대로 변환됩니다.
• 수축 분석: 행렬 기반 수축 조건을 리만 계량을 포함하는 스칼라 만족도 문제로 재구성합니다.
• 최적화 (MPC): 검증기를 모델 예측 제어 (MPC) 를 위한 전역 최적화기로 사용하여, 비선형 동역학과 제약 조건에 따른 비용 함수를 최소화하고, 인증된 하계에 의해 안내합니다.

3. 학습 및 합성

본 논문은 제어기와 증명서를 공동 합성하는 프레임워크에 대해 논의합니다:

• 반례 유도 귀납 합성 (CEGIS): 검증 중 발견된 반례를 학습 데이터로 사용하는 반복적 접근법입니다.
• 인증된 학습: $\alpha,\beta$-CROWN 이 생성한 미분 가능한 하계를 직접 학습 손실 함수에 통합하는 패러다임입니다. 이는 사양의 인증된 하계를 최대화하기 위한 기울기 기반 최적화를 가능하게 하여, 본질적으로 "검증 친화적"인 모델을 산출합니다.

주요 기여

1. 통합 프레임워크: 이 논문은 도달 가능성, 안정성, 안전성, 최적화를 포함한 다양한 제어 작업에 $\alpha,\beta$-CROWN 을 적용하는 통합 접근법을 제시합니다.
2. GPU 병렬화를 통한 확장성: 경계 전파 및 분할 - 바운드의 효율적이고 병렬화 가능한 특성을 GPU 에서 활용함으로써, 특히 고차원 및 복잡한 비선형 시스템의 경우 기존 SMT 또는 MILP 기반 접근법보다 우수한 확장성을 달성합니다.
3. 범용 적용성: 특정 네트워크 아키텍처나 증명서 유형으로 제한된 방법들과 달리, $\alpha,\beta$-CROWN 은 삼각함수, 조각별 선형 등 다양한 연산자를 지원하는 계산 그래프로 표현된 일반 비선형 함수를 처리합니다.
4. 미분 가능성: 선형 경계 전파는 완전히 미분 가능하므로, 검증 제약을 학습 루프에 직접 통합 (인증된 학습) 할 수 있습니다.
5. 실용적 구현: 이 튜토리얼은 계산 그래프 정의, 도메인 특화 언어 (DSL) 를 사용한 제약 조건 수립, 검증, 경계 계산 및 최적화 작업 실행 방법을 보여주는 상세한 프로그래밍 인터페이스 (API) 와 코드 예제를 제공합니다. 또한 dReal API 를 위한 플러그인 호환성 계층도 제공합니다.

결과 및 주장

본 논문은 제안된 파이프라인이 기존 접근법에서 도전적인 검증 및 최적화 문제에서 우월한 확장성을 입증한다고 주장합니다.

• 효율성: GPU 에서 동시에 수만 개의 부분 영역을 처리할 수 있는 능력은 대규모 영역의 신속한 가지치기와 작은 영역에서의 거친 경계를 통한 인증을 가능하게 합니다.
• 다용도성: 이 프레임워크는 라야푸노프 안정성, 배리어 함수 안전성, 수축 지표 등 다양한 제어 사양을 상자 영역에 대한 만족도 문제로 재구성함으로써 성공적으로 처리합니다.
• 학습 이점: 논문은 2 차원 쿼드콥터 환경에서 인증된 학습 접근법으로 학습된 모델들이 CEGIS 를 사용하여 학습된 모델들보다 검증 속도가 5 배 빠르다고 지적하며, 이는 학습 목표가 직접적으로 검증 가능성을 향상시킨다고 시사합니다.

의의

이 연구의 의의는 제어 이론과 확장 가능한 신경망 검증 간의 간극을 해소하려는 시도에 있습니다. 통합적이고 효율적이며 범용적인 프레임워크를 제공함으로써, 저자들은 형식적 인증을 학습 기반 제어 설계의 더 실용적이고 필수적인 구성 요소로 만들고자 합니다. 이 튜토리얼은 복잡하고 학습된 제어 정책에 엄격한 검증 기법을 적용하는 진입 장벽을 낮추어, 안전-중요 시스템에 대한 경험적 테스트를 넘어 형식적 보장을 제공하는 데 기여합니다.