본문으로 건너뛰기

연구·논문

오픈AI, ETH 반증 주장 공개…원제안자들이 검토

3줄 요약

  1. AI가 만든 ETH 반증 원고·Lean 증명 공개, 원제안자 포함 연구진이 점검
  2. 고정된 절 길이의 논리식 해 개수 계산이 대상, 일반 NP 해법으로 확대 불가
  3. 연구진은 참여가 정확성 인증을 뜻하지 않는다고 밝히고 공개 검토 방식 논의
실무개발자
가지처럼 나뉜 기호가 있는 칠판 앞 빈 세미나실과 연구 원고
AI 생성 개념 이미지: 공개된 수학 주장을 학계가 검토하는 과정을 표현한 빈 세미나실 · AI Ping

오픈AI가 10월 26일 지수시간가설(ETH)을 반증했다는 AI 원고와 Lean 형식증명을 공개했다. ETH를 제안한 러셀 임팔리아초·라마모한 파투리와 MIT의 라이언 윌리엄스가 독립적인 검토를 이끈다. 컴퓨터가 문제를 푸는 데 필요한 시간에 관한 오랜 가정이 이번 검토의 대상이다.

세 연구자는 공개 서한에서 자신들의 참여를 주장의 정확성에 대한 인증으로 받아들여서는 안 된다고 밝혔다. 이들은 논증의 옳고 그름과 한계를 확인하고, 다른 연구자가 재구성하고 질문할 수 있는 설명을 만드는 것을 당면 과제로 제시했다. ETH를 전제로 계산의 어려움을 분석해 온 연구자들에게는 가정을 검토할 자료가 생겼다. 오픈AI는 ETH가 그래프 이론·계산생물학·데이터베이스 등 수백 편의 논문에서 조건부 계산 난도를 도출하는 데 쓰였다고 설명했다.

ETH는 참·거짓 값을 배정해 논리식의 모든 조건을 만족시킬 수 있는지 묻는 3-SAT의 최악 계산시간에 관한 가설이다. 공개 원고는 각 절에 들어가는 변수나 그 부정의 수를 고정한 논리식에서, 조건을 만족하는 배정의 개수를 정확히 세는 결정적 알고리즘을 제시한다고 주장한다. 계산시간은 변수 수에 대해 지수함수보다 완만하게 증가하고 메모리는 다항식 범위라는 내용이다.

해의 개수가 0보다 큰지 확인하면 만족 가능 여부도 판정할 수 있다. 다만 원고는 이런 시간 보장이 일반적인 다항시간 환원을 거쳐 모든 NP 문제로 그대로 옮겨가지는 않는다고 명시했다. 여기서 다루는 것은 고정된 절 길이의 논리식이다. 원고에 적힌 날짜는 10월 17일이며, 10월 25일 개정본이라는 표시가 있다. 이 시간 상한만으로 P=NP가 따라오지는 않는다.

구리선으로 이어진 토글 스위치 교구와 가지 모양 표시가 있는 노트
AI 생성 개념 이미지: 참·거짓 배정의 조합을 스위치 교구로 표현한 장면 · AI Ping

원고의 속도 상한과 형식증명의 범위

검사 대상으로 공개한 정리 문장 파일은 고정된 k가 2 이상인 논리식을 정해진 방식으로 인코딩했을 때의 정확한 해 개수 계산을 대상으로 한다. 이 파일은 변수 개수와 입력의 비트 길이를 구분하며, 계산 과정이 사용하는 공간에도 다항식 한계를 둔다. 자연어 원고를 읽는 것 외에 어떤 입력과 계산 모형을 검증 대상으로 삼았는지 확인할 수 있게 한 자료다.

형식화 문서가 적은 계산시간 상한은 10월 25일 원고의 더 날카로운 상한보다 약하다. 둘 다 변수 수에 대해 부분지수시간이라는 범주에 들지만, 원고의 개선된 속도 표현 전체가 같은 수준으로 형식화됐다고 읽으면 범위를 넓히게 된다. 문서에는 일반 절 수의 경우와 절 수가 변수 수에 비례하는 경우를 나눠 원고의 상한도 별도로 적었다.

Lean 측의 Comparator 설명에 따르면 비교 검사는 제출한 증명이 목표와 같은 문장을 증명하는지, 허용된 공리만 쓰는지, Lean 커널이 받아들이는지를 확인한다. 문장에 등장하는 정의도 대조 대상이다. 따라서 기계 검사가 겨냥하는 정리의 문장과, 연구자가 일상 언어로 이해한 ETH의 관계를 읽는 작업이 검토 과정에 남는다.

오픈AI 저장소는 자료를 미공개 내부 모델이 만든 원고와 증명 산출물로 소개한다. 모델의 이름은 밝히지 않았으며, 전체 자료는 검증 단계가 서로 다른 원시 연구 자료라고 설명한다. 수정·정정은 새 버전으로 남기고 이전 공개판도 계속 열람할 수 있게 한다는 방침이다. 이번 ETH 원고와 범위 설명서를 특정해 읽어야 각 자료의 주장을 대조할 수 있다.

서술형 메모와 코드 형태의 문서 사이에 놓인 돋보기와 붉은 연필
AI 생성 개념 이미지: 서술형 논증과 형식화된 문장을 대조하는 검토를 표현한 장면 · AI Ping

오픈AI는 ETH의 자연어 반증을 10월 16일 얻었고 다음 날 Lean으로 형식화했다고 밝혔다. 외부 검토에는 비밀유지계약을 요구하지 않으며 참여는 자발적이고 무보수라고 설명했다. 윌리엄스도 자신의 공개 글에서 PDF와 Lean 소스를 즉시 공개해 달라고 요청했고 회사가 이를 받아들였다고 확인했다. 그는 검토 중의 발견 사항을 학계와 계속 공유하겠다고 밝혔다. 회사는 이 결과가 분야에 미치는 영향을 논의할 학술행사에 자금을 지원하기로 했다.

연구진의 서한은 질문·빈틈·수정·확인된 단계를 공유하면서도 독립적인 접근과 비판을 열어 두는 검토 방식을 논의하고 있다. 설명문과 단순화한 증명, 세미나도 협업 수단으로 제시했다. 부록은 2026년 말 이전에 열 것을 제안한 온라인 회의의 필요성·형식·시기에 관한 의견을 요청한다. 회의 개최일은 아직 명시하지 않았다.

출처

  • 활용 가이드읽기 약 18분

    AI 결과, 좋아 보이는 것과 쓸 만한 것

    같은 자료로 만든 결과를 채점하고, 한 조건을 고친 뒤 새 문제로 다시 확인합니다. 코딩 없이 평가 세트를 만듭니다.

    심화기획디자이너마케터영업제품 연구직장인개발자
  • 활용 가이드읽기 약 19분

    AI 도입, 시간 절약부터 중단 기준까지

    생성 시간뿐 아니라 검토·수정 시간까지 계산합니다. 작은 가상 기록으로 기준선과 비교하고, 계속 쓸지 고칠지 멈출지 판단합니다.

    심화기획디자이너마케터영업제품 연구직장인개발자