원문 보완판 — 사실 검토 반영

모든 명제 증명 체계에 대해 초다항 크기 하한을 보이면 NP≠coNP, 곧 P≠NP 가 따라온다. 이 글은 그 사다리에서 지금 멈춰 있는 칸인 AC0[p]-Frege 를 정면으로 공략하는 계획이다.

아이디어 개요

Cook–Reckhow 정리에 따르면 모든 명제 증명 체계에 대해 초다항 크기 하한을 보이면 NP≠coNP가 따라오고, 이는 곧 P≠NP를 함의한다.

이 프로그램은 Resolution에 대한 Haken의 지수 하한(1985), 제한 깊이 Frege(AC0-Frege)에 대한 Ajtai 및 Pitassi–Beame–Impagliazzo, Krajíček–Pudlák–Woods의 하한까지는 성공했으나, mod p 카운팅을 허용한 AC0[p]-Frege 앞에서 30년 넘게 정체되어 있다. 흥미로운 점은 대응하는 회로 모델(AC0[p])의 하한은 Razborov–Smolensky의 대수적 방법으로 이미 오래전에 해결되었다는 사실이다.

이 글은 회로 하한 기법을 증명 체계 하한으로 이식하는 일반 원리의 부재를 현재의 병목으로 보며, 본 아이디어는 (1) 다항식 계산법(Polynomial Calculus)의 차수 하한, (2) 질의-통신 리프팅 정리, (3) 증명 복잡도 생성기 기반의 어려운 후보 식이라는 세 가지 최신 도구를 결합해 AC0[p]-Frege 초다항 하한이라는 다음 단계를 정면 공략한다. 동시에 대수적 증명 체계 IPS의 부분 체계 하한을 병행 트랙으로 둔다. IPS 전체에 대한 초다항 하한이면 VP ≠ VNP 가 따라오므로(Grochow–Pitassi), 부분 체계 하한은 그 방향으로 가는 중간 단계다(부분 체계 하한 자체가 VP 대 VNP 성과는 아니다).

구체적 진행 방법

1. 기법-장벽 지도 작성: 실현 가능 보간(feasible interpolation), 스위칭 보조정리 기반 제한 논법, 크기-차수 트레이드오프, 리프팅 등 기존 하한 기법 각각이 AC0[p]-Frege 앞에서 정확히 어느 지점에서 무력화되는지(예: 강한 체계에서 보간이 암호학적 가정하에 실패한다는 Krajíček–Pudlák 계열 결과) 정리한 기술 지도를 만든다.
2. 어려운 후보 식 선정: 비둘기집 원리나 Tseitin 식은 카운팅 능력이 있는 체계에서 쉬워질 수 있으므로, Alekhnovich–Ben-Sasson–Razborov–Wigderson 및 Krajíček의 증명 복잡도 생성기, 특히 Nisan–Wigderson 생성기 기반 식을 주 후보로 채택하고, 확장 변수 도입에 대한 내성 등 후보군의 성질을 비교 분석한다.
3. 대수적 기초 하한 확보: 선정한 후보 식에 대해 유한체 F_p 위 Polynomial Calculus와 Nullstellensatz에서의 차수 하한과 크기 하한을 먼저 확립한다. 이것이 이후 단계의 원천 경도(hardness) 역할을 한다.
4. 대수적 리프팅 개발: 질의 복잡도를 통신 복잡도로 끌어올리는 기존 리프팅 정리를, 차수 하한을 상수 깊이 카운팅 증명의 크기 하한으로 번역하는 형태로 확장한다. 트리형 체계나 Res(lin), Res(mod p) 같은 약한 중간 체계에서 이미 성립하는 부분 결과를 출발점으로 삼는다.
5. 구조 정리 확립: AC0[p]-Frege 증명을 대수적 표준형으로 정규화하는 시뮬레이션 정리를 추진한다. 한정 산술(bounded arithmetic)과의 증명 가능성 번역 대응을 이용해, 크기 하한 문제를 4단계에서 만든 차수·통신 측도의 하한 문제로 환원하는 것이 목표다.
6. 중간 체계 사다리 공략: 깊이를 작게 고정한 카운팅 Frege, 확장 변수를 더한 Nullstellensatz, IPS의 제한 부분 체계(roABP-IPS, 다중선형 IPS 등 Forbes–Shpilka–Tzameret–Wigderson 계열 하한이 알려진 지점) 순서로 사다리를 구성하고, 각 단에서 4–5단계 도구의 유효성을 검증·보완한다.
7. 장벽 감사: 개발한 기법이 자연 증명 장벽의 증명 복잡도 쪽 대응물(PRG 가정하에 약한 한정 산술 이론은 초다항 회로 하한을 증명하지 못한다는 Razborov(1995)·Krajíček 계열 결과, 강한 co-비결정 하한의 실현 가능 증명 불가능성 Pich–Santhanam(2021))에 걸리는지 단계마다 점검하고, 생성기 기반 후보가 이 메타 장벽을 우회하는 근거를 명시적으로 문서화한다.
8. 확장 계획: AC0[p]-Frege가 뚫리면 생성기 경도의 자기 증폭과 한정 산술 독립성 결과를 지렛대로 Frege, Extended Frege로의 상승 전략을 수립하고, 병행 트랙인 IPS 하한은 Grochow–Pitassi 연결을 통해 대수 회로 하한 성과로 정리한다(그 연결은 IPS 전체 하한에 이르렀을 때 성립한다).

왜 해볼 만한 가치가 있는가

1. 가장 선명한 다음 단계다. Cook–Reckhow 사다리에서 Resolution과 AC0-Frege 다음 칸이 바로 AC0[p]-Frege이며, 회로 쪽 대응물은 이미 해결되어 있어 무엇이 빠져 있는지가 분야 내에서 가장 구체적으로 합의된 미해결 지점이다. 성공하면 30여 년 만의 전선 이동이 된다.
2. 고전적 장벽과의 관계가 유리하다고 본다. 상대화·대수화 장벽은 명제 증명 체계 하한에는 직접 적용되지 않는다고 본다. 자연 증명 장벽은 증명 복잡도에서는 「한정 산술에서의 실현 가능 증명 가능성」이라는 다른 형태로 논의된다. 본 계획은 그 형태를 정확히 겨냥해 설계된 생성기 기반 후보 식을 쓰고 7단계에서 장벽 감사를 상시 수행하므로, 알려진 장벽을 정면으로 위반하는 접근이 아니라고 본다.
3. 부분 성과도 독립적 가치가 크다. 새로운 차수 하한, 리프팅 정리의 확장, Res(lin)·IPS 부분 체계 하한은 각각 단독 결과로 성립하며, Resolution과 CDCL SAT 솔버의 대응 관계를 통해 솔버 성능의 이론적 한계 분석이라는 실용적 파생 성과도 나온다.
4. 이중 배당 구조다. Grochow–Pitassi에 의해 IPS에 대한 초다항 하한은 대수 회로 하한(VNP≠VP 방향)을 함의하므로, 병행 트랙은 단순한 실패 보험이 아니라 그 자체로 또 하나의 중심 추측을 공략하는 경로가 된다 — 다만 그 함의는 IPS 전체 하한에서만 성립한다.
5. 메타수학적 배당이 있다. 한정 산술 대응을 경유하므로 최종 목표에 못 미치더라도 특정 산술 이론에서 회로 하한 명제가 증명 불가능하다는 독립성 결과를 얻을 수 있고, 이는 P 대 NP가 왜 어려운지에 대한 정량적 설명을 축적하는 성과가 된다.