기술 요약: 비선형 동역학의 인증된 신경 근사 (Certified Neural Approximations of Nonlinear Dynamics)

문제 정의

비선형 동역학 시스템은 사이버 물리 시스템(cyber-physical systems)의 근간을 이루지만, 직접적으로 검증하거나 제어하기는 어렵습니다. 일반적인 전략은 추상화(abstraction)—즉, 원래 시스템을 근사하는 단순화된 모델—를 구축하는 것입니다. 신경망은 상태 공간을 암묵적으로 분할하고 단순화된 동역학을 학습할 수 있는 능력을 갖추고 있어, 이러한 목적을 위한 효과적인 도구로 부상했습니다.

그러나 이러한 신경 추상화가 중요한 응용 분야에서 안전하기 위해서는, 실제 시스템과의 근접성에 대한 **형식적 보증(formal guarantees)**이 반드시 수반되어야 합니다. 구체적으로, 주어진 도메인에 대해 신경망 $N(x)$가 실제 동역학 $f(x)$를 유계된 오차 $\epsilon$ 내에서 근사하는지(즉, $\|f(x) - N(x)\|_\infty \le \epsilon$) 인증해야 합니다.

기존의 검증 방법들은 비선형 실수 산술(nonlinear real arithmetic)을 추론하기 위해 SMT(Satisfiability Modulo Theories) 솔버(예: dReal)에 크게 의존합니다. 이러한 솔버들은 건전성(soundness)은 갖추고 있으나, 더 큰 네트워크나 고차원 시스템을 합리적인 시간 내에 검증하는 데 심각한 확장성 문제를 겪습니다. 이러한 계산적 병목 현상은 복잡하고 고차원적인 시나리오에서 신경 추상화의 실질적인 적용을 제한합니다.

방법론

저자들은 비용이 많이 드는 비선형 산술 SMT 솔버에 대한 의존성을 제거하는 새로운 확장 가능한 검증 프레임워크를 제안합니다. 대신, 이 방법은 **인증된 1차 테일러 모델(certified first-order Taylor models)**과 **병렬 가능한 적응형 분할 전략(parallelizable adaptive partitioning strategy)**을 활용합니다.

1. 인증된 1차 테일러 모델

비선형 술어 $\exists x : \|f(x) - N(x)\| > \epsilon$를 직접 검증하는 대신, 이 방법은 1차 테일러 전개를 사용하여 국소적으로 실제 동역학 $f(x)$를 근사합니다.

• 국소 선형화(Local Linearization): 입력 도메인 $X$를 초직육면체(hyperrectangles)로 분할합니다. 중심점이 $c$인 각 초직육면체 $H_\delta(c)$ 내에서, 동역학은 선형 함수와 나머지 항(remainder term)에 의해 경계가 정해집니다:
  $$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$$
  여기서 $J_f(c)$는 야코비안(Jacobian)이며, $R$은 (매끄러운 함수의 경우 Lagrange error bound 또는 ReLU 네트워크의 경우 CROWN으로부터 유도된) 인증된 오차 범위입니다.
• 선형 솔버를 통한 검증: 이 변환은 검증 문제를 선형 부등식의 만족 가능성을 확인하는 문제로 전환합니다. 저자들은 선형 경계 전파(linear bound propagation)를 기반으로 하는 신경망 검증 도구인 Marabou 2.0을 사용하여 이러한 조건을 검증합니다. 이를 통해 비선형 산술 추론의 계산 비용을 피할 수 있습니다.

2. 적응형 인증 정밀화 (Adaptive Certificate Refinement)

선형 근사로 인해 발생하는 보수성(선형화로 인해 오차 $R$이 너무 커지는 경우)을 해결하기 위해, 프레임워크는 적응형 정밀화 전략을 채택합니다.

• 분할 기준(Splitting Criteria): 다음의 경우 초직육면체를 분할합니다:
  1. 테일러 나머지(Taylor remainder)의 경계가 너무 보수적인 경우 ($R_{max} - R_{min} > \epsilon$).
  2. 솔버가 찾은 잠재적 반례가 실제 오차 조건을 만족하지 않는 경우 (선형화로 인한 "가짜" 반례).
• 표적 분할(Targeted Partitioning): 분할 축은 근사 오차에 대한 입력 차원의 기여도를 기준으로 선택되며, 비선형 항과 관련된 차원을 우선시합니다. 이를 통해 **출력 의존적 정밀화(output-dependent refinement)**가 가능해져, 서로 다른 출력 차원이 서로 다른 수준의 분할을 요구할 수 있습니다.
• 병렬화: 검증 과정은 공유 스택(깊이 우선 탐색)을 사용하는 방식으로 병렬화되며, 이는 작업자 프로세스 풀(pool of worker processes)에 의해 접근됩니다. 각 작업자는 초직육면체를 처리하거나, 인증하거나, 혹은 분할하여 하위 영역을 다시 스택에 넣습니다.

3. 학습 (Training)

신경망은 평균 제곱 오차(MSE)와 샘플링된 입력에 대한 최대 $L_\infty$ 오차를 모두 최소화하도록 학습됩니다. 손실 함수에는 샘플 효율성을 높이기 위해 최악의 경우 오차(worst-case error)에 대한 항이 포함됩니다.

주요 기여

1. SMT-Free 검증: 인증된 선형화를 기반으로 하여 기존 방식의 주요 병목 현상인 비선형 실수 산술 추론을 제거한 방법을 도입했습니다.
2. 적응형 병렬 정밀화: 입력 도메인 전체에 걸쳐 비균일한 정확도를 가질 수 있는 적응형 검증을 가능하게 함으로써, 건전성을 해치지 않으면서 보수성을 크게 줄이는 확장 가능한 전략을 제공합니다.
3. 확장성: 고차원 시스템(최대 7D) 및 기존의 최첨단 방법들보다 훨씬 큰 신경망을 다룰 수 있는 능력을 보여줍니다.
4. 새로운 응용 분야: 이전에 다루기 힘들었던 두 가지 시나리오로 신경 추상화를 확장했습니다:
   • 신경망 압축(Neural Network Compression): 압축된 네트워크가 더 큰 "교사(teacher)" 네트워크와 $\epsilon$-근접함을 검증합니다.
   • 코업만 연산자 발견(Koopman Operator Discovery): 네트워크 출력이 미래 상태의 시퀀스를 나타내는 궤적 수준의 예측을 검증합니다 (최종 레이어에서 100개 이상의 상태).

실험 결과

본 방법은 문헌의 확립된 벤치마크(예: WaterTank, JetEngine, Van der Pol Oscillator)와 새로운 도전적인 과제들을 통해 평가되었습니다.

• 최첨단 기술(SOTA) 대비 성능: dReal 기반 접근 방식(Abate et al., 2022)과 비교했을 때, 제안된 방법은 상당한 속도 향상을 보여주었습니다. 예를 들어, WaterTank 벤치마크에서 새 방법은 약 820배 더 빨랐습니다. dReal은 대부분의 대규모 모델(예: JetEngine의 3x[64] 구조, SteamGovernor)에서 시간 초과(1시간 제한)가 발생했지만, 제안된 방법은 Low Thrust Spacecraft(7D)와 같은 고차원 시스템을 포함하여 테스트된 모든 모델의 도메인을 100% 성공적으로 인증했습니다.
• 코업만 연산자(Koopman Operators): 프레임워크는 코업만 이론에 기반한 궤적 예측 네트워크를 성공적으로 검증했습니다. 해당 네트워크가 검증 데이터에서 낮은 MSE를 달ered음에도 불구하고, 검증 과정에서 오차가 허용 오차($\epsilon=0.1$)를 초과하는 특정 반례를 식별해 냈습니다. 결정적으로, 이 방법은 입력 도메인의 **99.03%**를 인증함으로써, 단일 반례만을 반환하는 기존 방식과 달리 모델이 신뢰할 수 있는 지점에 대한 세밀한 통찰을 제공했습니다.
• 신경 압축: 본 방법은 Lorenz attractor의 동역학을 근사하는 압축된 네트워크(4.2M에서 67k 파라미터로, 98.4% 감소)를 검증했습니다. 검증 과정은 350만 개 이상의 초직육면체를 처리했으며, 약 89시간 만에 완료되어 대규모의 비해석적(non-analytical) 동역학에 대한 실행 가능성을 입증했습니다.

의의 및 주장

본 논문의 주요 의의는 신경 추상화 검증의 확장성 병목 문제를 해결하는 데 있다고 주장합니다. 신경 네트워크의 검증(선형 솔버가 처리)을 비선형 동역학의 검증(국소 선형화 및 정밀화를 통해 처리)으로부터 분리함으로써, 저자들은 이전에 다루기 힘들었던 복잡하고 고차원적인 시스템의 형식적 검증을 가능하게 했습니다.

저자들은 이 접근 방식이 형식적 오차 경계를 제공하여, 오차를 유계된 교란(bounded disturbances)으로 해석함으로써 신경 근사가 안전한 대리 모델(surrogates)로 사용될 수 있게 한다고 강조합니다. 이러한 건전성은 추상화에서 검증된 속성(예: 안전성 또는 도달 가능성)이 실제 시스템으로 엄격하게 전이될 수 있게 합니다. 또한, 이 연구는 프레임워크의 다재다능함을 강조하며, 표준적인 동역학 시스템을 넘어 일반적인 함수 근사 작업(예: 네트워크 압축 및 연산자 이론을 위한 딥러닝 아키텍처)에도 적용될 수 있음을 보여줍니다.