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

작성자

Haebom

카테고리

Empty

저자

Ali Baheri, David Millard, Ignacio Laguna Peralta

💡 개요

본 연구는 학습된 푸리에 신경망 연산자(FNO)의 물리적 구조 보존 여부를 형식적으로 검증할 수 있는지 탐구합니다. FNO의 스펙트럼 컨볼루션을 선형 맵으로 간주하여 Z3의 선형 실수 산술로 정확하게 표현할 수 있음을 보이며, 이를 통해 FNO 모델의 물리 법칙 위배 여부를 검증하는 두 가지 인코딩 방식을 제안합니다. 제안된 방식은 소규모 FNO 모델에서 물리 법칙 위배 사례를 성공적으로 탐지하고 일부는 물리 법칙을 보존함을 증명합니다.

🔑 시사점 및 한계

•

FNO의 스펙트럼 컨볼루션이 고정된 가중치 및 그리드에서 선형 맵임을 증명함으로써, 형식 검증 가능성의 이론적 기반을 제공합니다.

•

제안된 형식 검증 방법론은 FNO가 기본적인 물리 법칙(예: 양수성, 질량 보존)을 위배하는 경우를 효과적으로 탐지하고, 일부 모델의 경우 물리 법칙 보존을 증명할 수 있음을 보여줍니다.

•

본 연구에서 제시된 '정확한 인코딩'은 소규모 모델에서는 효과적이나, ReLU 모델의 양수성 검증에서 시간 초과가 발생하는 등 복잡한 모델에 대한 확장성에 한계가 있습니다. '가벼운 동결 인코딩'은 확장성이 좋으나 원본 FNO에 대한 인증을 제공하지 못합니다. 따라서 실제 규모의 FNO에 대한 형식 검증을 위해서는 확장성과 정확성 간의 균형을 맞추는 추가적인 연구가 필요합니다.

PDF 보기

Made with Slashpage