技術要約：浮動小数点ニューラルネットワークは、証明可能なロバスト性を備えた万能近似器である

1. 問題提起

古典的な万能近似（Universal Approximation, UA）定理、およびより新しい区間万能近似（Interval Universal Approximation, IUA）定理は、ニューラルネットワークが連続関数やその直接像（区間）を任意の精度で近似できることを確立している。しかし、これらの理論的結果は、ニューラルネットワークが無限に精密な実数上で動作するという非現実的な仮定に基づいている。実際には、ソフトウェアの実装は有限精度の浮動小数点演算を使用しており、これにより離散化、有界性、丸め誤差、およびオーバーフロー／アンダーフローの可能性が生じる。

本論文が取り組む中心的な未解決問題は、IUA定理が浮動小数点の設定においても成立するかどうかである。具体的には、浮動小数点ニューラルネットワークは、抽象解釈（区間ドメイン）を通じて分析された際、丸められたターゲット関数の直接像を完全に捉えることができるのだろうか。これまでの研究では、これは確立されていなかった。その理由は、実数値ネットワークで使用される証明技法（例：特定のサブネットワークの構築）が、丸め誤差によって無効化されるためである（正確な算術に依存する特定のサブネットワークの構築が失敗してしまう）。

2. 手法

著者らは、実数値理論と浮動小数点の実際との間の溝を埋めるための、厳密な理論的枠組みを開発した。

2.1 浮動小数点意味論の定式化

本論文では、IEEE-754準拠の演算（$\oplus, \ominus, \otimes$）および「最も近い値への丸め（偶数への丸め）」モードを利用して、有限個の浮動小数点数の集合 $\mathcal{F}$ 上の関数としてニューラルネットワークを定義する。区間意味論 $\nu^\sharp$ は、抽象区間 $\langle a, b \rangle$（$[a, b]$ 内の浮動小数点の集合を表す）上で定義される。

2.2 活性化関数に関する条件

定理を証明するために、著者らは活性化関数 $\sigma: \mathcal{F} \to \mathcal{F}$ に対する一連の制約である条件1を導入する。これらの条件は、関数が以下の機能を備えていることを保証するものである：

1. 正確なゼロおよび、有界な範囲内の特定の非ゼロ値を出力すること。
2. 臨界値 $\eta$ の周囲で単調性または特定の閾値処理挙動を示すこと。
3. 無限の増大を防ぐための、リプシッツ連続性に似た連続性の制約を満たすこと。

本論文は、一般的な活性化関数（ReLU, GELU, Sigmoid, Tanhなど）の正しく丸められたバージョンが、Lemma 1（実数値関数の特性を浮動小数点の特性へと写像するもの）を活用することで、これらの条件を満たすことを示している。

2.3 証明戦略：分離可能性とインジケータ構成

証明の核心は、「万能区間近似器」として機能するニューラルネットワークを構築することにある。手法は主に2つの段階で進行する。

1. 分離可能性（Separability）： 著者らは、$([a, b]_\mathcal{F}, \eta, K, L_\phi, L_\psi)$-分離可能性と呼ばれる特性を定義する。この特性は、区間意味論の下で、スケーリングされたインジケータ関数（例：入力を $z$ 以下にマップして0とし、入力を $z$ より大きくマップして $K$ とする関数）を実装できるネットワークが存在することを保証する。

   • 証明では、丸め誤差を利用して区間を「収縮」させる特定のサブネットワーク（例：$\mu_z, \tau_{\theta, \theta'}$）を構築する。例えば、あるネットワークは、活性化関数を通過した後、特定の範囲の入力が単一の区間 $\langle \eta, \eta \rangle$ または $\langle \eta^+, \eta^+ \rangle$ にマップされるように設計される。
   • 決定的な点として、この構築は中間層における無限値を回避しており、重みを任意の大きさまでスケーリングする際に問題となるオーバーフローの問題に対処している。

2. 万能近似のための合成： 分離可能性の特性を用いて、以下のためのネットワークを構築する：

   • 任意のボックスのインジケータ関数。
   • 入力空間の任意の部分集合のインジケータ関数。
   • そして最終的に、これらのインジケータ関数の浮動小数点線形結合としてターゲット関数自体を表現することで、ターゲット関数を構築する。証明では、ターゲット関数の像を完全に再構成するために、蓄積される丸め誤差が完全に一致するように、浮動小数点の総和を慎重に管理している。

3. 主要な貢献

3.1 浮動小数点IUA定理（定理1）

本論文は、任意のターゲット関数 $f: \mathbb{R}^d \to \mathbb{R}$ と、条件1を満たす幅広いクラスの活性化関数に対して、その区間意味論 $\nu^\sharp$ が、ドメイン $[-1, 1]^d \cap \mathcal{F}^d$ 上の丸められたターゲット関数 $\hat{f}$ の直接像を正確に計算するような、浮動小数点ニューラルネットワーク $\nu$ が存在することを証明している。

• 正確性： 実数値のIUAが $\delta$ 近似を実現するのに対し、浮動小数点版は、ドメインが有限であるため $\delta = 0$（完全一致）を達成する。
• 汎用性： この定理は、連続関数に限らず（連続でない関数でも）、恒等関数を含む幅広い活性化関数に対して成立する。

3.2 証明可能なロバスト性を備えたネットワークの存在（定理2）

補言として、もし理想的なロバスト分類器が存在するならば（それがニューラルネットワークであるかどうかにかかわらず）、区間解析を通じて証明可能なロバスト性を備え、同一の予測を行う浮動小数点ニューラルネットワークが存在することを証明する。これは、浮動小数点の設定において、証明可能なロバスト性を備えたネットワークの表現能力に根本的な限界が存在するかどうかという問いを解決するものである。結論は、そのような限界は存在しない。

3.3 浮動小数点区間完全性（定理3）

本論文は、計算の完全性に関する驚くべき結果を確立している。加算 ($\oplus$) と乗算 ($\otimes$) のみを使用する直線的な浮動小数点プログラムのクラスは、浮動小数点区間完全である。これは、単純なプログラムが、有限の浮動小数点を入力として受け取り、有限または無限の浮動小数点を返す、あらゆる終了する浮動小数点プログラムの区間意味論をシミュレートできることを意味する。この結果は、IUA定理を全ドメイン $\mathcal{F}^d$ における恒等活性関数へと拡張するものである。

4. 結果と比較

本論文は、新しい浮動小数点IUA定理と従来の、実数値の結果との間の3つの根本的な相違点を強調している：

1. ターゲット関数： 実数値のIUAは連続関数を近似するが、浮動小数点IUAは、丸められたターゲット関数の像を正確に計算する（ドメインが有限であるため）。
2. 活性化関数： 実数値のIUAは「押しつぶし型（squashable）」の非アフィンな活性化関数を必要とするが、浮動小数点IUAは恒等関数に対しても成立する。これは、浮動小数点のアフィン変換が、丸め誤差のために実数上では厳密にはアフィンではないため、線形性を打破し、非線形な挙動を近似できるからである。
3. 近似 vs 正確性： 実数値の結果は $\delta$ 近似を提供するが、浮動小数点の結果は、丸められたターゲットに対する正確な一致を提供する。

5. 意義と主張

著者らは、本研究が、抽象解釈に基づくロバスト性検証と、実用的な浮動小数点実装との間の理論的な溝を埋めるものであると主張している。

• 理論的保証： これは、最先端のロバスト・ネットワークの精度不足が、その表現能力における根本的な限界によるものではなく、おそらく最適化の課題や使用されている特定の検証アルゴリズムに起因することを示している。
• 完全性： 区間完全性の結果は、単純な算術演算が、区間意味論の下で複雑な浮動小数点挙動をシミュレートするのに十分であることを示唆しており、浮動小数点プログラムの計算能力に関する新たな洞察を提供している。
• 実用的な関連性： 浮動小数点演算が標準である安全性が重視される領域（ヘルスケア、自動運転など）において、区間解析を使用するための理論的基礎を提供することで、IUA定理の妥当性を検証している。

本論文は、これらがあくまで存在証明であることを明記している。現在の学習アルゴリズムがそのようなネットワークを容易に見つけられると主張しているわけでも、新しい学習手法を提案しているわけでもない。貢献は厳密に理論的なものであり、「証明可能なロバスト性を備えた浮動小数点ネットワークの表現力の天井」は事実上存在しないことを確立している。