
2026년 10월 26일 오픈AI는 내부 모델이 수학·컴퓨터과학·물리학에서 세 가지 결과를 냈다고 발표했다. 그중 컴퓨터과학 결과는 지수 시간 가설(Exponential Time Hypothesis, ETH)을 반박하는 알고리즘이다. 다만 논문이 제시한 실행 시간은 점근적 한계에 관한 것이며, 숨은 상수는 공개되지 않았다. ETH를 제안한 연구자 두 명이 포함된 외부 검토 그룹이 증명을 살펴볼 예정이다.
이 해설은 오픈AI의 2026년 10월 26일 발표를 설명한다. 원문은 https://openai.com/index/building-scientific-understanding-with-academic-communities/에서 볼 수 있다.
오픈AI는 미공개 모델이 ETH가 거짓이라는 결과, 모든 차원에서 국소 평활화 추측이 성립한다는 결과(카케야 추측도 해결한다는 주장), 양자장론으로서 QCD가 존재한다는 결과를 냈다고 밝혔다. 3-SAT에 관한 논문은 모든 해를 세는 결정론적 알고리즘을 제시하며, 다항식 공간을 사용한다. 논문과 Lean 증명 파일은 공개됐지만, 실제 실행 시간은 숨은 상수와 입력 크기에 달려 있다.
오픈AI가 발표한 세 가지 결과
오픈AI는 내부 모델이 수학·컴퓨터과학·물리학 분야에서 결과를 냈다고 발표하고, 원고를 “원시 연구 데이터”라고 불렀다. 각 결과를 검토할 외부 전문가 그룹을 구성해 달라고 요청했다.
- 수학: 모든 차원에서 소그(Sogge)가 1991년에 제기한 국소 평활화 추측의 증명이다. 오픈AI는 이 결과가 모든 차원에서 카케야 추측과 스타인( Stein)의 제한 추측도 해결한다고 밝혔다. AI가 결과를 낸 날짜는 10월 18일이고, 다음 날 Lean으로 형식화했다. 두 결과물은 공개돼 있다.
- 컴퓨터과학: ETH가 거짓이라는 증명이다. AI는 10월 16일 결과를 찾았고, 10월 17일 Lean으로 형식화했다. 증명과 Lean 파일은 공개돼 있다. UC San Diego의 러셀 임팔리아초(Russell Impagliazzo)와 라마모한 파투리(Ramamoхан Paturi), MIT의 라이언 윌리엄스(Ryan Williams)가 이끄는 그룹이 검증하고 설명할 예정이다.
- 물리학: QCD와 순수 양-밀스 이론을 포함하는 표준 모형의 완성을 비롯한 양자장론의 존재 증명이다. 2004년 노벨 물리학상을 공동 수상한 데이비드 그로스(David Gross)가 이끄는 그룹이 이를 정리할 예정이다. AI가 만든 자료는 공개되지 않았다. 오픈AI는 양-밀스 이론의 Lean 형식화가 10월 16일 끝났다고 밝혔다.
오픈AI는 학술적 공로를 원하지 않으며, 실무 그룹은 무급으로 참여하고 자유롭게 발표할 수 있다고 밝혔다. 또 ETH 결과에 관한 학회를 지원하고, AI가 만든 결과를 다루는 워크숍을 위해 시몬스 재단에 500만 달러를 기부했다고 설명했다.
ETH가 말하는 것
3-SAT는 참 또는 거짓으로 정하는 변수 n개에 값을 배정해, 변수 세 개로 이뤄진 모든 절을 만족시킬 수 있는지 묻는 문제다. 가능한 모든 배정을 시도하면 2의 n제곱 단계가 든다.
더 효율적인 방법도 있지만, 논문에 따르면 지수의 상수를 줄이는 수준에 그쳤다. 쇼닝의 지역 탐색 알고리즘은 (4/3)의 n제곱 시간이며, 장(Jiang)과 차이(Cai)의 최근 프리프린트는 약 1.307의 n제곱 시간을 제시한다.
임팔리아초와 파투리는 프랜시스 제인(Francis Zane)과 함께 ETH를 제안했다. 논문은 이들의 2001년 연구를 인용한다. ETH는 최악의 경우 3-SAT에 2의 cn제곱에 해당하는 시간이 필요하다고 본다. 여기서 c는 어떤 고정된 양의 분수이며, 어떤 알고리즘도 이 분수를 0에 가까워지게 만들 수 없다는 뜻이다. 오픈AI의 발표에 따르면 ETH는 다른 문제의 계산 난도를 보이는 수백 편의 논문에서 사용돼 왔다.
강한 ETH(SETH)는 ETH보다 강한 주장이다. 따라서 ETH가 거짓이라면 SETH도 무너진다. 그러나 P 대 NP 문제의 답이 바뀌는 것은 아니다. 논문도 일반적인 환원 아래에서는 이런 실행 시간 한계가 모든 NP 문제에 그대로 적용되지 않는다고 지적한다.
논문이 주장하는 알고리즘
10월 17일 작성되고 10월 25일 수정된 논문은 고정된 k가 2 이상일 때 k-CNF 공식의 만족 배정 수를 모두 세는 결정론적 알고리즘을 제시한다. 알고리즘은 다항식 공간을 사용한다.
- 일반 공식에서는 (n + m)의 고정된 거듭제곱에 2의 O(n 곱하기 ln ln n의 제곱근 나누기 ln n의 제곱근)제곱을 곱한 시간이 든다.
- 절의 수가 D 곱하기 n 이하인 공식에서는 2의 O(n 나누기 ln n의 제곱근)제곱 시간이 든다.
세는 문제는 판정 문제보다 어렵기 때문에 같은 알고리즘으로 3-SAT를 판정할 수 있고, 변수를 하나씩 정해 해를 찾을 수도 있다. 논문은 그래프 색칠, 독립 집합, 완전 매칭을 더 빠르게 정확히 세는 방법과 새로운 회로 하한도 도출한다.
수치로 본 실행 시간
빅오 표기법은 상수를 숨기며 논문은 그 값을 밝히지 않는다. 아래 표의 모든 숨은 상수를 1로 둔 것은 해설의 가정이다. 실제 상수는 훨씬 클 수 있다.
Exponent per variable (bits of work per variable), with every hidden constant set to 1
n (variables) general bound sparse bound Lean statement PPSZ (best known)
1,000 0.53 0.38 1.42 0.386
1,000,000 0.44 0.27 1.86 0.386
1,000,000,000 0.38 0.22 2.02 0.386
general bound = sqrt(ln ln n / ln n) paper, Theorem 1.1, any clause count
sparse bound = 1 / sqrt(ln n) paper, Theorem 1.1, clauses <= D times n
Lean statement = (ln ln n)^2 / sqrt(ln n) the weaker bound the Lean theorem proves
PPSZ = log2(1.307031578) Jiang and Cai's randomized 3-SAT bound, cited in the paper
표의 수치는 변수 하나당 필요한 작업량을 비트 단위로 나타낸다. 현재 알려진 최선의 3-SAT 알고리즘은 변수당 약 0.386비트가 든다. 숨은 상수를 1로 두더라도 새 알고리즘의 일반 경계가 이보다 낮아지는 것은 변수가 약 5억 4,000만 개일 때다. 변수당 절의 수가 일정하게 제한되는 희소 공식에 적용하는 경계는 약 800개부터 이보다 낮아진다.
이에 따라 오픈AI도 이 결과를 실용적인 개선으로 바꾸려면 “상당한 추가 연구가 필요하다”고 밝혔다. 결과는 계산 비용이 장기적으로 어떻게 증가하는지를 다루며, 현재 실행하는 솔버의 성능 개선을 뜻하지 않는다.
Lean 증명이 확인하는 범위
저장소에는 정리를 일반 Lean 문법으로 적은 짧은 Comparator 과제 파일과 이를 증명하는 별도의 솔루션 라이브러리가 있다. exact_count_and_sat 정리는 k가 2 이상인 각 값에 대해 다중 테이프 기계와 양의 상수 C, A, S, d, e가 존재한다고 말한다. 이 기계는 모든 k-CNF 공식에 대해 정확한 해의 개수를 세고 참·거짓 답도 올바르게 낸다. 실행 시간은 C 곱하기 (입력 비트 수 + 1)의 d제곱에 2의 A 곱하기 rho(n)제곱을 곱한 값 이내이며, 공간은 다항식이다.
rho(n)은 n 곱하기 ln ln(n+16)의 제곱을 ln(n+16)의 제곱근으로 나눈 값이다. 논문 6.4절은 이를 더 약한 지수라고 부른다. 그래도 장기적으로는 고정된 n의 분수보다 작아지므로 ETH를 반박한다.
다만 두 가지 한계가 있다.
- 정리는 상수들이 존재한다고만 할 뿐 값을 제시하지 않는다. 따라서 실제 공식에 적용할 수 있는 실행 시간 상한을 계산할 수 없다.
- 상수를 모두 1로 두어도 rho(n)/n이 1 아래로 내려가는 것은 ln n이 약 5,500을 넘을 때다. 이는 n이 약 2,400자리인 경우에 해당한다. 그보다 작은 n에서는 증명된 경계가 모든 배정을 시도하는 방법보다 느리다.
과제는 Lean의 표준 공리 세 개만 허용한다. 솔루션 폴더에는 파일 3,977개가 있으며, 10월 27일 GitHub 파일 목록 기준 용량은 약 35.5MB다. 이 해설에서는 직접 빌드하지 않았다. README가 제시한 명령은 다음과 같다.
lake env comparator ComparatorChallenges/SubexponentialSAT.json
저장소와 검증 상황
openai/math저장소에는 373개 계열에 걸친 원고 721편이 있다. README는 최상위 결과의 약 42%가 Lean으로 형식화됐다고 밝힌다.- 모델에 제시된 문제는 약 4,000개였고, 각 결과에 평균 3시간의 ChatGPT Pro 추론 연산이 사용됐다.
- 오픈AI는 10월 7일 부호 오류로 논증이 무너진 원고 세 편을 철회하고 14편을 수정했다. Lean 검사를 받지 않은 결과는 틀릴 수 있다고 README도 밝힌다.
ETH를 가정한 복잡도 이론 논문은 반박 증명이 성립하면 그 가정에 기대던 난도 결과의 근거를 잃는다. 다만 실무 그룹의 검증은 진행 중이다. SETH는 ETH를 함의하므로 증명이 맞다면 SETH도 성립하지 않는다. 반면 SAT 솔버와 이를 사용하는 도구에는 당장 변화가 없다. 개선이 나타나는 입력 규모는 현실의 입력보다 훨씬 크고 상수도 공개되지 않았다. P 대 NP 문제는 논문 자체의 설명에 따라 이번 결과의 영향을 받지 않는다.
독자가 알아둘 점
복잡도 이론을 다룬다면 커뮤니티의 공개 검토를 요청한 임팔리아초·파투리·윌리엄스 그룹의 검증을 지켜볼 수 있다. Lean 과제의 정리 문장은 약 220줄이며, 저장소의 출처 자료에 실려 있다. 다만 지금은 이 결과를 근거로 솔버, 보안 추정치, 제품 계획을 바꾸지 말아야 한다. Lean 검사를 거치지 않은 AI 생성 증명은 초안으로 취급해야 한다는 점도 10월 7일 원고 철회 사례가 보여준다.
아직 증명이 검토를 통과했는지는 알 수 없다. 실무 그룹의 참여는 증명을 승인했다는 뜻이 아니다. Lean 문장이 의도한 주장을 정확히 표현하는지도 전문가가 확인해야 한다. Lean 검사는 적힌 문장을 증명할 뿐이며, 이 해설은 그 문장이 ETH에 관한 주장과 맞는다고 판단하지만 이는 해설자의 해석이다. 논문과 Lean 정리가 공개하지 않은 숨은 상수의 크기도 미지수다. 물리학 자료는 공개되지 않아 그로스 그룹 외부에서는 현재 QCD 주장을 검토할 수 없다. 표의 수치는 상수를 1로 가정한 것으로, 실제 실행 시간이 아니라 경계가 커지는 양상을 보여준다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요