対話型証明系

対話型証明系（たいわがたしょうめいけい、英: Interactive proof system）は、2者間のメッセージ交換によって計算をモデル化した計算模型であり、計算複雑性理論で使われる。2者とは、検証者と証明者と呼ばれ、与えられた文字列がある形式言語に属するか否かをメッセージのやり取りによって決定するものである。証明者は無限の計算資源を持つ全能の計算能力を持つが、検証者の方は限定的な計算能力を持つ。メッセージのやり取りは、検証者が証明者による証明に納得して正しいと判断するまで続けられる。 対話型証明系は、必ず次のような2つの要求に従う。 * 完全性: 文が真である場合、プロトコルに正しく従う検証者は、プロトコルに正しく従う証明者の証明に納得する。 * 健全性: 文が偽である場合、証明者がプロトコルに正しく従うかどうかに関わらず、プロトコルに正しく従う検証者は証明者の（真であるという）証明には従わない（小さな確率で納得してしまう可能性はある）。 なお、検証者がプロトコルに従わない場合は問題とはされず、常に検証者を信じるという点に注意されたい。 この系の特徴や関連する複雑性クラスが認識する言語の特徴は、検証者がどのように制限されるかに依存し、また検証者にどのような能力を与えるかに依存する。例えば、多くの対話型証明系は検証者の無作為選択能力に大きく依存する。交換されるメッセージの性質、その頻度や内容も重要である。対話型証明系は、それまで単一の機械で定義されてきた複雑性クラスに多大な影響を与えた。対話型証明系を使って定義された主な複雑性クラス（実際には複雑性クラスの階層）としては、AM、MA、、PCP などがある。