Training with Hard Constraints: Learning Neural Certificates and Controllers for SDEs

1. 연구 배경 및 문제 정의 (Problem)

• 배경: 확률 미분 방정식 (SDE) 으로 지배되는 시스템의 '도달 - 회피 (Reach-Avoid)' 제어 문제는 안전이 중요한 응용 분야 (예: 자율 주행, 항공) 에서 매우 중요합니다. 기존의 경험적 성능만으로는 안전 보장이 부족하며, 수학적 증명 (Formal Guarantees) 이 필요합니다.
• 핵심 문제:
  • SDE 시스템의 안전성을 보장하기 위해 초과martingale (Supermartingale) 기반의 인증서 (Certificate) 함수를 학습해야 합니다.
  • 이 인증서는 특정 불평등 (도달 확률 하한, 안전 집합 내에서의 감소 등) 을 전체 연속 영역 (Continuous Domain) 에서 만족해야 합니다.
  • 기존 신경망 (NN) 기반 접근법은 훈련 후 검증 (Post-training verification) 에 의존하거나, 제약 조건을 '소프트 (Soft)'하게 처리하여 전체 영역에서의 엄격한 보장 (Hard Guarantee) 을 제공하지 못했습니다.
  • 또한, 제어기 (Controller) 와 인증서 (Certificate) 를 동시에 학습하여 제어기가 인증 가능하도록 유도하는 방법도 부족했습니다.
• 목표:
  1. 신경망 훈련 과정에서 강제 제약 조건 (Hard Constraints) 을 직접 인코딩하여, 훈련 종료 시 제약 조건이 전역적으로 만족됨을 보장하는 방법 개발.
  2. 신경망 제어기와 인증서를 공동 학습 (Joint Synthesis) 하는 프레임워크 구축.

2. 제안된 방법론 (Methodology)

저자들은 두 가지 상보적인 훈련 프레임워크를 제안합니다.

A. Hard-SAT (Bound-Training Framework): 엄격한 보장 (Hard Guarantees)

• 개념: 도메인을 이산화 (Discretization) 하고 구간 산술 (Interval Arithmetic) 을 사용하여 각 셀 (Cell) 에서 신경망 출력의 상한/하한을 계산합니다.
• 손실 함수 (Loss Function):
  • 각 셀에서 인증서 제약 조건 (Eq. 4) 을 위반하는 정도를 측정하는 경계 기반 손실 (Bound-based Loss) 을 정의합니다.
  • 손실 함수가 0 이 되면, 해당 분할 (Partition) 내의 모든 점에 대해 제약 조건이 만족됨이 수학적으로 보장됩니다.
• 적응적 정제 및 병합 (Adaptive Refinement & Merging):
  • 차원이 증가함에 따라 셀 수가 기하급수적으로 늘어나는 문제 (Curse of Dimensionality) 를 해결하기 위해, 위반이 의심되는 셀만 선택적으로 세분화 (Refinement) 하거나, 조건을 충분히 만족하는 인접 셀을 병합 (Merging) 하는 전략을 사용합니다.
• 공동 학습: 제어기 파라미터가 포함된 미분 가능한 계산 그래프를 통해 제어기와 인증서를 동시에 최적화합니다.
• 한계: 5 차원 (5D) 시스템까지는 확장 가능하지만, 그 이상의 고차원 시스템에서는 분할 수가 너무 많아져 계산 비용이 prohibitive 해집니다.

B. Scenario-based Training: PAC 보장 (Probabilistic Guarantees)

• 개념: 상태 공간 분할 없이 무작위 샘플링을 기반으로 한 시나리오 최적화 (Scenario Optimization) 를 사용합니다.
• 접근 방식:
  • 신경망의 마지막 층 (Last Layer) 파라미터와 $\beta$ (확률 하한 관련 스칼라) 만을 변수로 하는 선형 계획법 (Linear Program, LP) 문제를 풉니다.
  • 충분한 수의 샘플 ($N$) 을 사용하여 제약 조건을 만족하도록 훈련합니다.
• 보장 (PAC Guarantee):
  • PAC (Probably Approximately Correct) 이론에 기반하여, 높은 확률 ($1-\delta$) 로 전체 상태 공간 중 매우 작은 영역 ($D_\epsilon$) 을 제외한 모든 곳에서 제약 조건이 만족됨을 보장합니다.
  • 샘플 수 $N$을 증가시키면 위반 영역의 부피 ($\epsilon$) 를 임의로 줄일 수 있습니다.
• 장점: 상태 공간 차원에 의존하지 않는 샘플 복잡도로 인해 10 차원 (10D) 이상의 고차원 시스템에도 확장 가능합니다.

3. 주요 기여 (Key Contributions)

1. Hard-SAT 프레임워크: 도메인 분할과 경계 기반 손실을 통해 신경망 인증서 훈련 시 전역적 강제 제약 조건 만족을 보장하는 방법론 제시.
2. 공동 합성 (Joint Synthesis): 제어기와 인증서를 하나의 통합된 손실 함수로 동시에 학습하여, 제어기가 검증 가능하도록 유도하는 알고리즘 개발.
3. 고차원 확장성 (Scalability): 분할 기반 방법의 한계를 극복하기 위해, PAC 보장을 제공하는 분할 없는 시나리오 기반 훈련 방법 제안 (최소 10D 시스템 지원).
4. 성능 입증: 다양한 벤치마크 (2D~10D GBM, Lorenz 시스템, XV-15 항공기 등) 를 통해 기존 최첨단 (SOTA) 방법보다 우수한 확장성과 검증 성공률을 입증.

4. 실험 결과 (Results)

• 검증 (Verification) 벤치마크:
  • 2D~5D 시스템: 제안된 Hard-SAT 방법은 기존 방법 (Neustroev et al., 2025) 보다 적은 분할 수로 더 빠르게 유효한 인증서를 찾았습니다. 5D GBM 에서도 성공적으로 작동했으나, 6D 이상에서는 메모리 부족으로 실패했습니다.
  • 10D 시스템: Hard-SAT 는 실패했으나, 시나리오 기반 방법이 $10^6$개의 샘플을 사용하여 10D GBM 에서 높은 신뢰도 ($1-10^{-9}$) 와 함께 유효한 인증서를 생성했습니다.
  • 정확도: 시나리오 기반 방법은 샘플 수를 늘림으로써 위반 영역 ($\epsilon$) 을 $10^{-4}$ 수준으로 줄일 수 있었습니다.
• 제어기 합성 (Control Synthesis):
  • 2D 역진자, 2D GBM, 3D 로렌츠 시스템, 3D XV-15 항공기 등 4 가지 복잡한 시스템에서 성공적으로 제어기와 인증서를 합성했습니다.
  • 모든 합성된 시스템에 대해 몬테카를로 시뮬레이션 결과, 도달 - 회피 확률이 1.0으로 확인되었습니다.
  • 특히, 사전 훈련 (Warm-start) 만으로는 유효한 인증서를 얻지 못했으나, 제안된 경계 기반 훈련을 통해 성공적으로 수렴함을 보였습니다.

5. 의의 및 결론 (Significance)

• 안전성 보장: 신경망 제어 시스템에 대해 "학습된 후 검증"이 아닌, "학습 과정 자체에서 제약 조건이 만족됨"을 보장하는 새로운 패러다임을 제시했습니다.
• 확장성: 기존에는 고차원 SDE 시스템에 대한 형식적 검증이 거의 불가능했으나, 제안된 두 가지 방법 (Hard-SAT 와 PAC 기반) 을 통해 5D~10D 이상의 시스템까지 확장 가능한 솔루션을 제공했습니다.
• 실용성: NASA XV-15 항공기와 같은 실제 복잡한 동역학 시스템에 적용 가능성을 보여주어, 안전이 중요한 자율 시스템의 신뢰성 확보에 기여합니다.
• 코드 공개: 모든 코드와 실험 설정을 GitHub 에서 공개하여 재현성을 보장합니다.

이 논문은 신경망 기반 제어 시스템의 안전성 검증 분야에서 엄격한 수학적 보장과 고차원 확장성이라는 두 마리 토끼를 잡은 획기적인 연구로 평가됩니다.