오픈AI·앤스로픽 “지수 시간 가설은 거짓”…검증대 오른 AI 증명

오픈AI와 앤스로픽이 하루 간격으로 자사 AI가 컴퓨터과학의 오랜 가설인 ‘지수 시간 가설(ETH, Exponential Time Hypothesis)’을 반증했다고 발표했다. 두 회사 모두 형식 검증 도구 린(Lean)으로 증명을 확인했다고 밝혔지만, 전문가들의 독립 검증은 이제 시작이다.

무엇을 주장했나

오픈AI는 10월 26일(현지시간) 수학·컴퓨터과학·물리학 세 분야의 새 결과를 발표하면서, 그중 하나로 ETH가 거짓이라는 증명을 내놓았다. 회사에 따르면 내부 AI가 10월 16일 자연어 증명을 찾았고, 다음 날 린으로 형식화했다. 린은 수학 증명의 각 단계를 컴퓨터가 기계적으로 검사하는 프로그래밍 언어다. 오픈AI는 자연어 문서와 린 증명을 깃허브에 공개했다.

앤스로픽은 10월 27일 깃허브에 ‘3-SAT를 2^o(n) 시간에 푸는 알고리즘(A 2^o(n) Time Algorithm for 3-SAT)’ 논문과 린 4 형식화(Lean 4 proof)를 올렸다. 저자는 ‘Claude(앤스로픽)’로 표기됐고, 내부 연구용 클로드 모델이 결과를 찾았다고 밝혔다. 앤스로픽은 이 알고리즘이 변수 n개짜리 3-SAT를 2^o(n) 시간에 판정해 ETH를 반증하고, 더 어려운 문제인 해의 개수 세기(#3-SAT)도 푼다고 설명했다.

ETH는 무엇인가

3-SAT는 참·거짓 변수로 이뤄진 논리식을 모두 참으로 만드는 값이 있는지 묻는 문제다. ETH는 이 문제를 푸는 데 변수 수가 늘수록 지수적으로 더 많은 시간이 든다는 가설로, 1999년 러셀 임팔리아초와 라마모한 파투리가 처음 발표했다. 테크크런치는 ETH가 ‘P≠NP’(답을 확인하기 쉬운 문제도 풀기는 어렵다는 추측)를 뒷받침하는 근거로 여겨져 왔다고 설명했다.

오픈AI는 ETH가 그래프 이론, 계산생물학, 데이터베이스, 계산기하학 등 수백 편의 논문에서 ‘이 문제는 빨리 풀 수 없다’는 결과를 끌어내는 전제로 쓰여 왔다고 밝혔다. 주장이 맞다면 이런 연구를 다시 검토해야 한다.

실용적 의미는 제한적

앤스로픽은 이 결과가 순수하게 점근적(asymptotic, 입력이 한없이 커질 때의 성질)이며 “실제로 논리식을 푸는 일에 대해서는 아무것도 말해 주지 않는다”고 밝혔다. 이 상한값은 변수가 10^108개 이상인 공식에 대해서만 무차별 대입 방식보다 나은 결과를 보여주므로, 실제 해결 방법에는 아무런 변화를 주지 않는다는 설명이다.오픈AI도 더 나은 알고리즘을 찾고 이론적 진전을 실질적 개선으로 잇기까지 상당한 추가 연구가 필요하다고 했다. 라이언 윌리엄스 MIT 교수는 오픈AI 측이 암호 체계를 깨는 결과는 아니라고 “상당히 확신”한다고 테크 크런치에 말했다.

검증은 이제 시작

린 검사를 통과했다고 해서 사람의 검토가 끝난 것은 아니다. 앤스로픽은 린 형식화를 AI 모델이 썼고, 린 정리 파일이 논문의 주장과 같은 내용을 말하는지는 기계가 확인하지 않는다고 밝혔다. 그래서 독자가 직접 대조할 수 있도록 그 파일을 짧게 유지했다는 설명이다.

오픈AI는 임팔리아초·파투리(UC샌디에이고)와 윌리엄스(MIT)가 이끄는 연구단에 검증과 후속 연구를 맡겼다. 이들은 공개서한에서 자신들의 참여를 주장에 대한 인증으로 받아들여서는 안 된다고 밝혔다. 윌리엄스 교수는 테크크런치에 오픈AI의 알고리즘이 “아마 최종 답은 아닐 것”이라고 말했다. 오픈AI는 연구단 요청에 따라 원시 데이터를 모두 공개하고 학술대회 자금을 대기로 했으며, 사이먼스 재단에 500만 달러를 기부했다고 밝혔다.

오픈AI는 같은 발표에서 모든 차원의 ‘국소 평활화 추측’(이에 따라 가케야·스타인 제한 추측) 증명과, 양-밀스 이론·양자색역학(QCD)을 포함한 4차원 양자장론의 존재 증명도 주장했다. 노벨 물리학상 수상자 데이비드 그로스가 이끄는 물리학 연구단은 AI 산출물 공개를 보류하고 직접 논문으로 정리하기로 했다.

	Anthropic	OpenAI
Found by an internal model	October 16	October 16
Made public	Paper dated Oct 26; GitHub and Hexagon Oct 27	Oct 26
Formal proof	Lean 4, plus a second kernel check	Lean, published on GitHub
Stated bound	2^O(n log log n / sqrt(log n)) for #3-SAT	About exp(n / (log n)^(1/2+o(1))), per Ryan Williams
How the discovery is described	14M output tokens, no human input	Checked by Impagliazzo, Paturi and Williams

Table 1Anthropic’s and OpenAI’s ETH results side by side (primary sources, Oct 26-27, 2026)

왜 중요한가

주장이 맞다면 이론 컴퓨터과학의 중요한 전제 하나가 바뀌고, 그 위에 쌓인 많은 연구를 다시 봐야 한다. 동시에 AI가 만든 증명을 누가 어떻게 검증하고 공로를 어떻게 나눌지라는 질문도 함께 던져졌다. TNW에 따르면 검증에 참여한 연구자들은 AI가 만든 결과의 공로가 결과를 검토하고 설명하는 사람이 아니라 먼저 발표하거나 더 강한 도구를 가진 쪽에 돌아갈 수 있다고 경고했다. 두 AI 기업이 하루 간격으로 비슷한 결과를 내놓은 이번 일은 그 경고를 시험하는 첫 사례가 될 전망이다.

*원문: OpenAI · Anthropic GitHub(formal-math/eth)