対話型証明系

対話型証明系の概念とその影響

対話型証明系（Interactive Proof System）は、2者間のメッセージのやり取りを通じて計算をモデル化する計算理論の枠組みです。ここでの2者は、検証者（Verifier）と証明者（Prover）と呼ばれます。主な目的は、与えられた文字列が特定の形式言語に属しているかどうかを決定することにあります。特に、証明者には無限の計算資源と全能の計算能力が与えられていますが、検証者は限られた計算能力を持つことが特徴です。メッセージのやり取りは、検証者が証明者の提供する証明に納得できるまで続きます。

完全性と健全性の条件

この証明系は、以下の2つの基本的な条件に従うことで成り立っています。

1. 完全性: 文が真である場合、プロトコルに従った検証者は、証明者からの証明に必ず納得します。
2. 健全性: 文が偽の場合、証明者の行動に関係なく、検証者は証明者の証明を受け入れる確率が非常に低い（1より小さい）です。

この条件から、検証者がプロトコルに従わなかった場合は特に問題視されない点に注目が必要です。ここでの重要な観点は、検証者がどのように制限されているか、またはどのような能力を持つかによって、認識される言語の特性が異なることです。

対話型証明系がもたらす影響

対話型証明系は、これまでの計算複雑性の研究において非常に大きな影響を与えています。特に、このフレームワークを用いて定義された複雑性クラスは多岐にわたり、AM（Arthur-Merlin）、MA（Merlin-Arthur）、IP（Interactive Polynomial）、PCP（Probabilistically Checkable Proofs）などのクラスがあります。

NPとそのプロトコル

NP（非決定性多項式時間）の複雑性クラスは、非常にシンプルな形の対話型証明系に基づいて定義できます。この場合、検証者は決定的な多項式時間の機械（Pマシン）で動作します。証明者は、入力を見て無限の計算能力を駆使して解を得て、その結果を多項式長のメッセージとして返します。検証者はその証明を決定的に検証し、妥当であれば受理し、不正確であれば拒絶します。

Arthur-MerlinとMerlin-Arthurプロトコル

1985年にLászló Babaiが発表した「Trading group theory for randomness」により、対話型証明系における対話的な計算の概念が広がりました。Arthur-Merlinプロトコルの検証者は確率的多項式時間の機械、証明者は無限の計算能力を有しています。この構成において、クラスMAは、検証者が常に適切な証拠を受理するわけではなく、より寛大な条件を採用しています。

パブリックおよびプライベートコインプロトコル

パブリックコインプロトコルでは、検証者の乱数が公開され、プライベートコインプロトコルではその選択が非公開です。この違いは証明システムの効率性に関わります。例えばBabaiがMAプロトコルを定義した際、Shafi GoldwasserとSilvio Micaliは対話型証明システムIP[f(n)]を導入しました。これは、メッセージのラウンド数に制限を設けている点が特徴です。

グラフ同型問題と言語の認識

IPの力を示す一例は、グラフ同型問題です。この問題は、同じノード数を持つ2つのグラフが同型であるかどうかを判定するものですが、証明の証拠がノードの対応関係を提示することで解決され、この問題は確実にNPに含まれます。

MIPの登場と新たな可能性

1988年にGoldwasserらが提案したMIP（Multi-prover Interactive Proofs）は、2人以上の証明者を持つ対話型証明系です。各証明者は完全に独立しており、共謀することができないため、検証者が悪意のある証明者から誤った証明を受理するリスクが低くなります。MIPは発展した結果、NEXPTIMEに相当する広範な複雑性クラスにまで拡張されることが分かりました。

まとめ

アディ・シャミアが1992年に証明したIP = PSPACEの結果は、この研究の重要性を一層際立たせます。対話型証明系は計算複雑性理論の奥深さを探求するための強力なツールであり、多くの問題を解決する方法を提供します。そのため、対話型証明系は、理論的な研究だけでなく、実用的な応用の観点からも重要な意義を持っています。

もう一度検索