오픈AI, 지수시간가설 반박 원고 공개…외부 연구진과 검증·해설 추진
오픈AI(OpenAI)가 10월 26일 AI가 작성한 지수시간가설(Exponential Time Hypothesis·ETH) 반박 원고와 형식 증명 자료를 공식 연구 저장소에 공개했다. ETH는 논리 문제를 푸는 데 필요한 시간의 한계에 관한 가설이다. 회사는 독립적인 컴퓨터과학 연구 그룹이 증명을 검토하고 설명할 예정이라고 밝혔다. 학계 검토가 끝났다는 발표는 아니다.
자세히
ETH의 중심 대상은 각 조건에 변수가 세 개씩 들어가는 3-SAT 문제다. 여러 참·거짓 조건을 한꺼번에 만족시키는 값이 존재하는지 묻는다. 변수 증가에 따라 최악의 경우 필요한 계산 시간이 얼마나 커지는지가 쟁점으로, 특정 문제 하나를 풀었다는 보고와 구별된다.
공개 원고는 조건을 만족시키는 값의 조합을 정확하게 세는 알고리즘을 제시한다. 각 조건에 들어가는 변수 수를 고정했을 때 준지수 시간과 다항식 크기의 저장 공간으로 처리한다는 내용이다. 여기서 준지수 시간은 기존 가설이 요구한 지수적 증가보다 느린 시간 증가를 뜻한다. 곧바로 일상적인 컴퓨터에서 짧은 시간에 끝난다는 의미는 아니다.
원고는 10월 17일 작성, 10월 25일 수정으로 표시돼 있어 26일 공개 발표와 구별된다. 조건을 만족하는 조합의 개수가 양수인지 확인하면 해의 존재도 판별할 수 있다. 개수를 세는 알고리즘이 ETH 반박으로 이어지는 이유다. 원고는 해당 입력 전체에 대한 알고리즘의 성질을 증명하려 한다.
형식 증명 범위 문서는 검증 대상을 더 구체적으로 한정한다. 정해진 방식으로 부호화한 논리식에 대해 결정적 계산 기계가 해의 개수를 정확히 세고, 계산 중 사용하는 공간도 제한된다는 내용이다. 또한 25일 원고가 제시하는 시간 상한이 린으로 설명한 상한보다 더 강하다고 구별한다. 두 자료가 나란히 공개됐다는 이유로 세부 주장까지 모두 같다고 읽어서는 안 된다.
형식 증명은 문장의 의미를 수학적 명제와 추론 규칙으로 옮겨 확인하는 방식이다. 따라서 독자에게 필요한 질문은 검증 도구를 사용했는지에 더해, 어떤 명제를 어떤 조건 아래 확인했는지다. 이번 공개 자료는 그 범위를 따로 적어 놓았다. 이 구분을 지키면 원고 전체를 통째로 자동 검증했다는 과장도, 공개된 검증 자료를 단순한 참고 파일로 낮춰 보는 해석도 피할 수 있다.
공개 이력에는 러셀 임팔리아초, 라마모한 파투리, 라이언 윌리엄스가 이끄는 독립 연구 그룹이 증명을 살펴보고 설명할 예정이라고 적혀 있다. 저장소 설명은 AI가 만든 원고들을 완성된 학술 논문보다 연구 기초 자료로 봐야 한다고 밝힌다. 공개 자료마다 검증 단계가 다르고, 모든 원고에 형식 증명이 붙어 있는 것도 아니다. 이번 ETH 자료에 명시된 검증 범위를 다른 수록 원고 전체에 적용해서는 안 된다.
실제 프로그램이 얼마나 빨라질지도 아직 말하기 어렵다. 원고는 답이 맞는지 효율적으로 확인할 수 있는 계산 문제들의 집합인 NP 전체에 같은 준지수 시간 결과가 옮겨가는 것은 아니라고 명시한다. 다른 문제로 확장하려면 변환 과정에서 문제 크기가 얼마나 늘어나는지 따져야 한다. 이번 공개로 이론적 주장과 검증 재료가 학계에 제시됐지만, 상용 프로그램의 성능 향상은 확인되지 않았다.
- 무엇이 달라지나
- 공식 공개 이력에 따르면 외부 연구 그룹의 요청으로 원고와 검증 자료를 즉시 공개했다. 원고뿐 아니라 컴퓨터가 논리적 단계를 확인할 수 있도록 작성한 린(Lean) 증명 자료도 열어, 주장과 검증 범위를 함께 살필 수 있게 했다.
- 한계
- 공개 원고의 주장을 학계의 검토가 끝난 결론으로 다루지 않는다. 논문은 모든 계산 문제를 빠르게 풀 수 있다는 결과를 주장하지 않으며, 문서에 나온 형식 증명 범위와 원고의 더 강한 시간 상한도 서로 다르다.