OpenAI·앤트로픽이 동시에 풀었다는 난제, 수학계는 어떻게 확인할까

OpenAI는 10월 26일 수학, 컴퓨터과학, 물리의 난제 세 개를 이름을 밝히지 않은 내부 모델로 풀었다고 발표했습니다. 그중 하나가 지수시간가설(Exponential Time Hypothesis, ETH)이 틀렸다는 증명입니다. 저장소 반영 시각 기준으로 약 6시간 뒤에는 앤트로픽도 같은 가설을 반증한 논문을 GitHub에 올렸습니다.

두 회사는 풀었다고 발표했고, 이제 학계가 확인할 차례입니다. OpenAI 모델은 10월 16일 ETH 반증을 찾았고, 다음 날 Lean 증명까지 마쳤습니다. Lean은 증명의 각 단계를 컴퓨터가 규칙대로 검사할 수 있게 적는 언어입니다.

다만 공식 인정까지는 시간이 걸립니다. OpenAI가 9월 8일 발표한 나비에-스토크스 증명은 7주가 지났지만, 클레이수학연구소(Clay Mathematics Institute) 뉴스 목록에는 후속 글이 없습니다. OpenAI는 이번에 수학·ETH 결과를 공개하고 외부 학자 그룹과 협업하는 방식을 내놨습니다. 다만 Lean 검사를 통과해도, Lean으로 적은 문장이 논문과 같은 말인지는 여전히 사람이 읽어야 합니다.

세 가지는 무엇을 풀었다고 하나

수학 결과는 1991년 Sogge가 제기한 국소 평활화 추측(local smoothing conjecture)입니다. 파동이 한곳으로 모여드는 현상을 다룹니다. 파동이 가장 세게 한곳에 몰리는 순간은 잠깐뿐이고, 아무 때나 측정해 보면 몰린 정도가 그 최악의 순간보다 훨씬 작다는 내용입니다. 2019년 다른 연구진이 2차원에서 증명했고, OpenAI는 자사 모델이 모든 차원에서 증명했다고 밝혔습니다. OpenAI는 여기서 Kakeya 추측과 Stein 제한 추측도 모든 차원에서 따라 나온다고 설명했습니다.

ETH는 Impagliazzo·Paturi·Zane가 2001년 논문에서 제기한 가설입니다. 대상인 3-SAT는 참·거짓 변수로 만든 논리식을 참으로 만드는 값이 있는지 묻는 문제로, 조건 하나에 변수가 최대 셋 들어갑니다. ETH는 가장 어려운 식에서는 어떤 방법을 써도 걸리는 시간이 변수 수에 따라 지수로 불어난다고 봅니다.

OpenAI 논문은 이 예상을 뒤집는다는 알고리즘을 실었습니다. 3-SAT를 포함한 더 넓은 형태의 논리식에서 참이 되는 값의 개수까지 세는 방법입니다. 변수가 늘어도 걸리는 시간은 지수보다 천천히 늘어납니다. OpenAI에 따르면 논문 수백 편이 "ETH가 참이라면 이 문제는 빨리 풀 수 없다"는 식의 결과를 ETH에 기대어 증명했습니다. 앤트로픽 논문은 이 결과가 P 대 NP 문제와 직접 관련이 없고 실용적인 알고리즘도 아니라고 했습니다.

물리 결과는 양자색역학(QCD)과 관련됩니다. QCD는 쿼크와 글루온 같은 입자가 강한 힘으로 주고받는 상호작용을 설명하는 이론입니다. OpenAI는 QCD를 포함한 특정한 4차원 양자장론이 수학적으로 엄밀하게 존재한다는 증명, 즉 이 이론을 수학의 기준에 맞게 세울 수 있다는 증명을 냈다고 했습니다.

하위 문제로 다룬 순수 양-밀스 이론은 쿼크 같은 물질 없이, 힘을 전하는 글루온끼리의 상호작용만 다룹니다. OpenAI는 이 이론의 존재 증명이 클레이수학연구소가 정한 밀레니엄 난제 가운데 '양자 양-밀스 이론' 문제의 일부라고 소개했습니다.

앤트로픽도 같은 결론을 냈다

앤트로픽은 anthropics/formal-math 저장소에 논문과 Lean 증명을 함께 올렸습니다. 논문에 따르면 내부 Claude 연구 모델이 10월 16일 사람의 입력 없이 핵심 알고리즘을 찾았고, 이때 출력 토큰 1,400만 개를 썼습니다.

OpenAI가 밝힌 발견일도 10월 16일입니다. 앤트로픽 논문은 OpenAI의 주장을 인용하면서, 두 결과가 서로 독립적으로 같은 시기에 나왔다고 썼습니다.

Lean을 통과해도 사람이 읽어야 하는 이유

Lean에서 각 단계를 검사하는 것은 컴퓨터지만, 검사 대상인 정리(定理)를 Lean 문장으로 옮겨 적는 일은 사람이나 AI가 합니다. 그 문장이 논문의 정리와 같은 말인지는 사람이 읽고 비교해야 합니다.

앤트로픽도 README에서, 정리를 적은 파일이 논문과 같은 내용인지는 기계로 확인할 수 없다고 인정했습니다. 그래서 그 파일을 사람이 읽을 만큼 짧게 두고, 논문 부록에 두 표현의 차이를 모아 두었습니다. OpenAI의 Lean 문서에도 Lean으로 증명한 시간 상한이 논문 본문보다 느슨하다는 설명이 들어 있습니다.

OpenAI는 9월 8일 유체의 흐름을 다루는 나비에-스토크스 방정식에 관한 밀레니엄 난제의 일부를 풀었다고 발표했습니다. 클레이수학연구소는 9월 11일 이 문제가 "풀린 것으로 보인다"는 발표가 나왔다고 알리며, 검토는 일부러 서두르지 않되 진행 상황은 알리겠다고 했습니다.

10월에는 킹스칼리지런던·케임브리지 연구진이 심사 전 논문에서 Lean 증명이 글로 쓴 증명과 맞지 않는다고 주장했습니다. 대학은 보도자료에서, 연구진이 원래 증명이 틀렸다는 것까지 보인 것은 아니며 두 증명이 서로 다른 명제를 다루는 것으로 보인다고 설명했습니다.

OpenAI가 앞서 공개한 AI 논문 가운데 오류가 확인돼 철회한 것도 있습니다. 이번 세 결과와는 별개인 대수기하학 논문 한 편에서 부호 오류가 나왔고, OpenAI는 10월 7일 이 논문과 여기에 기댄 논문 두 편을 함께 철회했습니다. 다른 논문 14편도 손봤다고 수학 저장소의 변경 기록에 적었습니다.

이번에 OpenAI는 외부 학자 그룹을 확인 절차에 넣었습니다. ETH 그룹은 가설을 함께 제안한 Impagliazzo·Paturi, 그리고 MIT의 Williams가 이끕니다. 세 사람은 공개 서한에서 자신들이 참여했다고 해서 증명이 맞다고 보증하는 것은 아니라고 선을 그었습니다. 주장이 맞다면 이론 컴퓨터과학의 중요한 부분이 바뀔 것이라고도 했습니다.

물리 그룹은 2004년 노벨물리학상을 받은 David Gross가 이끌며, AI가 만든 증명을 공개하지 않고 직접 글로 옮겨 쓰기로 했습니다. OpenAI는 9월 수학·AI 자문 그룹을 꾸린 데 이어, 공개 방식을 학계 의견에 따라 계속 바꾸고 있다고 했습니다.

연구자에게 달라지는 것

결과를 낸 모델은 두 회사 모두 내부 모델이라 외부에서 쓸 수 없습니다. 대신 수학·ETH 결과의 논문과 Lean 증명은 GitHub에 있어, 외부 연구자도 증명 검사를 직접 실행해 결과를 볼 수 있습니다.

OpenAI는 내부 모델이 낸 결과로 학술적 공로를 인정받으려 하지 않는다고 밝혔습니다. 검토를 돕는 기금도 약속했습니다. 이번 발표에 앞서 10월 15일, OpenAI는 Simons 재단이 새로 여는 사업에 500만 달러를 내겠다고 했습니다. 수학자가 AI의 결과를 검토하고 이해하도록 돕는 사업입니다. 돈은 재단이 관리하고, 워크숍과 학회 등을 지원할 예정입니다.

앤트로픽은 README의 압축 설명을 공개 모델 Claude Opus 5.5에 주면 높은 추론 강도에서 반증을 다시 끌어낸다고 주장합니다. 다만 이때 얻는 결과는 논문보다 느슨합니다. 3-SAT에 답이 있는지 판정하는 데 걸리는 시간이 지수보다 천천히 늘어난다는 데까지입니다.

논리식 풀이 도구를 쓰는 개발자에게는 당장 바뀌는 것이 없습니다.

이론 연구자에게는 사정이 다릅니다. ETH를 전제로 결과를 쌓아 온 연구자라면, 검토 그룹이 내릴 결론에 따라 자기 연구의 출발점을 다시 봐야 할 수 있습니다. 세 사람은 서한에서 주장이 맞다면 일부 해석은 바뀔 수 있지만, 그동안 쌓은 기법과 아이디어의 가치는 남는다고 했습니다.