対話型証明系
対話型証明系（たいわがたしょうめいけい、英: Interactive proof system）は、2者間のメッセージ交換によって計算をモデル化した計算模型であり、計算複雑性理論で使われる。2者とは、検証者と証明者と呼ばれ、与えられた文字列がある形式言語に属するか否かをメッセージのやり取りによって決定するものである。証明者は無限の計算資源を持つ全能の計算能力を持つが、検証者の方は限定的な計算能力を持つ。メッセージのやり取りは、検証者が証明者による証明に納得して正しいと判断するまで続けられる。
対話型証明系は、必ず次のような2つの要求に従う。
- 完全性: 文が真である場合、プロトコルに正しく従う検証者は、プロトコルに正しく従う証明者の証明に納得する。
- 健全性: 文が偽である場合、証明者がプロトコルに正しく従うかどうかに関わらず、プロトコルに正しく従う検証者は証明者の（真であるという）証明には従わない（小さな確率で納得してしまう可能性はある）。
なお、検証者がプロトコルに従わない場合は問題とはされず、常に検証者を信じるという点に注意されたい。
この系の特徴や関連する複雑性クラスが認識する言語の特徴は、検証者がどのように制限されるかに依存し、また検証者にどのような能力を与えるかに依存する。例えば、多くの対話型証明系は検証者の無作為選択能力に大きく依存する。交換されるメッセージの性質、その頻度や内容も重要である。対話型証明系は、それまで単一の機械で定義されてきた複雑性クラスに多大な影響を与えた。対話型証明系を使って定義された主な複雑性クラス（実際には複雑性クラスの階層）としては、AM、MA、IP、PCP などがある。
NP
[編集]よく知られている複雑性クラス NP は非常に単純な対話型証明系で定式化できる。この場合、検証者は決定的な多項式時間の機械である（つまり、Pマシン）。プロトコルは次の通り。
- 証明者は入力を見て、その無限の計算能力を使って解を計算し、証明の証拠となる多項式長のメッセージを返す。
- 検証者はその証拠を決定的な多項式時間で検証する。妥当であれば、それを受理し、そうでなければ拒絶する。
妥当な証明の証拠がある場合、証明者は常に検証者が受理するような証拠を与えることができる。妥当な証明の証拠がない場合、入力が言語に属していないということであり、いかなる証拠も受理されないので、悪意のある証明者であったとしても検証者を納得させられない。
Arthur-Merlin プロトコルと Merlin-Arthur プロトコル
[編集]NP をより対話的に定式化することもできるが、そのような対話による計算の概念は1985年になって登場した[1]。それは、László Babai の発表した "Trading group theory for randomness" という論文で定義された Arthur-Merlin（AM）クラス階層によるものである。その中で Arthur（検証者）は確率的多項式時間機械であり、Merlin（証明者）は無限の計算資源を持つ機械である。
クラス MA は、上述の NP の対話の単純な一般化であり、検証者は確率的ではなく決定的である。また、検証者が常に妥当な証拠を受理して妥当でないものを拒絶するのではなく、以下のようにもっと寛大な方針を採用する。
- 完全性: 文字列が言語に属する場合、証明者は検証者が受理するような証拠を最低でも 2/3 の確率で与えることができる（検証者の無作為選択に依存する）。
- 健全性: 文字列が言語に属さない場合、悪意の有無に関わらず、証明者が検証者が受理するような証拠を与えることができる確率は 1/3 未満である。
これは、通常のNPの対話プロトコルよりも強力であり、BPPのアルゴリズムが実用的であるように、このような確率的な証拠であっても検証に値する。Babai の提唱した他のクラスについては後述する。
公開硬貨と秘密硬貨
[編集]Babai がMAの証明系を定義した直後、シャフィ・ゴールドワッサーらは IP[f(n)] の対話型証明系を定義した論文のドラフト版を発表した。これは MA プロトコルと同様のマシン構成だが、入力長 n に対して f(n) 回のラウンドが許されていた。各ラウンドで、検証者は計算を行って証明者にメッセージを渡し、証明者も計算を行って検証者にメッセージを返す。そして全ラウンドの最後に検証者は決定しなければならない。例えば、IP[3] プロトコルなら、メッセージの並びは VPVPVPV となる。ここで、V は検証者のターン、P は証明者のターンである。
Arthur-Merlin プロトコルでは、Babai は同様のクラスを AM[f(n)] と定義した。これも f(n) 回のラウンドを許すものだが、彼はマシンに条件を1つ追加した。検証者は証明者に対して計算に使用したランダムビット列を全て提示しなければならないというものである。結果として検証者は証明者に対して何も隠せないことになる。なぜなら証明者の計算能力は無限なので、ランダムビット列さえ分かれば、検証者の計算を全てシミュレート可能だからである。ランダムビット列（硬貨投げ）が両方のマシンから見えるため、これを「公開硬貨」プロトコルと呼ぶ。一方 IP の手法を対照的に「秘密硬貨」プロトコルと呼ぶ。
公開硬貨の基本的な問題は次のようなものである。証明者が言語に属さない文字列を検証者に悪意を持って受理させようとした場合、検証者が内部状態を見せないようにするためにして証明者の計画を妨害する可能性がある。この問題があるため、IP 証明系が定義された。
1986年、ゴールドワッサーとシプサーは驚くべき結果を示した。すなわち、IP で認識できる言語は、Arthur-Merlin 公開硬貨プロトコルでも2ラウンド追加するだけで認識可能であり、結果としてほとんど差がないことがわかったのである。つまり、公開硬貨プロトコルも秘密硬貨プロトコルもほぼ同じであることが示された[2]。実際、Babai は 1988年、任意の定数 k について AM[k] が IP[k] と比較して劣らないことを示した[3]。
IP
[編集]秘密硬貨は意味がないかもしれないが、確率的検証機械と全能証明機械が多項式回数のやりとりをすることで、クラス IP に属する問題を解くことができる。
クラス IP の能力を示すため、グラフ同型問題を考えてみよう。これはノード数の等しい2つのグラフがあったとき、それらが同じ形であるかを判定する問題である。証明の証拠はノードの対応関係の組合せで示されるので、この問題は NP に属する。もちろん NP は MA に包含されるので、この問題は IP にも属する。また、アディ・シャミアはグラフ同型問題の補問題を解く IP アルゴリズムを発見した。co-NP 問題は NP に属するか不明であり、一般には属さないと考えられている[4]。
そのような機械は NP にあるとは信じられていない多くの問題を解けるだけでなく、一方向性関数が存在することを前提として、検証者に解法についての情報を与えずに多くの問題の解法があるかどうかを決定することができる。これらは、検証者に完全な解法が任せられない場合に重要となる。一見して、検証者が解法を知らないのに解法があるかどうかを判断するのは不可能に思われるが、NP に属するあらゆる問題にはいわゆるゼロ知識証明があると信じられており、暗号理論にとって重要である。ゼロ知識証明はゴールドワッサーらの IP に関する論文で提唱された概念だが、その能力の範囲を明らかにしたのは Oded Goldreich であった[5]。
この強力なマシンの前では、多くの問題が簡単に解かれるようであった。1992年、アディ・シャミアは計算複雑性理論の重要な成果となる事実、IP = PSPACE を証明した[6]。PSPACE は決定性チューリング機械で多項式領域を使って解ける問題のクラスである。確率的対話プロトコルと古典的な決定性機械の間のこの強い関係は、対話型証明系の能力と限界の概念を与え、2つの分野の重要な繋がりを確立した。
MIP
[編集]IP 設計者の目標は最も強力な対話型証明系の構築であり、当初それ以上に強力にするには検証者をさらに強力にする必要があり、現実的でないと思われていた。ゴールドワッサーらは 1988年、"Multi prover interactive proofs[...]" という論文でこれを打ち破り、IP の新たなバージョン MIP を定義した。これは証明者が独立して2つ存在する証明系である[7]。
2つの証明者は、検証者がそれらにメッセージを送り始めたら、相互の通信はできなくなる。証明者は別々の部屋に入れられているようなもので、共謀して検証者を騙すことはできない。従って、どちらかが悪意を持って検証者を騙そうとしてもその検出が容易となる。
実際、Babai、Fortnow、Lund の3人は IP = PSPACE であることから MIP = NEXPTIME を導出した。これは、非決定性チューリング機械で「指数関数時間」で解ける問題の集合であり、非常に大きなクラスである[8]。証明者を2つより多くしても、さらに言語が認識できるようにはならない。この結果に触発されて後述する PCP が設計された。PCP はスケールダウンしたバージョンであり、NP に関する対話型証明系である。
NPに属する各言語がゼロ知識証明を持つことを説明するに際して、IP では一方向性関数の存在を仮定する必要があったが、MIP ではそれが不要となる。これは、解読不能な暗号アルゴリズムの設計と関係がある[7]。さらに、MIP プロトコルは IP に属する全言語を定数回のラウンドだけで認識でき、3つめの証明者を追加すると NEXPTIME に属する全言語を定数回のラウンドで認識できる。
PCP
[編集]IP の設計者らは Babai の対話型証明系の一般化を意図していたが、逆に制限を加えることを検討した者もいる。その中でも最も価値の高いものとして、PCP(f(n), g(n)) がある。これは MA に制限を加え、Arthur は f(n) 個までのランダムビットだけを利用可能とし、Merlin から送られてくる証拠のうち g(n) ビットだけを調べることができるようにしたものである（調べるビット列の位置は基本的にランダムアクセス）。Sanjeev Arora と Shmul Safra が設計したものであり、PCP の背景には、証明文字列の完全な知識と無作為性のトレードオフを行っても、全体としての能力はあまり低下しないという洞察があった。
PCP クラス群に関していくつかの容易に証明可能な事実がある。PCP(0,poly)（無作為性なし）は、単なる NP である。PCP(poly,0)（証明結果を見ない）は、単なる co-RP である。Arora と Safra の最初の重要な成果は PCP(log, log) = NP を示したことである。これを言い換えると、NP プロトコルの検証者が証拠のうちの log n ビットだけを調べ、log n 個のランダムビットを使うと、普通の NP プロトコルと差が生じないのである[9]。
それだけではない。Arora と Safra はランダムビット数とアクセスビット数を同時に少なくしても意味がないことを知っていたが、彼らは一方だけを小さくできると信じていた。Arora らは最終的にこれをPCP定理としてまとめた。これは、証明結果へのアクセスを定数にまで低減させることができることを示したものである。すなわち、NP = PCP(log, O(1)) である[10]。彼らはこの NP の性質を使って、P = NP でない限り、一部のNP完全問題の最適化版に近似アルゴリズムが存在しないことを証明した。
脚注
[編集]- ^ László Babai. Trading group theory for randomness. Proceedings of the Seventeenth Annual Symposium on the Theory of Computing, ACM. 1985.
- ^ Shafi Goldwasser, Silvio Micali, and Charles Rackoff. The Knowledge complexity of interactive proof-systems. Proceedings of 17th Symposium on the Theory of Computation, Providence, Rhode Island. 1985. Extended abstract
- ^ László Babai and Shlomo Moran. Arthur-Merlin games: a randomized proof system, and a hierarchy of complexity classes. Journal of Computer and System Sciences, 36: p.254-276. 1988.
- ^ Shafi Goldwasser and Michael Sipser. Private coins versus public coins in interactive proof systems. Proceedings of ACM STOC'86, p.58-68. 1986.
- ^ O. Goldreich, S. Micali, A. Wigderson. Proofs that yield nothing but their validity. Journal of the ACM, volume 38, issue 3, p.690-728. July 1991.
- ^ Adi Shamir. IP = PSPACE. Journal of the ACM, volume 39, issue 4, p.869-877. October 1992.
- ^ a b M. Ben-or, Shafi Goldwasser, J. Kilian, and A. Wigderson. Multi prover interactive proofs: How to remove intractability assumptions. Proceedings of the 20th ACM Symposium on Theory of Computing, p.113-121. 1988.
- ^ László Babai, L. Fortnow, and C. Lund. Non-deterministic exponential time has two-prover interactive protocols. Computational Complexity, volume 1, p.3-40. 1991.
- ^ Sanjeev Arora and Shmuel Safra. Probabilistic Checking of Proofs: A New Characterization of NP. Journal of the ACM, volume 45, issue 1, p.70-122. January 1998.
- ^ Sanjeev Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof Verification and the Hardness of Approximation Problems. Proceedings of the 33rd IEEE Symposium on Foundations of Computer Science, p.13-22. 1992.
参考文献
[編集]- Michael Sipser (1997年). Introduction to the Theory of Computation. PWS Publishing. ISBN 0-534-94728-X Section 10.4: Interactive Proof Systems, pp.354–366.
- Christos Papadimitriou (1993年). Computational Complexity (1st edition ed.). Addison Wesley. ISBN 0-201-53082-1 Section 19.2: Games against nature and interactive protocols, pp.469–480.
外部リンク
[編集]- Complexity Zoo:
- Larry Gonick. "Proof Positive?". 対話型証明系についての漫画
