오픈AI, ETH 반증 주장 공개…원제안자들이 검토
3줄 요약
- AI가 만든 ETH 반증 원고·Lean 증명 공개, 원제안자 포함 연구진이 점검
- 고정된 절 길이의 논리식 해 개수 계산이 대상, 일반 NP 해법으로 확대 불가
- 연구진은 참여가 정확성 인증을 뜻하지 않는다고 밝히고 공개 검토 방식 논의
오픈AI가 10월 26일 지수시간가설(ETH)을 반증했다는 AI 원고와 Lean 형식증명을 공개했다. ETH를 제안한 러셀 임팔리아초·라마모한 파투리와 MIT의 라이언 윌리엄스가 독립적인 검토를 이끈다. 컴퓨터가 문제를 푸는 데 필요한 시간에 관한 오랜 가정이 이번 검토의 대상이다.
세 연구자는 공개 서한에서 자신들의 참여를 주장의 정확성에 대한 인증으로 받아들여서는 안 된다고 밝혔다. 이들은 논증의 옳고 그름과 한계를 확인하고, 다른 연구자가 재구성하고 질문할 수 있는 설명을 만드는 것을 당면 과제로 제시했다. ETH를 전제로 계산의 어려움을 분석해 온 연구자들에게는 가정을 검토할 자료가 생겼다. 오픈AI는 ETH가 그래프 이론·계산생물학·데이터베이스 등 수백 편의 논문에서 조건부 계산 난도를 도출하는 데 쓰였다고 설명했다.
ETH는 참·거짓 값을 배정해 논리식의 모든 조건을 만족시킬 수 있는지 묻는 3-SAT의 최악 계산시간에 관한 가설이다. 공개 원고는 각 절에 들어가는 변수나 그 부정의 수를 고정한 논리식에서, 조건을 만족하는 배정의 개수를 정확히 세는 결정적 알고리즘을 제시한다고 주장한다. 계산시간은 변수 수에 대해 지수함수보다 완만하게 증가하고 메모리는 다항식 범위라는 내용이다.
해의 개수가 0보다 큰지 확인하면 만족 가능 여부도 판정할 수 있다. 다만 원고는 이런 시간 보장이 일반적인 다항시간 환원을 거쳐 모든 NP 문제로 그대로 옮겨가지는 않는다고 명시했다. 여기서 다루는 것은 고정된 절 길이의 논리식이다. 원고에 적힌 날짜는 10월 17일이며, 10월 25일 개정본이라는 표시가 있다. 이 시간 상한만으로 P=NP가 따라오지는 않는다.
원고의 속도 상한과 형식증명의 범위
검사 대상으로 공개한 정리 문장 파일은 고정된 k가 2 이상인 논리식을 정해진 방식으로 인코딩했을 때의 정확한 해 개수 계산을 대상으로 한다. 이 파일은 변수 개수와 입력의 비트 길이를 구분하며, 계산 과정이 사용하는 공간에도 다항식 한계를 둔다. 자연어 원고를 읽는 것 외에 어떤 입력과 계산 모형을 검증 대상으로 삼았는지 확인할 수 있게 한 자료다.
형식화 문서가 적은 계산시간 상한은 10월 25일 원고의 더 날카로운 상한보다 약하다. 둘 다 변수 수에 대해 부분지수시간이라는 범주에 들지만, 원고의 개선된 속도 표현 전체가 같은 수준으로 형식화됐다고 읽으면 범위를 넓히게 된다. 문서에는 일반 절 수의 경우와 절 수가 변수 수에 비례하는 경우를 나눠 원고의 상한도 별도로 적었다.
Lean 측의 Comparator 설명에 따르면 비교 검사는 제출한 증명이 목표와 같은 문장을 증명하는지, 허용된 공리만 쓰는지, Lean 커널이 받아들이는지를 확인한다. 문장에 등장하는 정의도 대조 대상이다. 따라서 기계 검사가 겨냥하는 정리의 문장과, 연구자가 일상 언어로 이해한 ETH의 관계를 읽는 작업이 검토 과정에 남는다.
오픈AI 저장소는 자료를 미공개 내부 모델이 만든 원고와 증명 산출물로 소개한다. 모델의 이름은 밝히지 않았으며, 전체 자료는 검증 단계가 서로 다른 원시 연구 자료라고 설명한다. 수정·정정은 새 버전으로 남기고 이전 공개판도 계속 열람할 수 있게 한다는 방침이다. 이번 ETH 원고와 범위 설명서를 특정해 읽어야 각 자료의 주장을 대조할 수 있다.
오픈AI는 ETH의 자연어 반증을 10월 16일 얻었고 다음 날 Lean으로 형식화했다고 밝혔다. 외부 검토에는 비밀유지계약을 요구하지 않으며 참여는 자발적이고 무보수라고 설명했다. 윌리엄스도 자신의 공개 글에서 PDF와 Lean 소스를 즉시 공개해 달라고 요청했고 회사가 이를 받아들였다고 확인했다. 그는 검토 중의 발견 사항을 학계와 계속 공유하겠다고 밝혔다. 회사는 이 결과가 분야에 미치는 영향을 논의할 학술행사에 자금을 지원하기로 했다.
연구진의 서한은 질문·빈틈·수정·확인된 단계를 공유하면서도 독립적인 접근과 비판을 열어 두는 검토 방식을 논의하고 있다. 설명문과 단순화한 증명, 세미나도 협업 수단으로 제시했다. 부록은 2026년 말 이전에 열 것을 제안한 온라인 회의의 필요성·형식·시기에 관한 의견을 요청한다. 회의 개최일은 아직 명시하지 않았다.
출처
- October 26 announcement: independent examination of the ETH claim — OpenAI
- The Exponential Time Hypothesis is False — October 17, revised October 25 manuscript — OpenAI
- Family 378 — scope of the Lean formalization — OpenAI
- Comparator — statement, axiom and kernel checks — Lean FRO / Lean Prover
- Mathematics repository — artifact provenance and version policy — OpenAI
- Message to the TCS Community on ETH — Russell Impagliazzo, Ramamohan Paturi and Ryan Williams
- Independent examination of the ETH claim — public thread, October 26/27 — Ryan Williams
- SubexponentialSAT — target statement and computational encoding — OpenAI