はじめに
この記事では論文「Delegating Computation: Interactive Proofs for Muggles」(要約版: [1], 完全版: [2])について解説します。
最初に概要を述べます。次に論文全体を通して必要な前提知識について参考リンクを紹介し、解説を試みます。次に、主張の核となる部分のプロトコルについて解説します。最後に結論を書きます。
概要
多項式時間で解ける問題について、自分のコンピューターではリソースが足りないので他のコンピューターに計算を任せたい時があります。BOINCやSETI@HOMEなどが有名です。この計算と計算結果の検証について、それぞれ時間がかかりますが計算結果の検証の方が実際のタスクの計算よりも早く終わることが望ましいです。現実世界の並列計算機で扱える任意の計算問題に対して、そのような都合の良い検証が可能な、対話的証明方法が存在するというのが論文の主張です。
PCPの部分的に情報を開示する証明に従って、Sum-Checkプロトコル [16]を用います。
サーキット同士の関係を明示することなく、遠く離れたサーキット同士での関係を部分的な情報の開示によって証明することができます。[16] には本論文と同様の主張を別の方向からアプローチするヒントが書かれています。
前提知識
L-一様(L-uniform) とは
Lを決定性チューリングマシンで対数規模の領域(メモリ)を使って解くことができる決定問題の集合とする。
回路計算量の表現として、一般にチューリング機械とは異なり入力長ごとに異なる回路を用意しなければならない。入力長がn \in N
であるような回路の集合\{ C_n \}
に対して、リソースの制限されたチューリング機械Mを考える。Mは空間計算量として対数領域を消費する(L)。また、Mはn \in N
に対してC_n
の具体的な記述を出力する。このとき回路の集合\{ C_n \}
はL-一様(L-uniform)であるという。
NCとは
並列計算機で効率的に解けるとされる問題のクラス[7]。
公開乱数対話証明とは
[8]を参照。
検証者のコイン投げが公開されている(使用する乱数が証明者に知られている)タイプの対話型証明プロトコル。
対話型PCP(Interactive probabilistically checkable proof)とは
[9]にあるPCPの解説では「証明内の数ビットを知るだけである一定の確率での正しさが言える」とあるが、この証明内で得る情報に加えて、証明者と対話プロトコルで得られる情報も使うのが対話型PCP[10]。
MIPとは
多重証明者対話証明(Multi prover interactive proofs) のこと。
[11] を参照。
疑似証明 (argument)とは
普通の証明(proof)との違いは、疑似証明 (argument)における健全性が計算量的仮定に基づいているため、証明者Pの計算能力が確率的多項式時間チューリングマシンに制限されている点である。
通常の証明(proof)では無限の計算能力を持つ証明者Pの提出した証明に対しても正誤判定を行う必要がある。
polylogとは
計算量のオーダーの表記として、あるkに対して\text{polylog}(n) = (\text{log}(n))^k
と定義する。
Low-degree extension (LDE)とは
大雑把に言うと、ある関数fの入力のサイズを大きくしたgを作り、元のfの定義域の値を入力として与えた時の値はfとgで一致するようなとき、gはfのLDEであるという。
読む上で知っておくと便利な記法や知識について列挙する。
- 記法:
f \mid_A : A \rightarrow F
は関数の定義域の制限[12]を表す。 - 算術回路 (Arithmetic circuit complexity) [13][14]
- リード・マラー符号[15]
LDEの作り方の注意点
完全版[2]では2.3節にLDEの説明が載っている。以下で定義と記号を説明しておく。
\mathbb{H}
を\mathbb{GF}[2]
の拡大体とする。また、\mathbb{F}
を\mathbb{H}
の拡大体とする。m\in\mathbb{N}
とする。以下でk要素からなる文字列(w_0, w_1, ..., w_{k-1}) \in \mathbb{F}^k
の\mathbb{F}, \mathbb{H}, m, k \leq |\mathbb{H}^m|
に関するLDEを定義する。\alpha: \mathbb{H}^m \rightarrow \{0,1, ..., |\mathbb{H}^m| - 1\}
を適当な、効率的に計算可能な1:1対応関数とする。ここでは\alpha
として\mathbb{H}^m
の辞書的順序を採用する。文字列(w_0, w_1, ..., w_{k-1})
は以下の定義を用いるとW: \mathbb{H}^m \rightarrow \mathbb{F}
という関数とみなせる。
W(z) := \begin{cases} w_{\alpha(z)} & \text{if}\ \alpha(z) \leq k-1 \\ 0 & \text{o.w.} \end{cases}
W
に対して、W
を以下の\tilde{W} : \mathbb{F}^m \rightarrow \mathbb{F}
に変換する一意な拡張が存在する。ただし、ここで\tilde{W} \mid_{\mathbb{H}^m} \equiv W
である。
\tilde{W}(t_1, ..., t_m) = \sum_{i=0}^{k-1} \tilde{\beta_i}(t_1, ..., t_m) \cdot w_i
ただし、各の\tilde{\beta_i} : \mathbb{F}^m \rightarrow \mathbb{F}
はm変数多項式であり、パラメータとして\mathbb{H}, \mathbb{F}, m
にのみ依存し、w
から独立している。また\tilde{\beta_i}
のサイズは\text{poly}(|\mathbb{H}|, m)
であり、各変数に対して最大次数は|\mathbb{H}|-1
である。このような関数\tilde{W}
はw = (w_0, w_1, ..., w_{k-1})
のLDEであるといい、\text{LDE}_{\mathbb{H}, \mathbb{F}, m}(w)
で表される。
これを満たす具体的なLDEの構成を考える。例としてi=0の時\tilde{ \beta_0 } (t_1,...,t_m)
を考えてみる(とりあえず計算量は考えない)。具体的に、m = 2, \mathbb{H} = F_{2^2}, \mathbb{F} = F_{2^4}, k = 2^4
としておく。\tilde{\beta}
がw
に依存してはいけないということから、w
の係数は1つだけ1になり、残りは全て0になる必要がある。つまり、例えば拡張前の定義域に関して\tilde{\beta_0}(0, 0) = 1
とすると(t_1, t_2) \neq (0, 0)
に対して\tilde{\beta_0}(t_1, t_2) = 0
である必要がある。この時、拡張後の定義域\mathbb{F}
として入れる値のうち、拡張前の定義域に入っていないものについては何も考える必要がないことに注意する。
サムチェックプロトコルとは
有限体\mathbb{F}
を固定し、その部分集合H \subseteq \mathbb{F}
を考える。サムチェックプロトコルでは(必ずしも効率的とは限らない)証明者がm変数多項式f: \mathbb{F}^m \rightarrow \mathbb{F}
を与えられる。各変数の最大次数dはd\ll|\mathbb{F}|
を満たす。証明者は定数\beta \in \mathbb{F}
に対して以下を検証者に向けて証明する必要がある。
\sum_{z\in H^m} f(z) = \beta
検証者は\beta
を与えられ、f
に対してオラクルでしかアクセスできない。検証者は実行時間とオラクルへの問い合わせの両方で効率的である必要がある。このプロトコルを(P_{SC}(f), V^f_{SC}(\beta))
と書く。
ナイーブに考えるとオラクル問い合わせは|H|^m
回必要で、実行時間はfの実行時間tとしてt*|H|^m
かかるが、確率md/|\mathbb{F}|
で検証者が騙されうるプロトコルで、オラクル問い合わせが1回、実行時間が\text{poly}(|H|)
となるアルゴリズムが存在する。
検証者によるf
の評価回数が1回だけであることが後々重要になる。
詳しくは [16] を参照。
必要最小限のプロトコル
完全版[2]の方の論文で必要最小限のプロトコル(3. The Bare-Bones Protocol for Delegating Computation)を説明する章があるので、それを解説する。
算術回路Cは一様の幅Sと深さdを持つ。Cにおける深さi-1のレイヤを考える(レイヤはdが入力、0が出力になる)。このレイヤでの算術回路の演算結果(多項式)の入出力を考える。証明者はC(x) = 0を証明したい。全てのレイヤにおいて入出力が正しければ、回路全体の入出力も正しい。
よって各レイヤにおいて入出力が正しいことを検証者は検証したい。
各レイヤにおける出力は、一つ前のレイヤの算術回路の加算と乗算を使った合成になっている。従って、これを証明しようとするとナイーブな方法では加算と乗算のとりうるパターンを全て列挙する必要がある。しかし、実際にはとりうるパターンは様々な入力に対して関数を適用した和になっており、LDEとサムチェックプロトコルを使うことで大幅に簡略化された証明に変換できる。
サムチェックプロトコルを使った結果として、深さi-1における入出力の正しさの証明は深さiにおける入出力の正しさの証明に帰着できる。これを繰り返すと最終的にはCに対する入力が一致するかどうかをチェックする証明に帰着される。
以下、\tilde{V}_i
はサーキットの深さiにおける層のゲート(それぞれ入出力がある)を体で表現したものを拡張した関数とする。また、\tilde{\text{add}_i}, \tilde{\text{mult}_i}
は同階層にあるゲートが共通の入力を持っているかを判定するための関数を拡張したものとする。
算術回路Cと入力xに対して検証者は C(x) = 0を検証したいとする。回路Cのレイヤがd層になっていると仮定すると、i番目(1≦i≦d)の層で検証者が\tilde{V}_{i-1}(z_{i-1}) = r_{i-1}
を証明するタスクを\tilde{V}_{i}(z_{i}) = r_{i}
を証明するタスクに帰着させることができる。ここでz_i
はプロトコルによって決定される乱数である。d番目の層では検証者が自分自身で\tilde{V}_{d}(z_{d}) = r_{d}
であることを確認する。以下で詳細を説明する。
それぞれのz\in \mathbb{F}^m
に対して
\tilde{V}_{i-1}(z) = \sum_{p\in\mathbb{H}^m} \tilde{\beta}(z,p)\cdot\tilde{V}_{i-1}(p)
\tilde{\beta}: \mathbb{F}^m \times \mathbb{F}^m \rightarrow \mathbb{F}
は\text{poly}(|\mathbb{H}|,m)
のサイズで次数はそれぞれの変数に対して最大でも|\mathbb{H}|-1
になり、\text{poly}(|\mathbb{H}|,m)
以下の時間で計算ができる。
全ての p\in\mathbb{H}^m
に対して
\tilde{V}_{i-1}(p) = \sum_{{\omega_1, \omega_2}\in\mathbb{H}^m} \tilde{\text{add}_i}(p, \omega_1, \omega_2)\cdot(\tilde{V}_{i}( \omega_2) +\tilde{V}_{i}( \omega_2) ) + \tilde{\text{mult}_i}(p, \omega_1, \omega_2)\cdot \tilde{V}_{i}( \omega_2) \cdot \tilde{V}_{i}( \omega_2)
が成立する。従って、それぞれのz\in \mathbb{F}^m
に対して
\tilde{V}_{i-1}(z) = \sum_{{p, \omega_1, \omega_2}\in\mathbb{H}^m} \tilde{\beta}(z,p)\cdot ( \tilde{\text{add}_i}(p, \omega_1, \omega_2)\cdot(\tilde{V}_{i}( \omega_2) +\tilde{V}_{i}( \omega_2) ) + \tilde{\text{mult}_i}(p, \omega_1, \omega_2)\cdot \tilde{V}_{i}( \omega_2) \cdot \tilde{V}_{i}( \omega_2) )
それぞれの z\in \mathbb{F}^m
に対してf_z : ( \mathbb{F}^m)^3 \rightarrow \mathbb{F}
を以下で定義される関数とする。
f_z(p, \omega_1, \omega_2) := \tilde{\beta}(z,p)\cdot ( \tilde{\text{add}_i}(p, \omega_1, \omega_2)\cdot(\tilde{V}_{i}( \omega_2) +\tilde{V}_{i}( \omega_2) ) + \tilde{\text{mult}_i}(p, \omega_1, \omega_2)\cdot \tilde{V}_{i}( \omega_2) \cdot \tilde{V}_{i}( \omega_2) )
\tilde{\text{add}}_i
と \tilde{\text{mult}}_i
と\tilde{V}_i
の定義から、f_z
は3m変数の多項式でサイズが\text{poly}(S)
以下かつ、それぞれの次数に関して最大次数が \delta + |\mathbb{H}|-1 \leq 2\delta
になる。
それぞれのz\in \mathbb{F}^m
に対して
\tilde{V}_{i-1}(z) = \sum_{{p, \omega_1, \omega_2}\in\mathbb{H}^m} f_z(p, \omega_1, \omega_2)
になる。従って、\tilde{V}_{i-1}(z_{i-1}) = r_{i-1}
を証明することは
r_{i-1} = \sum_{{p, \omega_1, \omega_2}\in\mathbb{H}^m} f_{z_{i-1}}(p, \omega_1, \omega_2)
を証明するのと等しい。これはサムチェックプロトコルを実行することによって行われる。
サムチェックプロトコルを使う場合でも検証者は最終的にf_{z_{i-1}}(\cdot)
を1回だけ最後に計算する必要がある。\tilde{\text{add}_i}, \tilde{\text{mult}_i}
はオラクルでアクセスできると仮定するが、\tilde{V}_{i}( \omega_1), \tilde{V}_{i}( \omega_2)
に関しては検証者自身が(重い)計算をする必要がある。しかし、このプロトコルでは 検証者ではなく 証明者がこの値v_1, v_2
を計算して検証者に送る。
その際、証明者は嘘をついて正しくない値を送信することができるのだが、もしこの値が正しいということを(後々)何らかの手段で証明できるならば、以下が言えることになる。
「
\tilde{V}_{i-1}(z_{i-1}) = r_{i-1}
を効率的に証明するタスク」は「\tilde{V}_{i}( \omega_1) = v_1
と\tilde{V}_{i}( \omega_2) = v_2
を効率的に証明するタスク」に置き換えられる。
よって、「\tilde{V}_{i}( \omega_1) = v_1
と\tilde{V}_{i}( \omega_2) = v_2
を効率的に証明するタスク」を「\tilde{V}_{i}(z_{i}) = r_{i}
を効率的に証明するタスク」に変換することができれば、「\tilde{V}_{i-1}(z_{i-1}) = r_{i-1}
を効率的に証明するタスク」は「\tilde{V}_{i}(z_{i}) = r_{i}
を効率的に証明するタスク」に変換することができる。
そのような性質を持つz_i, r_i
を新たに以下のように定義する。
-
t_1, t_2 \in \mathbb{F}
を検証者と証明者の間で共有された点であるとする。\gamma: \mathbb{F} \rightarrow \mathbb{F}^m
をi \in \{1, 2\}, \gamma(t_i) = \omega_i
を満たす一意に定まる1次の多項式(直線)とする。 -
証明者は
\tilde{V}_{i} \circ \gamma : \mathbb{F} \rightarrow \mathbb{F}
を検証者に送信する。 -
関数
f: \mathbb{F} \rightarrow \mathbb{F}
(これはf = \tilde{V}_{i} \circ \gamma
であるはず)を証明者から受け取った検証者はfが高々m\cdot(|\mathbb{H}|-1)
次の多項式であることを確認して、f(t_1) = v_1
かつf(t_2) = v_2
であることを検証する。もしこれらの検証が成功するならば、検証者は乱数t\in \mathbb{F}
を選択して 証明者に送る。 -
証明者は 次のi+1フェーズで
z_i, r_i
を新たに以下のように定義してプロトコルを進める。z_i := \gamma(t)
r_i := f(t)
必要最小限のプロトコルでは 上位のレイヤで加算と乗算をどのように組み合わせているかを判定する部分をオラクルに置き換えているため、その部分の計算量を考慮する必要がないが、実際のプロトコルではCの性質を使ってその部分の計算量も十分小さいことが言える。
解説
以上は完全版[2]の方の論文で必要最小限のプロトコル(3. The Bare-Bones Protocol for Delegating Computation)までの説明です。以上を使った結論と要約版における応用を以下に示します。
1.1. 効率的な対話証明系
以下が主要な結論です。
定理1.
入力長n
に対して、深さd(n)
、回路数S(n)
、\text{log}(S(n))
-一様であるような論理回路の集合を考える。この集合が受理する言語L
に対して、L
には絶対完全性を満たし、1/2の健全性を満たすような公開乱数対話証明が存在する。
この公開乱数対話証明における証明者の計算時間は\text{poly}(S(n))
である。検証者の計算時間は(n + d(n)) \cdot \text{polylog}(S(n))
である。通信複雑性はd(n) \cdot \text{polylog}(S(n))
である。
健全性、完全性の定義は[17]参照。
証明者の計算時間が\text{poly}(S(n))
になるのは サムチェックプロトコルの制約による。
検証者の計算時間が (n + d(n)) \cdot \text{polylog}(S(n))
になるのは サムチェックプロトコルの制約による。
通信複雑性が d(n) \cdot \text{polylog}(S(n))
になるのは、 サムチェックプロトコルの各フェーズの通信複雑性が \text{polylog}(S(n))
であり、dフェーズまである事による。
系1.
L-一様かつNC
に属する言語L
を考える(L-一様のLは複雑性クラスのLで言語L
とは無関係)。ここで、言語L
はO(\text{log}(n))
-一様であるような論理回路の集合であり、回路数S(n) = \text{poly}(n)
かつd(n) = \text{polylog}(n)
とする。L
には絶対完全性を満たし、1/2の健全性を満たすような公開乱数対話証明が存在する。
この公開乱数対話証明における証明者の計算時間は\text{poly}(n)
である。検証者の計算時間はn \cdot \text{polylog}(n)
である。通信複雑性は\text{polylog}(n)
である。
1.2. 検証者の計算量を犠牲にした非対話証明系への拡張
1.1. の結果を使っている。機械的に変換できるプロトコルが存在する。
1.3. 検証者が対数空間計算量である公開乱数対話証明
1.1. の結果を使う。Pに属する問題には検証者が対数空間計算量で実行できる対話証明が存在する。
1.4. L-一様でないケース
プロトコルをオンライン・オフラインで分けて、オンラインの部分だけ見れば同様の結果が成立する。
1.5. NP言語ゼロ知識対話証明の通信複雑性の改善
公開乱数対話証明から対話型ゼロ知識証明への変換は既に存在するが、その変換に1.1.を応用する。
1.6. 対話型PCPへの応用
対話型PCP, PCA(確率検査疑似証明)において検証者の計算量を小さくする応用。
結論(と感想)
サムチェックプロトコルが肝で、他はおまけです。そもそもビットコインのフルノードの検証を対話的な証明を使うことで簡略化できないかというモチベーションで調べましたが、フルノード検証の計算量はブロック数に対して線形に増えるので直接の応用はできないと考えられます。
フルノード検証の高速化に関する話題は [3][4][5][6]を参照してください。
巨大な回路を作って実行し、検証者がその中での矛盾点を探すという手法はbitvm[18]とも似ている印象を受けました。
参考文献
[1] 要約版: https://www.microsoft.com/en-us/research/wp-content/uploads/2008/01/GoldwasserKR08a.pdf
[2] 完全版: https://eccc.weizmann.ac.il/report/2017/108/download/
[3] Incrementally Verifiable Computation:効率的に証明をつなげる https://tech.hashport.io/4123/
[4] 第三者を信頼せずに段階的検証可能計算(IVC)を実現するHaloの解説 https://tech.hashport.io/3248/
[5] Proof of Necessary Work: 再帰的SNARKを使ったビットコインの全ブロック検証 https://tech.hashport.io/3778/
[6] ブロックチェーンシステムのためのプログラミング言語Cairoについて https://tech.hashport.io/3594/
[7] https://ja.wikipedia.org/wiki/NC_(%E8%A8%88%E7%AE%97%E8%A4%87%E9%9B%91%E6%80%A7%E7%90%86%E8%AB%96)
[8] https://ja.wikipedia.org/wiki/Arthur%E2%80%93Merlin%E3%83%97%E3%83%AD%E3%83%88%E3%82%B3%E3%83%AB
[9] https://tech.fressets.com/1810/
[10] https://zkproof.org/2020/10/15/information-theoretic-proof-systems-part-ii/
[11] https://ja.wikipedia.org/wiki/%E5%AF%BE%E8%A9%B1%E5%9E%8B%E8%A8%BC%E6%98%8E%E7%B3%BB#MIP
[12] http://onionmarktwo.hatenablog.com/entry/2017/09/09/191731
[13] https://en.wikipedia.org/wiki/Arithmetic_circuit_complexity
[14] https://qiita.com/nrnrk/items/b9c915ba69ead4879875
[15] https://ja.wikipedia.org/wiki/%E3%83%AA%E3%83%BC%E3%83%89%E3%83%BB%E3%83%9E%E3%83%A9%E3%83%BC%E7%AC%A6%E5%8F%B7
[16] https://zkproof.org/2020/03/16/sum-checkprotocol/
[17] https://ja.wikipedia.org/wiki/Arthur%E2%80%93Merlin%E3%83%97%E3%83%AD%E3%83%88%E3%82%B3%E3%83%AB
[18] https://bitvm.org/bitvm.pdf