기술 요약: 부동 소수점 신경망은 증명 가능한 강건한 범용 근사 도구이다

1. 문제 정의

고전적인 범용 근사(Universal Approximation, UA) 정리와 최근의 구간 범용 근사(Interval Universal Approximation, IUA) 정리는 신경망이 연속 함수와 그 직접 이미지 맵(구간)을 임의의 정확도로 근사할 수 있음을 확립한다. 그러나 이러한 이론적 결과들은 신경망이 무한히 정밀한 실수 위에서 작동한다는 비현실적인 가정에 의존한다. 실제 구현에서는 소프트웨어가 유한 정밀도 부동 소수점 산술을 사용하며, 이는 이산화, 유계성, 반올림 오차 및 잠재적인 오버플로/언더플로를 유발한다.

본 논문이 다루는 핵심적인 미해결 질문은 IUA 정리가 부동 소수점 환경에서도 성립하는가 하는 점이다. 구체적으로, 부동 소수점 신경망이 추상 해석(구간 도메인)을 통해 분석될 때, 반올림된 타겟 함수의 직접 이미지 맵을 완벽하게 포착할 수 있는가? 기존 연구들은 이를 확립하지 못했는데, 이는 실수 기반 네트워크에서 사용되는 증명 기법(예: 정밀 산술에 의존하는 특정 서브 네트워크 구축)이 반올림 오차로 인해 무효화되기 때문이다.

2. 방법론

저자들은 실수 기반 이론과 부동 소수점 실무 사이의 간극을 메우기 위해 엄격한 이론적 프레임워크를 개발한다.

2.1 부동 소수점 의미론의 정식화

본 논문은 신경망을 IEEE-754 표준을 준수하는 연산($\oplus, \ominus, \otimes$)과 "최근접 짝수 반올림(round to nearest, ties to even)" 모드를 사용하는 유한 부동 소수점 집합 $\mathcal{F}$ 상의 함수로 정의한다. 구간 의미론 $\nu^\sharp$는 추상 구간 $\langle a, b \rangle$ (즉, $[a, b]$ 내의 부동 소수점 집합)에 대해 정의된다.

2.2 활성화 함수에 대한 조건

정리를 증명하기 위해, 저자들은 활성화 함수 $\sigma: \mathcal{F} \to \mathcal{F}$에 대한 제약 조건인 **조건 1(Condition 1)**을 도입한다. 이 조건들은 함수가 다음을 수행할 수 있도록 보장한다:

1. 정확한 0과 유계 범위 내의 특정 비제로(non-zero) 값을 출력함.
2. 임계값 $\eta$ 주변에서 단조성 또는 특정 임계 동작을 보임.
3. 무한한 성장을 방지하기 위해 립시츠 유사 연속성(Lipschitz-like continuity) 제약을 만족함.

본 논문은 적절하게 반올림된 일반적인 활성화 함수들(ReLU, GELU, Sigmoid, Tanh 등)이 Lemma 1을 활용하여 실수 함수와 부동 소수점 대응 관계를 매핑함으로써 이 조건들을 만족함을 입증한다.

2.3 증명 전략: 분리 가능성과 지시 함수 구축

증명의 핵심은 "범용 구간 근사기" 역할을 하는 신경망을 구축하는 것이다. 방법론은 두 가지 주요 단계로 진행된다.

1. 분리 가능성(Separability): 저자들은 $([a, b]_\mathcal{F}, \eta, K, L_\phi, L_\psi)$-분리 가능성이라는 속성을 정의한다. 이 속성은 구간 의미론 하에서 스케일링된 지시 함수(예: 입력이 $z$ 이하이면 0을, $z$보다 크면 $K$를 매핑하는 함수)를 구현할 수 있는 네트워크의 존재를 보장한다.

   • 증명은 반올림 오차를 이용하여 구간을 "축소(contract)"하는 특정 서브 네트워크(예: $\mu_z, \tau_{\theta, \theta'}$)를 구축한다. 예를 들어, 특정 범위의 입력이 활성화 함수를 통과한 후 단일 구간 $\langle \eta, \eta \rangle$ 또는 $\langle \eta^+, \eta^+ \rangle$로 매핑되도록 설계된다.
   • 결정적으로, 이 구조는 가중치를 임의의 크기로 스케일링할 때 발생하는 실수 기반 증명의 고질적 문제인 중간 레이어에서의 오버플로 문제를 해결한다.

2. 범용 근사를 위한 합성: 분리 가능성 속성을 사용하여 다음을 위한 네트워크를 구축한다:

   • 임의의 박스(box)에 대한 지시 함수.
   • 입력 공간의 임의의 부분 집합에 대한 지시 함수.
   • 최종적으로, 이러한 지시 함수들의 부동 소수점 선형 결합으로 타겟 함수 자체를 표현함으로써 타겟 함수를 구성한다. 증명 과정에서는 누적된 반올림 오차가 타겟 함수의 이미지 맵을 완벽하게 재구성하도록 부동 소수점 합산을 정교하게 관리한다.

3. 주요 기여

3.1 부동 소수점 IUA 정리 (정리 1)

본 논문은 임의의 타겟 함수 $f: \mathbb{R}^d \to \mathbb{R}$와 조건 1을 만족하는 광범위한 활성화 함수 클래스에 대하여, 구간 의미론 $\nu^\sharp$가 도메인 $[-1, 1]^d \cap \mathcal{F}^d$ 상의 반올림된 타겟 함수 $\hat{f}$의 직접 이미지 맵을 정확하게(exactly) 계산하는 부동 소수점 신경망 $\nu$가 존재함을 증명한다.

• 정확성(Exactness): $\delta$-근사를 달리는 실수 기반 IUA와 달리, 부동 소수점 버전은 도메인이 유한하므로 $\delta = 0$ (완전 일치)을 달성한다.
• 일반성(Generality): 이 정리는 연속 함수뿐만 아니라 임의의 타겟 함수에 대해 성립하며, 항등 함수(identity function)를 포함한 광범위한 활성화 함수에 적용된다(실수 기반 IUA에서는 불가능한 일).

3.2 증명 가능한 강건한 네트워크의 존재 (정리 2)

결론으로서, 본 논문은 이상적인 강건 분류기(비록 그것이 신경망이 아닐지라도)가 존재한다면, 구간 분석을 통해 증명 가능한 강건성을 가지며 동일한 예측을 수행하는 부동 소수점 신경망이 존재함을 증명한다. 이는 부동 소수점 환경에서 증명 가능한 강건한 네트워크의 표현력에 근본적인 한계가 있는지에 대한 의문을 해결한다: 그러한 한계는 존재하지 않는다.

3.3 부동 소수점 구간 완비성 (정리 3)

본 논문은 계산 완비성에 관한 놀라운 결과를 확립한다: 덧셈($\oplus$)과 곱셈($\otimes$)만을 사용하는 직선형(straight-line) 부동 소수점 프로그램의 클래스는 **부동 소수점 구간 완비적(floating-point interval-complete)**이다. 즉, 이러한 단순한 프로그램들은 유한한 부동 소수점을 입력으로 받아 유한 또는 무한한 부동 소수점을 반환하는 모든 종료되는 부동 소수점 프로그램의 구간 의미론을 시뮬레이션할 수 있다. 이 결과는 IUA 정리를 전체 도메인 $\mathcal{F}^d$ 상의 항등 활성화 함수로 확장한다.

4. 결과 및 비교

본 논문은 새로운 부동 소수점 IUA 정리와 기존의 실수 기반 결과 사이의 세 가지 근본적인 차이점을 강조한다:

1. 타겟 함수: 실수 기반 IUA는 연속 함수를 근사하지만, 부동 소수점 IUA는 (도메인이 유한하므로) 임의의 반올림된 타겟 함수의 이미지를 정확하게 계산한다.
2. 활성화 함수: 실수 기반 IUA는 "압착 가능한(squashable)" 비-아핀(non-affine) 활성화 함수를 요구하지만, 부동 소수점 IUA는 항등 함수에 대해서도 성립한다. 이는 부동 소수점 아핀 변환이 반올림 오차로 인해 실수 상에서 엄격한 아핀이 아니므로, 선형성을 깨고 비선형적 동작을 근사할 수 있기 때문이다.
3. 근사 vs 정확성: 실수 기반 결과는 $\delta$-근사를 제공하지만, 부동 소수점 결과는 반올림된 타겟 함수에 대한 정확한 일치를 제공한다.

5. 의의 및 주장

저자들은 이 연구가 추상 해석 기반의 강건성 검증과 실제 부동 소수점 구현 사이의 이론적 간극을 메운다고 주장한다.

• 이론적 보증: 증명 가능한 강건한 네트워크의 성능 저하가 표현력의 근본적인 한계 때문이 아니라, 최적화의 어려움이나 사용된 특정 검증 알고리즘 때문일 가능성이 높음을 보여준다.
• 완비성: 구간 완비성 결과는 단순한 산술 연산만으로도 복잡한 부동 소수점 동작을 시뮬레이션할 수 있음을 시사하며, 이는 구간 의미론 하의 부동 소수점 프로그램의 계산 능력에 대한 새로운 통찰을 제공한다.
• 실무적 관련성: IUA 정리를 부동 소수점 숫자로 검증함으로써, 본 논문은 부동 소수점 산술이 표준인 안전 필수 도메인(의료, 자율 주행 등)에서 구간 분석을 사용하는 것에 대한 이론적 토대를 제공한다.

본 논문은 이것들이 존재 증명임을 명시한다. 즉, 현재의 훈련 알고리즘이 그러한 네트워크를 쉽게 찾아낼 수 있다고 주장하거나 새로운 훈련 방법을 제안하는 것이 아니다. 기여는 순수하게 이론적이며, 증명 가능한 강한 부동 소수점 네트워크의 "표현력 천장"이 사실상 존재하지 않음을 확립하는 것이다.