Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators

기술 요약: 소형 푸리에 신경 연산자의 SMT 컴파일

문제 제기
푸리에 신경 연산자 (FNO) 는 편미분 방정식 (PDE) 시뮬레이션에 상당한 가속화를 제공하지만, 질량 보존이나 농도의 양수성 같은 물리적 제약에 대한 형식적 보장을 종종 제공하지 못합니다. 표준 검증은 몬테카를로 (MC) 테스트나 그라디언트 기반 위조 (falsification) 에 의존하지만, 이러한 방법들은 특정 입력만 샘플링하며 연속적인 입력 영역에 대한 포괄적인 보장을 제공할 수 없습니다. 기존 신경망 검증 도구는 주로 분류기나 제어 정책에 설계되었으며, 스펙트럼 컨볼루션, 함수 공간 입력, 또는 보존 법칙과 같은 PDE 고유의 속성을 기본적으로 처리하지 못합니다.

방법론
저자들은 훈련된 FNO 를 형식적 검증을 가능하게 하는 SMT(Satisfiability Modulo Theories) 솔버, 구체적으로 Z3 로 컴파일하는 것을 제안합니다. 핵심 통찰은 고정된 그리드와 고정된 훈련 가중치 하에서 FNO 의 스펙트럼 컨볼루션이 선형 사상이라는 점입니다. 결과적으로 ReLU 비선형성을 가진 FNO 는 정확히 Z3 의 선형 실수 산술로 표현될 수 있는 조각별 선형 사상이며, 순전파를 근사화하지 않고 표현할 수 있습니다.

방법론은 두 가지 주요 인코딩 전략을 포함합니다:

1. 정확한 인코딩 (Exact Encoding): 스펙트럼 컨볼루션은 표준 기저 벡터에 연산을 적용하여 명시적인 조밀 행렬 ($W^{spec}$) 로 컴파일됩니다. 전체 순전파는 아핀 사상의 합성과 좌표별 ReLU 함수의 합성으로 표현됩니다. 이 인코딩은 정연 (sound) 하여, "UNSAT" 결과는 모든 허용 가능한 입력에 대해 속성이 성립함을 증명하고, "SAT" 결과는 유효한 반례를 제공합니다. 그러나 복잡도가 $O(N^2H^2L)$로 증가하여 작은 그리드 크기 ($N \le 32$) 로 제한됩니다.
2. 동결 인코딩 (Frozen Encoding): 더 큰 그리드 ($N \le 64$) 로 확장하기 위해, 스펙트럼 경로는 참조 입력에서 유도된 상수로 대체됩니다. 이는 복잡도를 $O(NH^2L)$로 줄이고 초 단위 이하의 검사를 가능하게 합니다. 그러나 이는 근사화이므로, "UNSAT" 결과는 원래 FNO 가 아닌 동결된 대리 모델 (surrogate) 만 인증하며, "SAT" 결과는 원래 모델에서의 검증이 필요합니다.

실험은 주기적 경계 조건을 가진 1 차원 대류 - 확산 - 반응 (ADR) 방정식에 초점을 맞춥니다. 연구는 두 가지 속성을 검증합니다:

• 질량 비증가: 출력의 이산 질량이 입력 질량을 허용 오차 $\epsilon = 0.05$만큼 초과하는지 확인합니다.
• 양수성: 음수가 아닌 입력이 모든 그리드 점에서 음수가 아닌 출력을 생성하는지 확인합니다.

주요 기여

• 정확한 컴파일: 명시적 스펙트럼 행렬을 구성함으로써 고정 그리드 FNO 를 Z3 의 선형 실수 산술로 정확하게 컴파일한 최초의 사례를 제시합니다.
• 최초의 형식적 증명: 16 까지의 그리드 크기에서 선형 (ReLU 없는) FNO 에 대한 양수성 인증서를 생성하는 등 신경 PDE 연산자에 대한 최초의 정연한 형식적 증명을 제공합니다.
• 비교 분석: 10 개의 소형 모델 (85~117 개 파라미터) 에 걸쳐 Z3 를 그라디언트 기반 위조 및 몬테카를로 테스트와 비교합니다.
• 정연성 - 확장성 경계: 저자들은 정확한 검증과 확장성 사이의 트레이드오프를 특징화하여, 정확한 인코딩이 작은 선형 모델에 대한 증명과 중간 규모의 ReLU 모델에 대한 반례를 지원하지만, 근사적 인코딩은 더 확장되지만 원래 모델에 대한 형식적 정연성을 잃음을 보여줍니다.

결과

• 질량 비증가: 정확한 인코딩을 사용하여 Z3 는 10 개 모델 모두에 대한 정연한 질량 위반 반례를 찾았습니다. 10 개 모델 중 7 개에서 Z3 는 그라디언트 기반 위조 및 MC 테스트보다 더 심각한 위반을 발견했습니다. 선형 모델의 경우 Z3 는 더 깊은 위반을 찾기 위해 전역적으로 최적화했으며, ReLU 모델의 경우 그라디언트 탐색이 여전히 경쟁력이 있었습니다.
• 양수성:
  • 선형 모델 (L=1): Z3 는 2 개의 정연한 양수성 증명 ($N=8$ 및 $N=16$ 그리드 크기) 을 생성하고 다른 선형 모델에서 4 개의 정연한 반례를 찾았습니다.
  • ReLU 모델 (L=2): Z3 는 1 개의 정연한 반례를 찾았지만, 활성화 패턴의 조합적 폭발 ($2^{NH}$) 로 인해 나머지 3 개의 양수성 쿼리에서 시간 초과가 발생했습니다. 그라디언트 위조는 4 개의 ReLU 모델 모두에서 위반을 성공적으로 발견했으며, 종종 Z3 보다 더 심각한 수준이었습니다.
• 동결 인코딩: 이 접근법은 8 개의 더 큰 모델 ($N=32$에서 $64$) 에서 양수성을 성공적으로 검증하고 그 중 4 개에서 질량 반례를 찾았습니다. 그러나 이러한 결과는 근사적입니다. 양수성 증명은 동결된 대리 모델에만 적용되며, 질량 반례는 원래 모델에서 재검증이 필요했습니다 (3 개 확인, 1 개 미확인).

의의 및 주장
이 논문은 생산 규모 검증을 위한 해결책이 아닌 개념 증명 (proof of concept) 으로 자신을 위치시킵니다. 저자들은 명시적으로 결과가 대규모 FNO 검증을 해결하지 못한다고 밝히며, 테스트된 모델은 고정된 은닉 층과 제한된 파라미터를 가진 "장난감 크기"라고 말합니다.

의의는 다음을 입증하는 데 있습니다:

1. FNO 는 조각별 선형 형태로 정확하게 컴파일되어 물리 기반 속성에 대한 SMT 솔버의 사용을 가능하게 합니다.
2. 형식적 검증은 작고 선형인 신경 연산자에 대해 가능하며, 이러한 시스템에 대한 최초의 정연한 인증서를 산출합니다.
3. 명확한 경계가 존재합니다. 즉, 정확한 증명은 현재 작은 선형 모델에만 실용적이며, 정확한 반례는 중간 규모의 ReLU 모델로 확장됩니다. 더 큰 연산자는 범용 SMT 솔버 대신 근사적 인코딩이나 확장 가능한 특수 신경망 검증기 (예: $\alpha$-$\beta$-CROWN) 와의 통합이 필요합니다.

저자들은 이 작업이 형식적 검증 커뮤니티가 신경 PDE 대리 모델에 참여하도록 장려하며, 연산자 학습 커뮤니티가 검증 가능성을 설계 기준으로 삼아야 함을 시사한다고 결론지었습니다.