보완
사실 검토 — 작은 수정 후 가능
2026-10-07 에 이 글에 적힌 사실(인용한 정리·결과·추측·장벽 서술)을 원 논문·서베이와 대조한 검토입니다. 아이디어가 옳은지가 아니라 사실이 정확한지와, 알려진 결과와 이 글의 제안·판단이 문장에서 갈려 있는지를 봤습니다.
판정: 작은 수정 후 가능
인용 정리와 저자는 대부분 정확하다. 고칠 것은 (1) IPS 부분 체계 하한을 VP 대 VNP 성과처럼 쓴 곳, (2) 「자연 증명 장벽의 증명 복잡도 판본」 설명이 원 결과와 다르게 요약된 곳, (3) 진단·장벽 판단을 사실처럼 쓴 곳이다.
확인한 사실
| 주장 | 사실 여부 | 근거 |
|---|---|---|
| Cook–Reckhow: 모든 명제 증명 체계 초다항 하한 ⇒ NP ≠ coNP ⇒ P ≠ NP | 맞음(실제로는 ⇔) — J. Symbolic Logic 44(1) 1979 | Cook–Reckhow 1979 |
| Resolution 지수 하한, Haken(1985) | 맞음 — 비둘기집 원리, TCS 39 1985 | Haken 1985 |
| AC0-Frege 하한: Ajtai, Pitassi–Beame–Impagliazzo, Krajíček–Pudlák–Woods | 맞음 — Ajtai(FOCS 1988, 초다항), PBI(Comput. Complexity 1993)·KPW(Random Struct. Alg. 1995) 지수 | Proof complexity (Wikipedia) |
| AC0[p]-Frege 앞에서 30년 넘게 정체 | 맞음 — 1990년대 초부터 미해결(Res(⊕) 등 하위 체계 부분 진전만 있음) | 위와 같음 |
| 대응 회로 모델 AC0[p] 하한은 Razborov–Smolensky | 맞음 — Razborov(1987, MAJ ∉ AC0[2]), Smolensky(STOC 1987) | Smolensky 1987 |
| 병목은 이식 원리의 부재 | 해석 — 분야의 통념에 가깝지만 정리가 아님. 핵심 정리 칸에 단정문으로 있음 | — |
| 강한 체계에서 보간이 암호 가정하 실패(Krajíček–Pudlák 계열) | 맞음 — Krajíček–Pudlák 1998(Extended Frege, RSA), Bonet–Pitassi–Raz 2000(Frege·TC0-Frege), Bonet–Domingo–Gavaldà–Maciel–Pitassi 2004(AC0-Frege, Diffie–Hellman 강한 가정) — 따라서 AC0[p]-Frege 에도 보간이 실패 | — |
| ABRW·Krajíček 의 증명 복잡도 생성기, NW 생성기 기반 식 | 맞음 — Alekhnovich–Ben-Sasson–Razborov–Wigderson(FOCS 2000/SICOMP 2004), Krajíček(2001·2004), Razborov(Annals 2015, NW 생성기) | — |
| 비둘기집·Tseitin 은 카운팅 체계에서 쉬워질 수 있음 | 맞음(완곡 표현) — mod 2 Tseitin 은 AC0[2]-Frege 에서 쉬움 | — |
| Res(lin)·Res(mod p) 같은 약한 중간 체계 부분 결과 | 맞음 — Raz–Tzameret(2008) Res(lin), Itsykson–Sokolov 트리형 Res(⊕) 하한, 이후 정규·제한 깊이 Res(⊕) 하한(2024~). 일반 Res(⊕) 하한은 미해결 | — |
| roABP-IPS·다중선형 IPS 하한(FSTW 계열) | 맞음 — Forbes–Shpilka–Tzameret–Wigderson(CCC 2016 / ToC 2021). 단, 알려진 대수 회로 하한을 증명 복잡도로 옮긴 것이고 어려운 예는 비불리언(subset-sum) | FSTW |
| IPS 초다항 하한 ⇒ VNP ≠ VP (Grochow–Pitassi) | 맞음 — IPS 전체에서 어떤 불리언 항진식이든 초다항 하한 ⇒ VP ≠ VNP (FOCS 2014, J. ACM 2018) | Grochow–Pitassi |
| 병행 트랙(IPS 부분 체계 하한)이 지연되어도 VP 대 VNP 쪽 성과가 된다 | 부정확 — Grochow–Pitassi 함의는 IPS 전체 하한에만 성립. 부분 체계 하한은 대개 기존 대수 하한의 결과물이어서 VP 대 VNP 진전이 아님 | 위 두 항목 |
| 자연 증명 장벽의 증명 복잡도 판본 = 「강한 체계는 자신의 하한을 실현 가능하게 증명하기 어렵다」(Razborov·Krajíček) | 요약 부정확 — Razborov(Izvestiya 1995)는 「PRG 가정하에 약한 한정 산술 이론(S²₂(α) 등)은 초다항 회로 하한을 증명하지 못한다」이다. 증명 체계 하한 쪽 대응 결과로는 Pich–Santhanam(STOC 2021, 「NP 에 대한 강한 co-비결정 하한은 실현 가능하게 증명될 수 없다」)이 더 가깝다 | — |
| Resolution 과 CDCL 대응 | 맞음 — Pipatsrisawat–Darwiche(2011), Atserias–Fichte–Thurley(2011) | — |
| 상대화·대수화는 명제 증명 체계 하한에 직접 적용되지 않음 | 판단 — 장벽 표에는 판단으로 표시됨, 「왜」 2번째 항목에는 단정문 | — |
고칠 곳
- 핵심 정리 3번째 줄
- 원문: 「대응하는 회로 모델 AC0[p] 의 하한은 Razborov–Smolensky 가 이미 해결했다 — 병목은 회로 하한 기법을 증명 체계 하한으로 이식하는 일반 원리의 부재다.」
- 제안: 「대응하는 회로 모델 AC0[p] 의 하한은 Razborov–Smolensky(1987)가 이미 해결했다 — 이 글은 병목을 회로 하한 기법을 증명 체계 하한으로 이식하는 일반 원리의 부재로 본다.」
- 핵심 정리 5번째 줄·개요 셋째 문단 끝
- 원문: 「병행 트랙: 대수적 증명 체계 IPS 의 부분 체계 하한 — 주 트랙이 지연되어도 대수 회로 하한(VP 대 VNP) 쪽 성과가 된다.」
- 제안: 「병행 트랙: 대수적 증명 체계 IPS 의 부분 체계 하한. IPS 전체에 대한 초다항 하한이면 VP ≠ VNP 가 따라오므로(Grochow–Pitassi), 부분 체계 하한은 그 방향으로 가는 중간 단계다(부분 체계 하한 자체가 VP 대 VNP 성과는 아니다).」
- 「왜」 4번째 항목
- 원문: 「그래서 병행 트랙은 단순한 실패 보험이 아니라 그 자체로 또 하나의 중심 추측을 공략하는 경로가 된다.」 — 앞 문장(Grochow–Pitassi)은 맞으므로, 끝에 「— 다만 그 함의는 IPS 전체 하한에서만 성립한다」를 덧붙인다.
- 7단계
- 원문: 「자연 증명 장벽의 증명 복잡도 판본(강한 체계는 자신의 하한을 실현 가능하게 증명하기 어렵다는 Razborov·Krajíček 계열 결과)」
- 제안: 「자연 증명 장벽의 증명 복잡도 쪽 대응물(PRG 가정하에 약한 한정 산술 이론은 초다항 회로 하한을 증명하지 못한다는 Razborov(1995)·Krajíček 계열 결과, 강한 co-비결정 하한의 실현 가능 증명 불가능성 Pich–Santhanam(2021))」
- 「왜」 2번째 항목
- 원문: 「상대화·대수화 장벽은 명제 증명 체계 하한에는 직접 적용되지 않고, 자연 증명 장벽도 증명 복잡도에서는 실현 가능 증명 가능성이라는 다른 형태로 나타난다.」
- 제안: 「상대화·대수화 장벽은 명제 증명 체계 하한에는 직접 적용되지 않는다고 본다. 자연 증명 장벽은 증명 복잡도에서는 「한정 산술에서의 실현 가능 증명 가능성」이라는 다른 형태로 논의된다.」
고칠 곳을 반영하고 글 아래에 참고 문헌(위 표의 근거)을 붙이면 「검토 완료」로 바꿀 수 있습니다.
이 글에 단 답 0
아직 없습니다.