입증 복잡성

논리와 이론 컴퓨터 과학, 특히 증명 이론과 계산 복잡성 이론에서 증명 복잡성은 진술을 증명하거나 반박하는 데 필요한 계산 자원을 이해하고 분석하는 것을 목표로 하는 분야다.입증 복잡성에 대한 연구는 주로 다양한 명제 증명 시스템에서 증명 길이의 하한과 상한을 증명하는 것과 관련이 있다.예를 들어, 입증 복잡성의 주요 난제들 중 하나는 일반적인 명제 미적분학인 Frege 시스템이 모든 tautology의 다항식 크기 증거를 인정하지 않는다는 것을 보여준다.여기서 증명의 크기는 단순히 그 안에 있는 기호의 수일 뿐이며, 증명한 tautology의 크기에서 다항식이라면 증명의 크기가 다항식이라고 한다.

증명 복잡성에 대한 체계적인 연구는 계산 복잡성의 관점에서 명제 증명 시스템의 기본 정의를 제공한 스티븐 쿡과 로버트 레크쇼(1979)의 연구로 시작되었다.특히 Cook and Leckhow는 모든 토폴로지에 대해 다항식 크기 증명을 허용하는 제안형 검증 시스템이 NP=CONP와 동등하기 때문에, 더 강하고 강력한 제안형 증명 시스템의 입증 크기가 coNP(따라서 P와 NP를 분리하기 위한 단계로 볼 수 있다고 보았다.

현대의 증명 복잡성 연구는 계산 복잡성, 알고리즘 및 수학의 많은 영역에서 아이디어와 방법을 끌어낸다.많은 중요한 알고리즘과 알고리즘 기법이 특정 증명 시스템의 증명 검색 알고리즘으로 주조될 수 있기 때문에, 이러한 시스템에서 입증 크기의 하한을 증명하는 것은 해당 알고리즘의 런타임 하한을 의미한다.이것은 입증 복잡성을 SAT 해결과 같은 더 많은 적용 영역과 연결시킨다.

수학적 논리학은 또한 명제적인 증명 크기를 연구하는 틀의 역할을 할 수 있다.제1차 이론과 특히 경계가 있는 산술이라는 이름으로 나오는 페아노 산술의 약한 단편들은 명제 증명 시스템의 균일한 버전 역할을 하며, 다양한 수준의 실현 가능한 추론 측면에서 짧은 명제적 증명들을 해석할 수 있는 추가적인 배경을 제공한다.

프루프론트

명제 증명 시스템은 두 개의 입력을 가진 증명 검증 알고리즘 P(A,x)로 주어진다.만약 P가 쌍(A,x)을 받아들인다면, 우리는 x가 A의 P-proof라고 말한다.P는 다항식 시간에 실행해야 하며, 더욱이 A가 tautology일 경우에만 P-proof가 있다는 것을 유지하여야 한다.

명제 증명 시스템의 예로는 시퀀스 미적분학, 분해능, 절단면 및 프레지 시스템이 있다.ZFC와 같은 강력한 수학 이론은 제안 증명 시스템도 유도한다: ZFC의 제안적 해석에서 tutology$$$$ology {\$displaystyle \tau }$의 $증거$는 공식화된 문장 ' statement {\$displaystyle \tau}$은 tutology$'$의 ZFC 입증이다.

다항식 크기 증명 및 NP 대 coNP 문제

증명 복잡성은 일반적으로 주어진 상호연구를 위해 시스템에서 가능한 최소 크기의 증명이라는 관점에서 증명 시스템의 효율성을 측정한다.증명(존중 공식)의 크기는 증명(존중 공식)을 나타내기 위해 필요한 기호의 수입니다.명제 증명 시스템 P는 크기가 $n{\displaystyle }$ ${\displaystyle n}$인 모든 tautology에 P-proof (${\displaystyle n{}^{}+}$ c ) c $displaystyle (n+c)^{c}$일 정도로$$ ${\displaystyle {일정}^{}}$한 c$$ {\$displaystyle c}$이 있는 경우 다항식적으로 경계된다$.$ 증명 복잡성의 중심 문제는 tautology가 다항성인 경우 이해해야 한다.형식적으로.

문제(NP 대 coNP)

다항식 명제 증명 시스템이 존재하는가?

Cook and Leckhow(1979)는 NP=coNP인 경우에만 다항 경계 교정 시스템이 존재한다고 관찰했다.따라서, 특정 증명 시스템이 다항식 크기 증명서를 인정하지 않는다는 것을 증명하는 것은 NP와 coNP(따라서 P와 NP)를 분리하기 위한 부분적인 진전으로 볼 수 있다.^[1]

인증 시스템 간의 최적화 및 시뮬레이션

증명 복잡성은 시뮬레이션 개념을 사용하는 증명 시스템의 강도를 비교한다.검증 시스템 P는 tautology의 Q-proof를 부여한 다항식 시간 함수가 있으면 증명 시스템 Q를 시뮬레이션한다.P가 Q를 시뮬레이션하고 Q가 P를 시뮬레이션한다면, 증명 시스템 P와 Q는 p-등가성이 있다.또한 시뮬레이션에 대한 더 약한 개념도 있다: 증명 시스템 P는 증명 시스템 Q를 시뮬레이션한다. 즉, 검증 시스템 P는 tutology A의 모든 Q-proof x에 대해, y, y의 길이가 최대 p( x )인 A의 P-proof y가 있다.

예를 들어, 연속 미적분은 (매) 프레지 시스템과 p-등가하다.^[2]

증명 시스템은 다른 모든 증명 시스템을 p-모사할 경우 p-최적적이며, 다른 모든 증명 시스템을 모사할 경우 최적이다.그러한 증명 시스템이 존재하는지는 공개적인 문제다.

문제(최적성)

p-최적 또는 최적의 제안 증명 시스템이 있는가?

모든 명제 증명 시스템 P는 P의 건전성을 가정하는 공리로 확장된 Extended Frege에 의해 시뮬레이션될 수 있다.^[3]최적(p-최적) 증명 시스템의 존재는 NE=coNE(존중 E=NE)라는 가정으로부터 따르는 것으로 알려져 있다.^[4]

많은 취약한 입증 시스템의 경우 특정 강력한 시스템을 시뮬레이션하지 않는 것으로 알려져 있다(아래 참조).그러나 시뮬레이션의 개념이 완화된다면 그 문제는 여전히 열려있다.예를 들어, 해상도가 다항식적으로 Extended Frege를 효과적으로 시뮬레이션하는지 여부는 공개된다.^[5]

증거 검색의 자동화

증명 복잡성에 있어서 중요한 질문은 증명 시스템에서 증거를 찾는 복잡성을 이해하는 것이다.

문제(자동화성)

Resolution 또는 Frege 시스템과 같은 표준 인증 시스템에서 증명을 검색하는 효율적인 알고리즘이 있는가?

이 문제는 자동성(자동화성이라고도 함)^[6]의 개념으로 공식화할 수 있다.

A proof system P is automatable if there is an algorithm that given a tautology ${\displaystyle \tau }$ outputs a P-proof of ${\displaystyle \tau }$ in time polynomial in the size of ${\displaystyle \tau }$ and the length of the shortest P-proof of ${\displaystyle \tau }$. Note that if a proof system is not polynomia경계선을 그리면, 여전히 자동화할 수 있다.증명 시스템 P는 증명 시스템 R과 tautology$\tau {\displaystyle }$ {\$displaystyle \tau}$을(를) 제공하는 알고리즘이 있는 경우 약하게 자동화할 수 있으며, $\tau {\displaystyle }$ ${\displaystyle \tau}$의 크기 및 $\tau {\displaystyle }$ ${\displaystyle \tau$의 최단 P-p 길이인 $\tau {\displaystyle }$ ${\$proof를 시간$$ 다항목으로 출력한다.

많은 관심 증명 시스템은 자동화할 수 없는 것으로 여겨진다.그러나 현재는 조건부 음성 결과만 알려져 있다.

• Krajichek와 Pudlahk(1998)는 RSA가 P/poly에 대해 안전하지 않는 한 Extended Frege는 약하게 자동화할 수 없다는 것을 증명했다.^[7]
• Bonet, Pitassi, Raz(2000년)는 Diffie–가 아니면 $T{\displaystyle }$ ${\displaystyle {}^{}}$ ${\displaystyle {0\mathrm{}}^{}}$ ${\$ -Frege$$ 시스템이 약하게 자동화할 수 없다는 것을 증명했다.헬만 체계는 P/폴리에게 안전하지 않다.^[8]이것은 보넷, 도밍고, 가발다, 마키엘, 피타시(2004)에 의해 확장되었다. 그는 디피-가 아닌 한 최소 2개의 일정한 깊이의 프레지 시스템은 약하게 자동화할 수 없다는 것을 증명했다.Helman 계획은 부차적인 시간에 일하는 통일되지 않은 적들에 대해 안전하지 않다.^[9]
• 알레흐노비치와 라즈보로프(2008)는 FPT=W[P]^[10]가 아니면 나무와 같은 결의와 결의안은 자동화할 수 없다는 것을 증명했다.이것은 갈레시와 로리아(2010)에 의해 연장되었는데, 그는 Nullstellensatz와 다항식 미적분은 고정 매개변수 계층 구조가 붕괴되지 않는 한 자동화할 수 없다는 것을 증명했다.^[11]메르츠, 피타시, 위(2019년)는 지수 시간 가설을 가정할 때 특정 준폴리놈 시간에도 나무와 같은 결의와 결의는 자동화할 수 없다는 것을 증명했다.^[12]
• 아세리아스와 뮐러(2019)는 P=NP가 아니면 해상도가 자동화할 수 없다는 것을 증명했다.^[13]This was extended by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (2020) to NP-hardness of automating Nullstellensatz, Polynomial Calculus, Sherali–Adams;^[14] by Göös, Koroth, Mertz and Pitassi (2020) to NP-hardness of automating Cutting Planes;^[15] and by Garlík (2020) to NP-hardness of automating k-DNF Resolution.^[16]

결의안의 약한 자동성이 표준 복잡성-이론적 경도 가정을 깨뜨릴지는 알 수 없다.

긍정적인 측면에서는

• Beame과 Pitassi(1996)는 나무와 같은 분해능은 준-폴리놈 시간에서 자동화할 수 있고 분해능은 약하게 하위존재 시간에서 작은 폭의 공식에서 자동화할 수 있다는 것을 보여주었다.^[17][18]

경계 산술

명제 증명 시스템은 상위 질서의 이론의 통일되지 않은 등가물로 해석될 수 있다.등가성은 흔히 경계 산술 이론의 맥락에서 연구된다.For example, the Extended Frege system corresponds to Cook's theory ${\displaystyle \mathrm {PV} _{1}}$ formalizing polynomial-time reasoning and the Frege system corresponds to the theory ${\displaystyle \mathrm {VNC} ^{1}}$ formalizing ${\displaystyle {\mathsf {NC}}^{1}}$ reasoning.

이 서신은 스테판 쿡(1975)에 의해 소개되었는데, 그는 CNP 이론의 formally ${\displaystyle {}_{}^{}}$ ${\displaystyle {b\mathrm{}}_{}^{}}$ ${\$ $\$$Pi_{1}^{b}$ 공식에$$ 대해 ${\displaystyle {}_{}}$으로 $\pi {\displaystyle {\mathrm{}}_{}^{}}$$$1 b {\$displaystyle \mathrmatmatrm{1}{$1}}}}는 Extended Frege의 다항 크기 교정본이 있는 tautional tautorology 시퀀스로 번역된다$$.또한 Extended Frege는 가장 약한 시스템이다. 다른 증명 시스템 P가 이 속성을 가지고 있다면 P는 Extended Frege를 시뮬레이션한다.^[19]

제프 패리스와 알렉스 윌키(1985)가 제시한 2차 진술서와 명제 공식 사이의 대체 번역은 프레지나 일정한 깊이 프레지 같은 익스텐드 프리지의 서브시스템을 포착하는 데 더욱 실용적이었다.^[20][21]

위에서 언급한 서신에서는 이론상의 증명들이 해당 증명 체계에서 일련의 짧은 증거들로 번역된다고 말하지만, 반대되는 함축성의 형태는 또한 그러하다.시스템 P에 해당하는 이론 T의 적절한 모델을 구성함으로써 증명 시스템 P에서 증명 크기에 대한 하한을 도출할 수 있다.이것은 아제이의 방법이라고 알려진 접근방식인 모델 이데아 구조물을 통해 복잡성 하한을 증명할 수 있다.^[22]

SAT 해결사

명제 증명 시스템은 tautology를 인식하기 위한 비결정론적 알고리즘으로 해석될 수 있다.따라서 증명 시스템 P에 대한 초다항식 하한을 증명하는 것은 P에 기초한 SAT에 대한 다항식 시간 알고리즘의 존재를 배제한다.예를 들어, 불만족스러운 인스턴스에 대한 DPLL 알고리즘의 실행은 나무와 같은 분해능 반박에 해당한다.따라서 나무와 같은 분해능(아래 참조)에 대한 지수 하한은 SAT에 대한 효율적인 DPLL 알고리즘의 존재를 배제한다.마찬가지로 지수 분해능 하한은 CDCL 알고리즘과 같은 분해능에 기반한 SAT 해결사가 SAT를 효율적으로 해결할 수 없다는 것을 의미한다(최악의 경우).

하한

명제적 증거의 길이에 대한 하한을 증명하는 것은 일반적으로 매우 어렵다.그럼에도 불구하고, 약한 증명 시스템의 하한을 증명하는 몇 가지 방법이 발견되었다.

• 하켄(1985)은 결의안과 비둘기 구멍 원리에 대한 기하급수적인 하한을 증명했다.^[23]
• 아제타이(1988)는 일정한 깊이의 프레게 제도와 비둘기홀 원리에 대한 초폴리노믹 하한선을 증명했다.^[24]이것은 크라지체크, 푸들라크, 우즈와^[25] 피타시, 베임, 임팔리아조에 의해 기하급수적인 하한선으로 강화되었다.^[26]Ajtai의 하한은 무작위 제한 방법을 사용하며, 또한 회로 복잡성에서 AC⁰ 하한을 도출하는 데 사용되었다.
• Krajichek(1994)은 ^[27]실현 가능한 보간 방법을 공식화하고 나중에 결의안 및 기타 증명 시스템에 대해 새로운 하한을 도출하는 방법을 사용했다.^[28]
• Pudlahk(1997)는 실현 가능한 보간법을 통해 비행기를 절단하는 지수적인 하한을 증명했다.^[29]
• 벤 사손과 위그더슨(1999)은 결의안 수정 폭의 하한을 줄이기 위해 결의안 수정 크기의 하한을 줄이는 증명 방법을 제공했는데, 하켄의 하한에 대한 많은 일반화를 포착했다.^[18]

Frege 시스템에 대한 비경쟁 하한을 도출하는 것은 오랫동안 열려 있는 문제다.

실현 가능한 보간

Consider a tautology of the form ${\displaystyle A(x,y)\rightarrow B(y,z)}$. The tautology is true for every choice of ${\displaystyle y}$, and after fixing ${\displaystyle y}$ the evaluation of ${\displaystyle A}$ and ${\displaystyle B}$ are independent because they are defined on di변수들의 집합들 집합This means that it is possible to define an interpolant circuit ${\displaystyle C(y)}$, such that both ${\displaystyle A(x,y)\rightarrow C(y)}$ and ${\displaystyle C(y)\rightarrow B(y,z)}$ hold.보간 회로는 $A{\displaystyle (}$ ${\displaystyle x}$, ${\displaystyle y}$) ${\displaystyle A(x,y)}$이(가) 거짓인지$$ 또는 $B{\displaystyle (y}$, ${\displaystyle z}$) ${\displaystyle B(y,z)}$이(가) 참인지$$ 여부를 $y{\displaystyle }$ ${\displaysty y}$만 고려하여 결정한다$.$보간 회로의 특성은 임의적일 수 있다.Nevertheless, it is possible to use a proof of the initial tautology ${\displaystyle A(x,y)\rightarrow B(y,z)}$ as a hint on how to construct ${\displaystyle C}$. A proof systems P is said to have feasible interpolation if the interpolant ${\displaystyle C(y)}$ is efficiently computable fromP의 $tutology{\displaystyle }$ A${\displaystyle }$( ${\displaystyle x}$, y${\displaystyle }$)${\displaystyle }$→ B${\displaystyle }$( ${\displaystyle y}$, ${\displaystyle z}$) ${\displaystyle A(x,y)\오른쪽$ 화살표 $B(y,z)}$에 대한 모든 증거.증빙의 길이에 관해서 효율을 측정한다: 긴 증빙을 위해 보간물을 계산하는 것이 더 쉽기 때문에, 이 성질은 증명 시스템의 강도에 있어서 반-모노톤인 것처럼 보인다.

다음 세 가지 진술은 동시에 사실일 수 없다: ($a{\displaystyle }$) A${\displaystyle }$( ${\displaystyle x}$, y${\displaystyle }$)${\displaystyle }$→ ${\displaystyle B}$( ${\displaystyle y}$, ${\displaystyle z}$) ${\displaystyle A (x,y)\오른쪽$ 화살표 B$(y,z)}}$은 일부 증명 시스템에 짧은 증거를 가지고$$ 있다. (b) 그러한 증명 시스템은 실현 가능한 보간성을 가지고 있다. (c) 보간 회로는 계산상적으로 어려운 문제를 해결한다.(a)와 (b)는 (c)와 모순되는 작은 보간 회로가 있음을 암시하는 것이 분명하다.이러한 관계를 통해 교정 길이 상한을 계산에서 하한으로 변환하고 효율적인 보간 알고리즘을 교정 길이에 대한 하한으로 변환할 수 있다.

결의안 및 절단면과 같은 일부 증명 시스템은 실현 가능한 보간 또는 그 변형을 인정한다.^[28][29]

실현 가능한 보간법은 자동화의 약한 형태라고 볼 수 있다.실제로 Extended Frege와 같은 많은 증명 시스템의 경우 실현 가능한 보간법은 약한 자동성과 동등하다.Specifically, many proof systems P are able to prove their own soundness, which is a tautology ${\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}$ stating that `if ${\displaystyle \pi }$ is a P-proof of a formula ${\displaystyle \phi (x)}$ then ${\displaystyle \phi (x)}$ holds'.여기서 $\pi {\displaystyle }$ ,${\displaystyle \varphi }$, x ${\displaystyle \pi ,\phi ,x}$은(는) 자유 변수에 의해 인코딩된다.Moreover, it is possible to generate P-proofs of ${\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}$ in polynomial-time given the length of ${\displaystyle \pi }$ and ${\displaystyle \phi }$. Therefore, an efficient interpolant resulting from short P-proofs of soundness of P would decide whether a given 공식 $\varphi {\displaystyle }$ ${\displaystyle \pi }$은(는) 짧은 P-proof $proof{\displaystyle }$ ${\displaystyle \pi }$을(를) 인정하고$$ 있다$.$ 이러한 보간제는 P가 약하게 자동화할 수 있음을 증명하는 증명 시스템 R을 정의하는 데 사용될 수 있다.^[30]반면에 입증 시스템 P의 약한 자동화성은 P가 실현 가능한 보간법을 인정한다는 것을 의미한다.단, 증명시스템 P가 자체의 건전성을 효율적으로 입증하지 못하면 실현 가능한 보간을 인정하더라도 약하게 자동화할 수 없을 수 있다.

많은 비신뢰성 결과는 각 시스템에서 실현 가능한 보간법에 대한 증거를 제공한다.

• Krajichek와 Pudlahk(1998)는 RSA가 P/poly에 대해 안전하지 않은 한 Extended Frege가 실현 가능한 보간법을 인정하지 않는다는 것을 증명했다.^[31]
• Bonet, Pitassi, Raz(2000년)는 Diffie–가 아니면 T ${\displaystyle {}^{}}$ ${\displaystyle {0\mathrm{}}^{}}$ ${\$ -Frege$$ 시스템이 실현 가능한 보간법을 인정하지 않는다는 것을 증명했다.헬만 체계는 P/폴리에게 안전하지 않다.^[32]
• 보넷, 도밍고, 가발다, 마키엘, 피타시(2004)는 디피-가 아닌 한 일정한 깊이의 프레지 시스템이 실현 가능한 보간법을 인정하지 않는다는 것을 증명했다.Helman 계획은 부차적인 시간에 일하는 통일되지 않은 적들에 대해 안전하지 않다.^[33]

비표준 로직

증명서의 크기를 비교하는 아이디어는 증거를 생성하는 자동화된 추론 절차에 사용될 수 있다.일부 연구는 명제적 비분류적 로직, 특히 직관적, 모달적, 비단조적 로직의 증명 크기에 대해 수행되었다.

Hrubesh(2007–2009)는 일부 모달 로직과 직관 논리에서 실현 가능한 단조로운 보간 버전을 사용하여 확장 프리지 시스템에서 증명 크기의 지수 하한을 입증했다.^[34][35][36]

참고 항목

• 계산 복잡성
• 회로 복잡성
• 통신 복잡성
• 수학적 논리학
• 증명 이론
• 복잡도 클래스
• NP(복잡성)
• coNP

참조

추가 읽기

• Beame, Paul; Pitassi, Toniann (1998), "Propositional proof complexity: past, present, and future", Bulletin of the European Association for Theoretical Computer Science, 65: 66–89, MR 1650939, ECCC TR98-067
• Cook, Stephen; Nguyen, Phuong (2010), Logical Foundations of Proof Complexity, Perspectives in Logic, Cambridge: Cambridge University Press, doi:10.1017/CBO9780511676277, ISBN 978-0-521-51729-4, MR 2589550 (2008년부터 적용됨)
• Krajíček, Jan (1995), Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press
• Krajíček, Jan (2005), "Proof complexity" (PDF), in Laptev, A. (ed.), Proceedings of the 4th European Congress of Mathematics, Zürich: European Mathematical Society, pp. 221–231, MR 2185746
• Krajichek, Jan, Proof Complexity, Cambridge University Press, 2019.
• Pudlák, Pavel (1998), "The lengths of proofs", in Buss, S. R. (ed.), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, Amsterdam: North-Holland, pp. 547–637, doi:10.1016/S0049-237X(98)80023-2, MR 1640332

외부 링크

• 증명 복잡성
• 증명 복잡성 메일 목록.