\texttt{Range-Arithmetic}: Verifiable Deep Learning Inference on an Untrusted Party

技術要約：Range-Arithmetic – 信頼できない第三者による検証可能なディープラーニング推論

問題提起
分散型機械学習（ML）システムは、ブロックチェーンの制限を克服するために、リソース集約的なタスク（深層ニューラルネットワーク（DNN）の推論など）を信頼できない外部の当事者（プルーバー／証明者）にオフロードすることにますます依存しています。ここでの重要な課題は、検証者がプロセス全体を再実行する必要なく（再実行は往々にして非常に高コストであるため）、これらのアウトソーシングされた計算の完全性を確保することです。

既存の検証可能計算（VC）技術は、MLに適用する際に大きな障壁に直面しています。ほとんどのVCスキームは有限体上で動作し、算術演算（加算と乗算）に限定されています。しかし、標準的なMLの計算には、非算術的な操作が含まれます。具体的には以下の通りです：

1. 固定小数点丸め（Fixed-point rounding）: 行列乗算の後に、精度管理およびオーバーフロー防止のために必要となります。
2. 非線形活性化関数: ReLU（整流線形ユニット）などの操作です。

これらの操作を従来のVCフレームワーク内で表現するには、複雑なブール回路エンコーディング、高次多項式、または大規模な事前計算済みルックアップテーブルが必要になることが多く、これらはプルーバーの労力、検証者のコスト、および通信帯域幅に多大なオーバーヘッドをもたらすか、あるいはReLUと丸めの両方を同時にサポートすることに失敗します。

手法：Range-Arithmetic フレームワーク
著者らは、有限体ベースの証明システムとの互換性を維持しながら、DNN推論を効率的に検証するために設計された新しいフレームワークである Range-Arithmetic を提案しています。核心となる革新は、非算術的な操作を、ブールエンコーディングやルックアップテーブルを使用せずに、sum-checkプロトコルと連結された範囲証明（range proofs）を通じて検証可能な算術ステップへと変換することにあります。

このフレームワークは、以下のメカニズムを通じて動作します：

1. 行列乗算の検証:
   行列乗算（$C = AB$）の検証は、sum-check問題として再定式化されます。行列の要素を有限体上の多項式拡張（MLE）として表現することで、積の正当性の検証は多項式の恒等性を検証することへと還元されます。著者らは、Schwartz-Zippelの補題を利用して、ランダムな点におけるこの恒等性をチェックし、通信複雑性を $O(\log n)$ に低減させるためにsum-checkプロトコルを採用しています。

2. 丸めの検証:
   乗算の後に適用される丸め操作 $R(x)$ を検証するために、著者らはプロセスを算術的制約へと分解します。彼らは、丸みによって破棄される部分（$E$）と、丸みの分数の分子（$D$）を定義します。正当性は、集約された範囲証明（aggregated range proofs） を通じて以下の2つの条件を証明することで保証されます：

   • 破棄されたビットが特定の狭い区間（$-2^{s-1} \leq e_i < 2^{s-1}$）内に存在すること。
   • 残りの値が、ラップアラウンド（桁溢れ）なしに $2^s$ の整数倍であること。
     このアプローチにより、大規模な有限体を要求することなく、標準的な範囲証明を用いて丸めを検証することが可能になります。

3. ReLUの検証:
   $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$ と定義されるReLU関数は、以下のように検証されます：

   • 範囲証明を用いて、絶対値 $Y = |A|$ が非負であることを証明する。
   • 多項式 $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$ に対するsum-checkプロトコルを用いて、すべての要素について $a_i^2 = y_i^2$ であることを証明する。
   • 最終的な線形結合 $B = (A + Y)/2$ を検証する。

4. 構成（Composition）:
   本フレームワークは、ニューラルネットワークの推論をレイヤーのシーケンスとして扱います。各レイヤー（行列乗算と丸め、またはReLU活性化）は独立して検証されます。あるレイヤーの出力コミットメントが次のレイヤーの入力として機能するため、大規模な中間行列を再送することなく、検証アルゴリズムのモジュール的な構成が可能になります。

主な貢献
本論文は、以下の具体的な貢献を主張しています：

• 統一されたフレームワーク: Range-Arithmeticは、固定小数点丸みとReLUの両方をサポートしながら、$O(n^3)$ のプルーバー複雑性、$O(n^2)$ の検証者複雑性、および $O(\log n)$ の通信複雑度を同時に達成する初めての手法です。
• オーバーヘッドの排除: このアプローチは、ブール回路エンコーディング、（オーバーフローを防ぐための）大規模な有限体、および大規模な事前計算済みルックアップテーブルを必要としません。これらは先行研究で一般的です。
• プリプロセッシング不要: R1CSベースまたは算術回路ベースのアプローチとは異なり、この手法はプリプロセッシングやエンコーディングのオーバーヘッドを必要としません。
• 実用性: オーバーフローを回避するために有限体を拡大する必要がないため、暗号学的なサイズの素数に対して実用的であり続けます。

実験結果
著者らは、線形ニューラルネットワーク、およびMNISTデータセット（6ビットの整数部と8ビットの小数部を使用）を用いて訓練された4層全結合ネットワークのケーススタディにおいて、提案アルゴリズムを評価しました。

• 性能比較: ReLUサポートがなく、フィールド拡大を必要とする最先端の手法 [20] と比較して、Range-Arithmeticはネットワークのレイヤー数が増加するにつれて優れた性能を示しました。
• 指標: 提案手法は、プルーバーと検証者の両方の計算コストを削減し、通信オーバーヘッドを低下させました。
• 詳細: MNISTのケーススタディにおいて、プルーバーの実行時間は約230ミリ秒、検証者の実行時間は約154ミリ秒でした。
• スケーラビリティ: 行列サイズが増大するにつれ、通信コストは対数的に増加しましたが、プルーバーおよび検証者の実行時間は多項式的にスケールしました。

意義と主張
本論文は、Range-Arithmeticが、信頼できない第三者による検証可能なDNN推論において、プルーバーの労力、検証者コスト、通信、および機能の完全性の間で「最もバランスの取れたトレードオフ」を提供すると位置付けています。著者らは、ルックアップベースの手法は純粋なReLU検証においては高速である可能性があるものの、大規模な補助テーブルを必要とするため、リソース制約のある検証者にとって非実用的であると強調しています。Range-Arithmeticは、これらのテーブルを軽量な範囲証明に置き換えることで、分散型MLシステムの特定の制約に対して、より一般的かつ効率的なソリューションを提供します。本研究は、複雑で非算術的なML操作を（再実行することなく）効率的に検証することを可能にすることで、オープンで動的な環境における信頼できる自律的なAIアプリケーションを促進することを目指しています。