대화형 증명 시스템

대화형 증명 프로토콜의 일반적인 표현. 계산 복잡도 이론에서 **대화형 증명 시스템**(Interactive proof system)은 증명자와 검증자라는 두 주체 간의 메시지 교환으로 컴퓨테이션을 모델링하는 추상 기계이다. 이들은 주어진 문자열이 형식 언어에 속하는지 여부를 확인하기 위해 메시지를 교환한다. 증명자는 무제한의 계산 자원을 가지고 있지만 신뢰할 수 없는 반면, 검증자는 제한된 계산 능력을 가지고 있지만 항상 정직하다고 가정한다. 검증자가 문제에 대한 답을 얻고 그것이 정확하다고 "확신"할 때까지 검증자와 증명자 사이에 메시지가 전송된다. 모든 대화형 증명 시스템에는 두 가지 요구 사항이 있다. * **완전성**: 명제가 참이면 정직한 증명자(즉, 프로토콜을 올바르게 따르는 증명자)는 정직한 검증자에게 명제가 참임을 확신시킬 수 있다. * **건전성**: 명제가 거짓이면 프로토콜을 따르지 않더라도 어떤 증명자도 정직한 검증자에게 명제가 참이라고 확신시킬 수 없다. 다만, 일부 작은 확률의 경우는 예외이다. 시스템의 특정 특성과 그에 따라 인식할 수 있는 언어의 복잡도 종류는 검증자에 부과되는 제약 조건과 부여되는 능력에 따라 달라진다. 예를 들어, 대부분의 대화형 증명 시스템은 검증자의 임의 선택 능력에 결정적으로 의존한다. 또한 교환되는 메시지의 특성(개수 및 내용)에도 의존한다. 대화형 증명 시스템은 하나의 기계만을 사용하여 정의된 전통적인 복잡도 종류에 중요한 영향을 미치는 것으로 밝혀졌다. 대화형 증명 시스템을 설명하는 주요 복잡도 종류는 **AM** 및 **IP**이다.
# 배경
모든 대화형 증명 시스템은 문자열 L의 형식 언어를 정의한다. 증명 시스템의 **건전성**은 증명자가 작은 확률을 제외하고는 잘못된 명제 y \not\in L에 대해 검증자를 승인하게 할 수 없다는 속성을 나타낸다. 이 확률의 상한은 증명 시스템의 **건전성 오류**라고 한다. 더 공식적으로는, 모든 증명자 (\tilde{\mathcal{P)와 모든 y \not\in L에 대해 다음이 성립한다. : \Pr[(\perp,(\text{accept}))\gets (\tilde{\mathcal{P)(y) \leftrightarrow (\mathcal{V})(y)] < \epsilon. 여기서 \epsilon \ll 1 이다. 건전성 오류가 검증자의 잠재적 실행 시간의 다항식 분수(즉, \epsilon\leq1/\mathrm{poly}(|y|))로 제한되는 한, 검증자의 실행 시간에 비해 건전성 오류가 미미한 함수가 될 때까지 건전성을 증폭시키는 것은 항상 가능하다. 이는 증명을 반복하고 모든 증명이 검증될 때만 수용함으로써 달성된다. \ell번 반복 후, 건전성 오류 \epsilon는 \epsilon^\ell로 감소할 것이다..
# 대화형 증명의 종류

## NP
NP 복잡도 종류는 매우 간단한 증명 시스템으로 볼 수 있다. 이 시스템에서 검증자는 결정적, 다항 시간 기계(P 기계)이다. 프로토콜은 다음과 같다. * 증명자는 입력을 보고 무제한의 능력을 사용하여 해를 계산하고 다항식 크기의 증명 인증서를 반환한다. * 검증자는 결정적 다항 시간 내에 인증서가 유효한지 확인한다. 유효하면 승인하고, 그렇지 않으면 거부한다. 유효한 증명 인증서가 존재하는 경우, 증명자는 항상 해당 인증서를 제공하여 검증자를 승인하게 할 수 있다. 그러나 유효한 증명 인증서가 없는 경우, 입력은 해당 언어에 없으며, 아무리 악의적인 증명자라도 검증자를 달리 설득할 수 없다. 왜냐하면 어떤 증명 인증서도 거부될 것이기 때문이다.
## 아서-멀린 및 멀린-아서 프로토콜
아서-멀린 프로토콜 NP가 상호작용을 사용하는 것으로 볼 수 있지만, 1985년이 되어서야 두 독립적인 연구 그룹에 의해 (복잡도 이론의 맥락에서) 상호작용을 통한 컴퓨테이션 개념이 고안되었다. 라슬로 바바이의 "Trading group theory for randomness"가 발표된 한 접근 방식은László Babai. Trading group theory for randomness. Proceedings of the Seventeenth Annual Symposium on the Theory of Computing, ACM. 1985. 아서-멀린(**AM**) 클래스 계층을 정의했다. 이 발표에서 아서(검증자)는 확률적, 다항 시간 기계인 반면, 멀린(증명자)은 무제한 자원을 가지고 있다. 특히 **MA** 클래스는 위에서 언급한 NP 상호작용의 간단한 일반화이며, 검증자는 결정론적 대신 확률적이다. 또한, 검증자가 항상 유효한 인증서를 수락하고 유효하지 않은 인증서를 거부하도록 요구하는 대신, 더 관대하다. * **완전성:** 문자열이 언어에 속한다면, 증명자는 검증자가 최소 2/3의 확률로 수락할 수 있는 인증서를 제공할 수 있어야 한다(검증자의 무작위 선택에 따라 다름). * **건전성:** 문자열이 언어에 속하지 않는다면, 아무리 악의적인 증명자라도 1/3을 초과하는 확률로 검증자를 설득하여 문자열을 수락하게 할 수 없다. 이 기계는 일반적인 NP 상호작용 프로토콜보다 잠재적으로 더 강력하며, 인증서는 검증하기에 덜 실용적이지 않다. 왜냐하면 **BPP** 알고리즘은 실용적인 컴퓨테이션을 추상화하는 것으로 간주되기 때문이다(BPP 참조).
## 공개 코인 프로토콜 대 비공개 코인 프로토콜
공개 코인 프로토콜에서는 검증자가 수행한 임의 선택이 공개된다. 비공개 코인 프로토콜에서는 비공개로 유지된다. 바바이가 **MA**에 대한 자신의 증명 시스템을 정의한 같은 회의에서, 샤피 골드와서, 실비오 미칼리 및 찰스 래코프는doi=10.1137/0218012 Extended abstract date=2006-06-23 대화형 증명 시스템 **IP**[f(n)]을 정의하는 논문을 발표했다. 이것은 **MA** 프로토콜과 동일한 기계를 사용하지만, 입력 크기 n에 대해 f(n) 라운드가 허용된다. 각 라운드에서 검증자는 계산을 수행하고 증명자에게 메시지를 전달하며, 증명자는 계산을 수행하고 검증자에게 정보를 다시 전달한다. 마지막에 검증자는 결정을 내려야 한다. 예를 들어, **IP**[3] 프로토콜에서 시퀀스는 VPVPVPV이며, V는 검증자 턴이고 P는 증명자 턴이다. 아서-멀린 프로토콜에서 바바이는 f(n) 라운드를 허용하는 유사한 클래스 **AM**[f(n)]을 정의했지만, 그는 기계에 한 가지 추가 조건을 부여했다. 즉, 검증자는 계산에 사용하는 모든 임의 비트를 증명자에게 보여주어야 한다. 그 결과, 증명자가 사용한 임의 비트를 알면 증명자가 검증자가 하는 모든 것을 시뮬레이션할 수 있을 만큼 강력하기 때문에 검증자는 증명자로부터 아무것도 "숨길" 수 없다. 이것을 공개 코인 프로토콜이라고 하는데, 임의 비트("코인 던지기")가 두 기계 모두에게 보이기 때문이다. **IP** 접근 방식은 대조적으로 비공개 코인 프로토콜이라고 한다. 공개 코인의 본질적인 문제는 증명자가 언어에 없는 문자열을 검증자가 수락하도록 악의적으로 설득하려 할 때, 검증자가 내부 상태를 숨길 수 있다면 증명자의 계획을 좌절시킬 수 있을 것처럼 보인다는 것이다. 이것이 **IP** 증명 시스템을 정의하는 주요 동기였다. 1986년, 골드와서와 시프서는Shafi Goldwasser and Michael Sipser. Private coins versus public coins in interactive proof systems date=2005-01-27. Proceedings of ACM STOC'86, pp. 58–68. 1986. 아마도 놀랍게도, 검증자가 코인 던지기를 증명자로부터 숨기는 능력이 두 라운드만 더 추가된 아서-멀린 공개 코인 프로토콜이 모든 동일한 언어를 인식할 수 있다는 점에서 결국 거의 도움이 되지 않는다는 것을 보여주었다. 그 결과 공개 코인 프로토콜과 비공개 코인 프로토콜은 거의 동등하다. 사실, 바바이가 1988년에 보여주듯이, 모든 상수 k에 대해 **AM**[k] = **AM**이므로, **IP**[k]는 **AM**에 비해 이점이 없다.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. 이러한 클래스의 위력을 보여주기 위해, 하나의 그래프의 정점을 재배열하여 다른 그래프와 동일하게 만들 수 있는지 여부를 결정하는 문제인 그래프 동형 문제를 고려해보자. 이 문제는 **NP**에 속하는데, 증명 인증서가 그래프를 동일하게 만드는 순열이기 때문이다. 그래프 동형 문제의 여집합, 즉 **NP**에 속하는 것으로 알려지지 않은 co-**NP** 문제는 **AM** 알고리즘을 가지고 있으며, 이를 이해하는 가장 좋은 방법은 비공개 코인 알고리즘을 통하는 것이다.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.
## IP
IP (복잡도) 비공개 코인은 유용하지 않을 수 있지만, 더 많은 라운드 상호 작용은 유용하다. 확률적 검증 기계와 전능한 증명자가 다항식 개수의 라운드 동안 상호 작용하도록 허용하면, **IP**라고 불리는 문제 클래스를 얻는다. 1992년, 아디 샤미르는 복잡도 이론의 핵심 결과 중 하나에서 **IP**가 다항 공간에서 일반적인 결정론적 튜링 기계로 풀 수 있는 문제 클래스인 **PSPACE**와 같음을 밝혀냈다.Adi Shamir. IP = PSPACE. Journal of the ACM, volume 39, issue 4, p.869–877. October 1992.
## QIP
QIP (복잡도) 시스템의 요소가 양자 컴퓨팅을 사용할 수 있도록 허용하면, 해당 시스템은 **양자 대화형 증명 시스템**이라고 불리며, 해당 복잡도 종류는 **QIP**라고 불린다.year=2010 일련의 결과들은 2010년 **QIP** = **PSPACE**라는 획기적인 발견으로 이어졌다.pages=573–582s2cid = 34380788
## 영지식
영지식 증명 대화형 증명 시스템은 **NP**에 속하지 않는다고 여겨지는 문제들을 해결할 수 있을 뿐만 아니라, 일방향함수의 존재에 대한 가정 하에, 증명자는 검증자에게 해에 대한 정보를 전혀 주지 않고도 해를 확신시킬 수 있다. 이는 검증자가 전체 해를 신뢰할 수 없을 때 중요하다. 처음에는 검증자가 인증서를 보지 못했는데도 해가 있다고 확신할 수 있다는 것이 불가능해 보이지만, 영지식 증명이라고 알려진 이러한 증명은 실제로 **NP**의 모든 문제에 대해 존재한다고 여겨지며 암호학에서 가치가 있다. 영지식 증명은 골드와서, 미칼리, 래코프가 **IP**에 관한 1985년 원본 논문에서 특정 수론 언어에 대해 처음 언급했다. 그러나 그들의 위력은 오데드 골드라이히, 실비오 미칼리, 아비 위그더슨에 의해 **NP** 전체에 대해 시연되었고, 이는 러셀 임파글리아초와 모티 융에 의해 **IP** 전체로 처음 확장되었다.Russell Impagliazzo, Moti Yung: Direct Minimum-Knowledge Computations. CRYPTO 1987: 40-51
## MIP
**IP** 설계자들의 한 가지 목표는 가능한 가장 강력한 대화형 증명 시스템을 만드는 것이었으며, 처음에는 검증자를 더 강력하게 만들지 않고는(그렇게 하면 비실용적이게 됨) 더 강력하게 만들 수 없을 것처럼 보였다. 골드와서 등은 1988년 "Multi prover interactive proofs: How to remove intractability assumptions"에서 이를 극복했다. 이 논문은 두 명의 독립적인 증명자가 있는 **MIP**라는 **IP** 변형을 정의한다.M. Ben-or, Shafi Goldwasser, J. Kilian, and A. Wigderson. [http://theory.lcs.mit.edu/~cis/pubs/shafi/1988-stoc-bgkw.pdf Multi prover interactive proofs: How to remove intractability assumptions url=https://web.archive.org/web/20070417142744/http://theory.lcs.mit.edu/~cis/pubs/shafi/1988-stoc-bgkw.pdf. Proceedings of the 20th ACM Symposium on Theory of Computing, pp. 113–121. 1988. 두 증명자는 검증자가 메시지를 보내기 시작한 후에는 통신할 수 없다. 범인과 그의 공범이 따로 심문받을 때 거짓말을 하는지 알아내기 더 쉬운 것처럼, 다른 증명자와 다시 확인할 수 있다면 악의적인 증명자가 검증자를 언어에 없는 문자열을 수락하도록 속이려 하는 것을 감지하는 것이 훨씬 쉽다. 실제로, 이것은 매우 유용하여 바바이, 포트노우, 룬드는 **MIP**가 비결정론적 기계가 지수 시간 내에 해결할 수 있는 모든 문제의 클래스인 **NEXPTIME**과 같다는 것을 보여줄 수 있었다. 이는 매우 큰 클래스이다.year=1991 NEXPTIME은 PSPACE를 포함하며, PSPACE를 엄격하게 포함하는 것으로 여겨진다. 두 명 이상의 상수를 추가해도 더 많은 언어를 인식할 수 있게 되지는 않는다. 이 결과는 이 정리의 "축소판"으로 볼 수 있는 유명한 PCP 정리의 길을 열었다. **MIP**는 또한 **IP**가 가정해야 하는 일방향 함수 가정 없이도 **NP**의 모든 언어에 대한 영지식 증명을 설명할 수 있는 유용한 속성을 가지고 있다. 이것은 증명 가능한 깨지지 않는 암호화 알고리즘 설계에 영향을 미친다. 더욱이, **MIP** 프로토콜은 **IP**의 모든 언어를 상수 라운드 내에서 인식할 수 있으며, 세 번째 증명자가 추가되면 상수 라운드 내에서 **NEXPTIME**의 모든 언어를 인식할 수 있어 **IP**보다 그 위력을 다시 보여준다. 어떤 상수 k에 대해서도 k명의 증명자와 다항식 개수의 라운드를 가진 MIP 시스템이 단 두 명의 증명자와 상수 개수의 라운드를 가진 동등한 시스템으로 변환될 수 있다는 것이 알려져 있다.archive-url=https://web.archive.org/web/20100713035025/http://groups.csail.mit.edu/cis/pubs/shafi/1988-stoc-bgkw.pdf
## PCP
PCP (복잡도) **IP**의 설계자들이 바바이의 대화형 증명 시스템의 일반화를 고려한 반면, 다른 이들은 제약을 고려했다. 매우 유용한 대화형 증명 시스템은 **PCP**(f(n), g(n))이며, 이는 아서가 f(n)개의 임의 비트만 사용하고 멀린이 보낸 증명 인증서의 g(n)개의 비트만 검사할 수 있는 (본질적으로 임의 접근을 사용하는) **MA**의 제약이다. 다양한 **PCP** 클래스에 대한 여러 가지 쉽게 증명할 수 있는 결과들이 있다. 랜덤성이 없지만 인증서에 접근할 수 있는 다항 시간 기계의 클래스인 1=\mathsf{PCP}(0,\mathsf{poly})는 단순히 **NP**이다. 다항식 개수의 랜덤 비트에 접근할 수 있는 다항 시간 기계의 클래스인 1=\mathsf{PCP}(\mathsf{poly},0)는 **co-RP**이다. 아로라와 사프라의 첫 번째 주요 결과는 1= \mathsf{PCP}(\log, \log) = \mathsf{NP}라는 것이었다. 다시 말해, **NP** 프로토콜에서 검증자가 증명 인증서의 O(\log n) 비트만 선택하여 볼 수 있도록 제약되어도, 사용할 수 있는 O(\log n) 개의 랜덤 비트가 있는 한 아무런 차이가 없다.Sanjeev Arora and Shmuel Safra. Probabilistic Checking of Proofs: A New Characterization of NP. Journal of the ACM, volume 45, issue 1, pp. 70–122. January 1998. 더욱이, PCP 정리는 증명 접근 횟수를 상수까지 줄일 수 있다고 주장한다. 즉, 1=\mathsf{NP} = \mathsf{PCP}(\log, O(1))이다.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, pp. 13–22. 1992. 이들은 **NP**의 이러한 유용한 특성화를 사용하여 P = NP가 아닌 한 특정 NP-완전 문제의 최적화 버전에 대한 근사 알고리즘이 존재하지 않음을 증명했다. 이러한 문제들은 현재 근사 난해라고 알려진 분야에서 연구되고 있다.
# 교재
* Arora, Sanjeev; Barak, Boaz, "Complexity Theory: A Modern Approach", Cambridge University Press, March 2009. * url = https://archive.org/details/introductiontoth00sips Section 10.4: Interactive Proof Systems, pp. 354-366\. * isbn = 978-0-201-53082-7 Section 19.2: Games against nature and interactive protocols, pp. 469-480\.