"수학자들은 요청한 적 없다" 오픈AI 수학 원고 31시간 만에 3편 철회

부호 하나에 원고 3편

저장소에 새로 생긴 변경 기록(history.md)이 철회 경위를 적고 있습니다. 문제의 원고는 「쪼개진 아벨 8차원 다양체 위 베유 류의 대수성」입니다. 철회 공지에 따르면 원고는 음수로 남은 이중점 개수 −m을 지우려고 안정화 자취(stabilization trace)를 m개 넣으면서 각 자취의 부호를 +1로 셌습니다. 실제 부호는 −1이어서 합은 −2m으로 남고, 합이 0이어야 쓸 수 있는 엘리아시베르크–머피 상쇄 정리의 전제가 성립하지 않습니다. 그 뒤에 이어지는 구성도 근거를 잃었고, 같은 구성을 빌려 쓴 「K3 곡면의 쿠가–사타케 대응의 대수성」과 「K3 곡면 곱의 유리 호지 추측」이 함께 내려갔습니다.

세 번째 원고는 공개 다음 날 새벽 스콧 애런슨 텍사스대 오스틴 교수가 블로그에서 호지 추측 쪽 진전으로 링크했던 원고입니다. 철회 공지는 증명을 거둬들일 뿐 명제가 거짓이라고 주장하지는 않는다고 덧붙였고, 철회 전 PDF는 첫 커밋 주소로 남겨 두었습니다. 누가 오류를 처음 찾았는지는 기록에 없습니다.

변경 기록에는 다른 손질도 함께 적혀 있습니다. 립시츠 높이와 애시킨–텔러 흐름을 다룬 원고 4편, 켈러 극소 모형 프로그램 원고 6편 등 14편에서 증명을 보수하거나 진술과 가정을 고쳤고, 고친 원고를 인용하는 13편은 참고문헌 날짜를 새 판에 맞췄습니다. 원고 수는 722편에서 719편이 됐습니다. 공개 직후 Lean 형식화 목록 파일에 오른 원고는 162편이었고, 10월 8일 수정 뒤에는 173편이 됐습니다. 오픈AI는 같은 수정에서 형식화 6건과 보조 결과 5건을 더해, 원고별 주 결과로 세면 719건 가운데 300건(약 42%)이 형식화됐다고 밝혔습니다. 두 숫자는 세는 단위가 다릅니다.

공개 전날 밤 X에는 「오픈AI, 미공개 영화 500편의 마지막 10분 공개」라는 가짜 보도자료를 올린 계정이 있었습니다. 타오는 이 패러디를 매스토돈에 소개했고, 철회 약 10시간 뒤인 10월 9일 0시 14분, 같은 계정에 후속 보도자료가 올라왔습니다.

엔딩 3편을 철회하지만 나머지 497편은 전적으로 신뢰한다는 제목입니다. 본문 속 대변인은 엔딩 3편이 틀렸다는 사실이 시스템이 작동한다는 증거라고 말하고, 틀린 곳을 고쳐 준 무급 자원봉사자들에게 고맙다고 인사합니다. 오류를 알린 사람들이 엔딩을 실제로 봤는데, 회사는 그런 시청을 예상하지도 권하지도 않았다는 문장도 들어 있습니다.

「수학자들은 요청하지 않았다」

성명을 낸 인간수학협회(Association for Human Mathematics, AHM)는 홈페이지에서 스스로를 인공지능의 위협으로부터 인간의 활동으로서의 수학을 지키고, 기업의 이해에서 수학계의 독립을 지키는 단체로 소개합니다. 성명은 오픈AI가 표절과 저작권 침해, 상표 희석 소송을 치르는 중이라는 문장으로 시작합니다. 이어 오픈AI가 정당성의 근거로 내세운 수학과 AI 자문그룹(AGMAI)이 첫 권고문 첫머리에서 공개되지 않은 모델로 고급 수학 문제를 시험하지 말라고 했는데, 오픈AI가 그 전제를 무시했다고 적었습니다.

수학자들은 이 작업을 해 달라고 요청한 적이 없습니다.— 인간수학협회 커뮤니케이션 실무그룹

성명은 700개 넘는 파일을 한꺼번에 내놓은 일을 힘의 과시라고 불렀고, 수학자들에게 오픈AI와의 협업을 그만두라고 촉구했습니다. 타오는 이 성명을 「손님 글」로 자기 블로그에 옮기면서, 원래 다른 파일 형식으로 쓴 글을 AI로 변환해 올렸다는 주석을 달았습니다.

자문그룹의 입장은 더 조심스럽습니다. 미국 시각 10월 6일 낸 짧은 성명에서 자문그룹은 자신들의 자문 역할을 결과의 영향에 대한 판단이나 오픈AI가 결과를 얻은 과정에 대한 승인으로 해석하지 말라고 적었습니다. 이번 공개는 인간이 이해하는 과정의 시작일 뿐이고, 수학 연구의 미래가 AI 연구소가 낸 결과를 이해하는 일로만 채워질 수는 없다는 문장도 들어 있습니다. 권고를 얼마나 잘 따랐는지는 수학계가 평가할 일이라고 맺은 이 성명을 두고, 애런슨은 지지도 비난도 하지 않게 아주 조심스럽게 쓴 글이라고 평했습니다.

타오 자신의 생각은 공개 4시간 전에 이미 나와 있었습니다. 그는 매스토돈에 올린 글 4편에서, 전통적인 「수학 1.0」에서는 난제가 풀리면 강연과 워크숍, 공동 연구가 뒤따르며 증명이 소화되고 교과서에 들어갔다고 설명했습니다. 지금은 분야에 관심 없는 AI 프롬프트 작성자들이 목표한 문제만 풀고 떠나고, 결과를 충분히 이해하지 못해 강연도 질문 응대도 하지 못하는 일이 잦다고 적었습니다.

열린 문제의 해답이 지속할 수 없는 방식으로 대규모로 수확되고 있습니다.— 테렌스 타오, UCLA 수학자 (매스토돈)

한번 풀린 문제는 다시 열린 문제로 되돌릴 수 없고, 해답이 있다는 사실만으로 다른 길을 찾으려는 사람과 AI의 시도가 오염된다는 것이 그의 설명입니다. 그는 이 흐름 때문에 분야 전체가 덜 비옥해진다고 적었습니다.

8월부터 쌓인 공방

반발은 이번에 처음 나온 것이 아닙니다. 8월 1일 오픈AI는 미출시 모델 Astra로 난제 10건을 풀었다고 발표했고, 사이언티픽 아메리칸은 5일 뒤 일부 결과가 기존 논문의 논증을 제대로 인용하지 않았다는 수학자들의 비판을 실었습니다. 예시바대 스티븐 밀러는 자기 2016년 논문의 논증이 오픈AI 결과의 바탕이 됐다며 연구 부정이라고 주장했고, 오픈AI 대변인은 결과의 정확성에 책임을 지며 사람 수학자에게 기대하는 기준을 지키고 있다고 답했습니다.

9월 9일에는 에이전트 약 1만 개를 88시간 돌린 나비에–스토크스 증명이 나왔습니다. 기즈모도는 9월 17일(미국 시각) 디인포메이션 보도를 인용해, 오픈AI 직원들이 곧 호지 추측을 풀 것으로 보면서도 수학자들을 더 화나게 하지 않고 발표할 방법을 고민한다고 전했습니다. 오픈AI는 9월 21일 자문그룹 출범을 알렸고, 자문그룹은 8일 뒤 공개 권고문을 냈습니다. 이번 공개에는 CM 아벨 다양체의 호지 추측 원고가 들어 있었고, 철회된 3편도 호지 추측의 특수한 경우를 겨냥한 원고였습니다.

유일 게임 추측, 무엇을 증명했다고 하나

애런슨의 글은 아홉 살 아들이 엄마에게 「로봇이 엄마가 평생 연구한 문제를 풀었다며」라고 놀렸다는 이야기로 시작합니다. 그 엄마가 텍사스대 오스틴의 이론전산학자 데이나 모시코비츠입니다. 오픈AI의 372개 결과 묶음 가운데 102번 묶음에 그가 오래 매달려 온 유일 게임 추측(Unique Games Conjecture)의 증명 원고가 들어 있습니다.

유일 게임 추측은 수바시 콧이 대학원생이던 2002년 내놓았습니다. 그래프의 꼭짓점에 정해진 팔레트의 색을 칠하되, 변마다 「이쪽이 빨강이면 저쪽은 파랑」처럼 한쪽 색이 정해지면 반대쪽 색이 하나로 정해지는 규칙이 붙어 있습니다. 색의 가짓수를 충분히 크게 잡으면, 규칙의 99%를 지킬 수 있는 그래프에서도 1%를 지키는 칠하기를 찾는 일조차 어려운(NP-난해) 경우가 있다는 것이 추측의 내용입니다. 2008년 프라사드 라가벤드라는 이 추측이 참이면 반정부호 계획법(SDP) 완화에 기반한 알고리즘이 완벽한 해가 없는 모든 제약 만족 문제에서 최선이라는 것을 보였습니다. 최대 절단(Max-Cut)의 고에만스–윌리엄슨 비율(약 0.878)과 정점 덮개의 근사 비율 2를 더 개선할 수 없다는 결론도 그동안 이 추측을 가정해야 얻을 수 있었습니다.

오픈AI의 원고 「The Unique Games Theorem」은 58쪽이고, 원고에 적힌 날짜는 9월 23일입니다. 원고의 주장에 따르면 0과 1/2 사이의 어떤 오차 ε, δ를 고정하든, 3SAT(참·거짓 변수 세 개씩 묶인 논리식을 만족시킬 수 있는지 묻는 대표적인 NP-완전 문제)를 유일 게임으로 바꾸는 결정론적 다항 시간 변환이 있습니다. 만족 가능한 식은 규칙의 1−ε 이상을 지킬 수 있는 게임이 되고, 만족 불가능한 식은 규칙의 δ 넘게는 지킬 수 없는 게임이 됩니다. 색은 이진 벡터 공간 F₂ˢ의 원소이고 모든 규칙은 평행 이동 꼴입니다.

같은 묶음의 다른 원고 4편은 최대 절단과 정점 덮개, Min-UnCut, 유향 되먹임 정점 집합의 근사 난도를 추측을 거치지 않고 직접 증명했다고 주장합니다. 105번 묶음은 콧의 또 다른 추측인 2-to-1 게임 추측을, 모든 규칙을 지킬 수 있는 게임과 거의 지킬 수 없는 게임을 가르는 형태로 증명했다고 주장합니다.

원고 서론은 2018년 콧·민저·사프라의 그라스만 확장 정리와 바라크·코타리·슈토이러의 행렬 쇼트코드를 출발점으로 삼고, 잡음을 비선형 사상으로 바꿨다고 설명합니다. 모시코비츠의 첫 독후감은 혹독했습니다. 애런슨이 옮긴 문자에서 그는 원고가 너무 엉망으로 쓰여 AI 도움 없이는 읽을 수 없고, 롱코드도 쇼트코드도 아닌 외계의 무언가 같은 새 부호를 만들어 냈다고 적었습니다. 그는 하루 종일 GPT-6 Astra에게 증명을 설명하게 했고, 한국 시각 10월 8일 오후 애런슨은 아내가 이제 증명을 대부분 이해했으며 새 아이디어에 감탄해 곧 강연을 하고 싶어 한다고 댓글에 적었습니다.

Lean 인증서가 확인한 것

오픈AI는 이 결과에 Lean 형식 증명을 붙였습니다. 검증용 문장 파일(UniqueGamesTheorem.lean)은 3SAT 식의 이진 부호화와 유일 게임 인스턴스를 직접 정의하고, 다항 시간 계산은 Lean 수학 라이브러리 Mathlib의 튜링 기계 정의로 적습니다. 허용된 공리는 Lean의 표준 공리 세 개(propext, Quot.sound, Classical.choice)뿐입니다. 증명이 든 폴더에는 Lean 파일 478개, 약 8.7MB가 있고, 이름이 KMS로 시작하는 파일들도 있습니다. 표준 공리 말고는 아무것도 허용하지 않으니, 검사를 통과했다면 원고가 외부 입력으로 쓴 콧·민저·사프라 정리 같은 결과까지 Lean 안에서 증명됐다는 이야기가 됩니다.

검사를 실제로 돌려 본 외부 기록은 하나 찾았습니다. 독립 연구자 아리엘 엘보임은 한국 시각 10월 9일 오후 캐글 노트북에서 철회 반영 뒤의 저장소를 받아 Comparator를 약 57분 돌렸고, 「통과」 판정과 표준 공리 세 개만 쓰였다는 기록을 10일 새벽 깃허브에 올렸습니다. 그는 오픈AI 논증을 11쪽으로 줄인 증명과 17쪽 요약본도 함께 냈는데, 둘 다 AI 모델로 준비했고 아직 사람 전문가가 검토하지 않았다고 스스로 적었습니다.

이 검사가 확인하는 범위는 좁습니다. 오픈AI의 형식화 목록 파일에는 검토 상태가 여전히 「미확인」, 형식화 방식은 「에이전트」로 적혀 있습니다. 케플러 추측의 형식 증명을 이끈 수학자 토머스 헤일스는 10일 새벽 타오 블로그 기고에서, Lean 증명은 커널 검사를 거친 뒤에도 정리 문장이 의도한 내용과 같은지 사람이 감사하기 전까지 받아들이면 안 된다고 적었습니다. 그는 올해 7~8월 Lean에서 콜라츠 추측을 거짓으로 「증명」하는 버그 등 여러 건전성 버그가 나왔다가 모두 고쳐졌다는 사실도 짚었습니다. 나비에–스토크스 형식화는 12개가 넘는 검사기로 교차 확인됐는데, 유일 게임 쪽에서 제가 찾은 외부 검사 기록은 엘보임의 한 번입니다.

Lean의 증명은 정리 문장이 충실한지 사람이 감사하기 전에는 받아들이지 말아야 합니다.— 토머스 헤일스, 피츠버그대 수학자 (타오 블로그 기고)

애런슨도 같은 단서를 달았습니다. 그는 증명이 맞다고 꽤 확신한다면서도, 사람 가운데 이 증명들을 이해한 이가 아직 거의 없어 보인다고 적었습니다. 댓글에서 커널 버그를 이용한 가짜 증명일 가능성을 묻자, Lean 커널 버그가 모두 확실히 고쳐지기 전까지는 완전히 배제할 수 없지만 확률은 매우 낮다고 답했습니다.

사람이 먼저 내놓은 결과

이 추측을 둘러싼 사람의 경주도 있었습니다. 퀀타 매거진에 따르면 MIT의 도르 민저는 9월 11일 아침 오픈AI가 유일 게임 추측을 풀었다는 소문을 들었습니다. 그와 대학원생 두 명(Yumou Fei, Shuo Wang)은 콧의 4-to-1 게임 추측을 증명하고 원고를 쓰던 중이었고, 3일 뒤인 9월 14일 95쪽 원고를 계산 복잡도 논문 저장소 ECCC에 서둘러 올렸습니다. 첫 쪽에는 수학적으로는 완결됐지만 아직 보여 주고 싶은 꼴로 다듬지 못했다는 양해의 글을 달았습니다.

이 결과로 3가지 색으로 칠할 수 있는 그래프를 몇 가지 색을 쓰든 제대로 칠하기 어렵다는, 수십 년 묵은 문제가 풀렸습니다. 프린스턴대 마크 브레이버먼은 크레용 한 상자를 다 써도 안 된다고 표현했습니다. 같은 원고는 한국 시각 10월 9일 새벽 arXiv에도 올라왔습니다. 오픈AI 묶음에는 이보다 강한 2-to-1 게임 추측 증명이 Lean과 함께 들어 있지만, 퀀타는 그 원고가 사람의 편집도 독립 전문가의 검토도 거치지 않았다고 적었습니다.

실패해 보고 왜 실패했는지 아는 데 큰 가치가 있습니다.— 도르 민저, MIT 교수 (퀀타 매거진)

민저는 AI를 쓰면 그 과정이 통째로 빠진다고 덧붙였고, 잠도 자고 밥도 먹는 사람이 1조 달러짜리 회사에 결과를 빼앗길지 모른 채 긴 연구를 이어 가야 한다는 걱정도 털어놓았습니다. 카네기멜런대 라이언 오도널은 민저 팀을 두고 머리로 풀고 자기 손가락으로 썼다고 평했습니다. 애런슨과 그레그 쿠퍼버그가 2007년 제기한 유니터리 합성 문제에 3년을 쏟은 닥쉬타 쿠라나도 10월 8일 블로그에서, 문제가 아직 열려 있는 세계에 조금 더 머물고 싶은 마음과, 다른 사람의 길로 올랐어도 정상에서는 새 산이 보인다는 마음을 함께 적었습니다.

오픈AI 방식과 앤트로픽 방식

애런슨은 같은 글에서 다른 공개 방식을 하나 나란히 놓았습니다. 오픈AI 공개 하루 전인 한국 시각 10월 6일 새벽, 조시 앨먼과 버지니아 바실레프스카 윌리엄스가 3SUM(정수 n개 가운데 합이 0인 세 수를 찾는 문제)과 모든 쌍 최단 경로(APSP)를 교과서 알고리즘보다 다항식만큼 빠르게 푸는 76쪽 논문을 arXiv에 올렸습니다. 실행 시간은 각각 O(n^1.9992)과 O(n^2.9995)이고, 논문 서두에는 3SUM·APSP 가설을 깨는 알고리즘을 Claude가 찾았다고 적혀 있습니다.

논문 끝의 경위에 따르면 앤트로픽 직원이 암호학의 열린 문제를 내부 연구 모델에 맡겼는데, Claude는 받은 구성을 검증하고 개선하는 대신 이 알고리즘을 만들었습니다. 그 세션은 사람 입력 없이 출력 토큰 1,600만 개를 썼습니다. 앤트로픽은 9월 비밀 유지 계약 아래 두 저자에게 알고리즘을 넘기며 보상과 공개 버전 Claude 사용을 제안했고, 저자들이 이해하고 단순화하고 확장해 논문을 썼습니다.

애런슨은 앞의 방식이 사람들 사이에 지저분한 AI 증명을 먼저 소화하는 경주를 붙이고, 뒤의 방식은 어떤 수학자가 AI의 대변인이 될지를 회사가 고르게 만든다고 정리했습니다. 둘 다 장단점이 있다며 독자에게 의견을 물었습니다.

「누구에게나 열린 문제」

애런슨은 성명에 동의하지 않았습니다. 그는 10월 9일(미국 시각) 덧붙인 글에서 「요청하지 않았다」는 문장을 짚으며, 하디가 라마누잔에게 누가 이 이상한 항등식들을 증명해 달라고 했느냐고 묻는 꼴이라고 받아쳤습니다. 수학계가 AI 회사를 압박하는 일은 지지하지만, 우리 재미를 망치지 않게 AI로 열린 문제를 풀지 말라는 입장은 지킬 수 없다는 것이 그의 주장입니다. 수학 문제는 미움받는 회사를 포함해 누구에게나 열려 있고, 그런 능력은 GPT나 Claude 구독자에게 금세 퍼진다는 이유를 들었습니다. 토론토대 대니얼 리트도 사이언티픽 아메리칸에 답을 알고 싶다면 회사에 비밀로 해 달라고 할 이유가 없다고 말했습니다.

UCLA의 라구 메카는 타오 블로그 기고에서 AI가 낸 해답 가운데 일부는 훌륭하지만 아주 낯설지는 않다고 적었습니다. 그런데도 소수 연구자 말고는 거의 시도를 멈춘 문제들이었다며, 이름난 수학자들이 실패했다는 평판이나 전해 내려오는 한계 때문에 스스로 장벽을 그려 왔을 수 있다고 돌아봤습니다.

YouTube 영상 · 누르면 재생

한국 시각 10일 오전 공개된 All-In 팟캐스트는 23분을 이 일에 썼습니다. 데이비드 프리드버그는 아마 인류 역사에서 가장 큰 발견의 날이라고 했고, 인간수학협회의 성명을 두고는 직업을 지키려는 시각이라고 평했습니다. 차마스 팔리하피티야는 반론을 맡아, 이번에 풀린 문제들은 과학자들끼리 중요하다고 여겨 온 아주 좁은 지적 탐구 영역이고 암 치료나 초음속 비행기로 곧장 이어지지는 않는다고 말했습니다. 그는 이번 일로 드러난 것은 코드에 이어 수학도 완전히 검증할 수 있는 분야라는 사실이라고 덧붙였습니다.

숫자도 말이 옮겨 갈수록 달라졌습니다. 오픈AI README는 모델에 약 4,000문제를 던졌다고 적었는데, 애런슨은 본문에 약 8,000문제를 시도해 5% 정도를 풀었다고 적었습니다. 결과 대부분이 같은 절차로 나왔고 결과 하나에 평균 ChatGPT Pro 사고 연산 3시간이 들었다는 오픈AI의 설명과, 거의 모든 결과가 에이전트 하나에 프롬프트 하나로 나왔다는 대변인의 말은 모델이 공개되지 않아 아직 누구도 재현할 수 없습니다.

다음에 나올 것

모시코비츠는 유일 게임 증명을 대부분 이해했다며 곧 강연을 하고 싶다고 했지만, 날짜는 아직 나오지 않았습니다. 오픈AI는 결과를 이해하도록 돕는 워크숍과 학회를 지원하겠다고 했고, 모델 공개 시점은 밝히지 않았습니다. 저장소 README에는 수정과 철회를 새 판으로 기록하고 이전 판도 남기겠다는 약속이 적혀 있어, 앞으로의 철회와 수정도 history.md에서 확인할 수 있습니다.

소식·12분 읽기AI"사람이었다면 필즈상" 준리만 가설까지, 오픈AI 수학 원고 722편 공개오픈AI가 10월 7일 아침(한국 시각) 내부 모델이 쓴 수학 원고 722편을 깃허브에 공개했습니다. 약 4,000문제에서 나온 결과 묶음 372개로 준리만 가설 증명 주장까지 담겼고, 162편은 주 결과를 Lean으로 형식화했습니다.읽기

국내 연구자도 원고와 Lean 파일을 바로 받아 볼 수 있습니다. 아파치 2.0으로 풀려 있어 누구나 Comparator를 직접 돌려 볼 수 있고, 엘보임이 공개한 검사 스크립트도 참고할 수 있습니다. 원고를 받아 줄 쪽의 사정도 달라졌습니다. 수학자들이 원고를 올리는 arXiv는 10월부터 제출자 한 사람당 한 달에 2편으로 제한했고, 오픈AI의 719편은 그 바깥인 회사 깃허브에 있습니다. 같은 주 타오 블로그에는 수학자의 길을 계속 가도 되는지 묻는 학부생의 편지와, 그래도 수학 공부를 이어 가라는 수학자 알바로 로사노로블레도의 답장이 실렸습니다.

읽어 주셔서 고맙습니다.

초이 드림