앤스로픽 논문도 ETH를 반박했지만 실전 영향은 없다

앤스로픽은 2026년 10월 27일 클로드가 3-SAT 문제를 아원지수 시간에 푸는 알고리즘을 제시해 지수 시간 가설(ETH)을 반박한다는 논문을 공개했다. 오픈AI도 같은 날 자사 모델이 비슷한 결과를 냈다고 발표했지만, 두 증명은 아직 연구자들이 검토하고 있다.

논문은 A 2^o(n) Time Algorithm for 3-SAT이며, 저자란에는 “Claude (Anthropic)”이라고 적혀 있다. 앤스로픽은 핵심 알고리즘을 내부 클로드 연구 모델이 10월 16일 인간의 입력 없이 출력 토큰 1,400만 개를 사용해 찾았다고 밝혔다. 논문은 오픈AI 내부 모델도 독립적으로 비슷한 결과를 증명했다고 주장한다고 덧붙였다.

3-SAT는 세 개의 리터럴로 이뤄진 절들의 논리식이 참이 될 수 있는지 묻는 문제다. 논문에 따르면 알고리즘은 만족 가능성 판정뿐 아니라 더 어려운 계수 문제인 #3-SAT를 결정적으로 푼다. 앤스로픽 README에 제시된 시간은 2^O(n log log n / sqrt(log n))이다. 이는 모든 양의 d에 대해 2^(dn)보다 느리게 증가하므로 ETH와 모순된다. ETH는 2001년 임파글리아초와 파투리가 제시한 가설로, 3-SAT를 어떤 양의 상수 d에 대해서도 2^(dn) 시간에 풀 수 없다고 본다.

논문은 ETH가 거짓이면 강한 지수 시간 가설(SETH)도 성립하지 않는다고 설명한다. 또 독립 집합, 클리크, 정점 덮개, 지배 집합 문제에도 이론상 아원지수 시간 알고리즘이 가능해지고, E^NP에 대한 새로운 회로 하한도 도출된다고 주장한다.

앤스로픽은 증명을 Lean 4로 형식화해 GitHub에 공개했다. 회사에 따르면 빌드는 가상 CPU 24개에서 약 8분 걸렸고 Lean의 표준 공리 세 개만 사용했다. 지속적 통합 과정에서는 Comparator로 정리 진술을 도전 파일과 비교하고, nanoda라는 별도로 작성한 두 번째 커널로 증명을 다시 검사한다.

다만 형식 검증기가 증명한 명제가 논문에 적힌 주장과 일치하는지까지 확인해 주지는 않는다. 앤스로픽은 이 점을 고려해 정리 진술 파일을 짧게 유지하고, 논문 부록에 그 내용과 논문 사이의 차이를 실었다고 설명한다. 따라서 두 연구소의 결과가 실제로 ETH를 반박하는지는 형식 증명뿐 아니라 정리 진술 자체도 전문가가 살펴봐야 한다.

이 결과는 실용적인 SAT 풀이를 바꾸지 않는다. 논문도 “우리 결과는 실제로 수식을 푸는 일에 관해 아무것도 말해주지 않는다”고 선을 긋는다. 논문이 제시한 새 시간 경계가 완전 탐색보다 빨라지는 변수 수는 다음과 같다.

논문은 변수 100개인 문제도 이미 완전 탐색으로는 풀기 어렵다고 설명한다. 산업용 SAT 솔버가 사용하는 휴리스틱은 이번 결과의 영향을 받지 않는다. 또한 이 결과가 P와 NP의 관계에 직접 영향을 주는 것은 아니다.

버클리 이론 컴퓨터과학자 젤라니 넬슨(Jelani Nelson)은 X에 두 모델이 같은 날 결과를 얻은 것으로 보인다고 적었다. 그는 공개 전 주에 다른 연구자들과 클로드의 증명을 읽고 설명을 다듬는 데 도움을 줬다고 밝혔다. 넬슨은 두 증명이 하위 차수 항을 제외하면 대략 exp(O(n / sqrt(log n))) 시간에 이르는 것으로 보인다고 덧붙였다.

라이언 윌리엄스(Ryan Williams), 러셀 임파글리아초(Russell Impagliazzo), 라마모한 파투리(Ramamohan Paturi)는 두 형식 명제가 ETH를 제대로 나타내는지 살펴볼 워크숍을 준비하고 있다. 결과를 판단할 다음 단계는 이들의 검토와 두 증명에 대한 외부 전문가들의 평가다. 관련 배경은 오픈AI가 양-밀스·ETH·카쿠야 결과를 주장한 보도에서 확인할 수 있다.