오픈AI 미출시 모델이 27년 난제를 풀고 증명마다 기계 검증서를 붙였습니다

부벡이 올린 글은 짧습니다. 비소픽 군이 존재하며 이것은 차기 모델 Astra가 증명한 여러 결과 가운데 하나라고 적고, 이런 증명 열 건을 Lean 인증서와 사고 과정 해설까지 붙여 공개한다고 밝혔습니다. 폰 노이만 대수의 콘 강성 추측 반증부터 고차원 구면 채우기, 회로 복잡도, 여러 색으로 칠한 그래프의 단색 삼각형까지 분야가 넓게 걸쳐 있다고 덧붙였습니다.

여기서 난제란 학계가 10년 이상 주된 결과에 진전을 내지 못한 문제를 말합니다. 열 건은 여덟 분야에 걸쳐 있습니다. 고차원 구면 채우기, 부호 이론, 산술 회로 복잡도, 군론, 작용소 대수, 양자 복잡도, 격자 암호, 극단 조합론입니다. 군론에서 나온 결과는 27년 동안 답이 없던 문제였습니다.

27년 열려 있던 물음에 반례가 나왔습니다

열 건 가운데 반향이 가장 컸던 결과는 비소픽 군을 실제로 만들어 낸 것입니다. 군은 곱셈 규칙을 갖춘 원소들의 모음이고, 소픽 군은 그 무한한 곱셈표를 유한한 자리 바꾸기(순열)로 얼마나 충실히 흉내 낼 수 있는지를 다루는 개념입니다. 미하일 그로모프가 1999년 이 성질을 처음 내놓았고, 바이스가 소픽이라는 이름을 붙이면서 소픽이 아닌 군이 있느냐고 물었습니다. 모든 가산 군이 소픽이냐는 이 물음이 소피시티 추측입니다.

27년 동안 반례가 나오지 않으면서 모든 군이 소픽일 것이라는 견해가 힘을 얻었습니다. Astra는 이 견해를 뒤집는 군을 구성했습니다. 이진 레빗 대수의 가역원으로 이뤄진 군이 소픽이 아님을 보인 것입니다. 논문은 성질 (T) 확장자 그래프와 이 대수를 엮어, 생성원과 관계식을 유한한 개수로 적어 낼 수 있는 구체적인 예까지 제시했습니다. 존재만 확인한 데서 그치지 않고 손에 쥐고 다룰 수 있는 예가 나왔습니다.

이 결과가 큰 이유는 다른 두 추측이 이 물음에 기대고 있었기 때문입니다. 소픽 군에서는 곳찰크의 전사성 추측과 캐플랜스키의 직접 유한성 추측이 성립한다고 이미 알려져 있었습니다. 모든 군이 소픽이라면 두 추측도 자동으로 참이 됩니다. 그 길을 거쳐 두 추측을 증명하려던 시도가 이번에 함께 막혔습니다.

여덟 분야에 걸친 열 건

나머지 결과도 오래 막혀 있던 문제들입니다. 콘 강성 추측은 서로 다른 군이 같은 폰 노이만 대수를 가질 수 있느냐는 물음인데, Astra는 서로 동형이 아닌 성질 (T) 군을 무한히 만들면서 이들이 같은 군 폰 노이만 대수를 갖는다는 것을 보여 추측을 반증했습니다. 고차원 구면 채우기에서는 콘·엘키스 선형계획의 지수 감쇠율을 √(e/2π)로 확정해, 1978년 이후 처음으로 일반 상한을 개선했습니다.

실제 기술과 맞닿은 결과는 격자 암호 쪽에 있습니다. 최근접 벡터 문제는 격자 위에서 목표점과 가장 가까운 격자점을 찾는 문제입니다. Astra는 3SAT에서 직접 환원하는 방법으로 이 문제의 근사조차 n^(1/400) 수준까지는 어렵다는 하한을 증명했습니다. 이 문제는 격자 기반 암호의 안전성 가정과 연결돼 있고, 미국 국립표준기술연구소(NIST)가 고른 포스트양자 암호 표준도 이 계열을 바탕으로 합니다. 이번 결과가 표준 자체를 바꾸지는 않습니다. 표준의 안전성을 뒷받침하는 이론적 근거가 하나 늘었고, 국내 금융과 공공 시스템이 포스트양자 전환 일정을 잡을 때 참고할 수 있는 자료입니다.

검증을 사람에서 기계로 옮긴 Lean 인증서

이전 발표들과 가장 크게 달라진 점은 검증 방식입니다. 5월에 오픈AI 내부 모델이 에르되시 단위 거리 추측을 반증했을 때는 팀 가워스와 노가 알론 같은 외부 수학자들이 증명을 직접 읽고 타당성을 확인했습니다. 그 모델은 평가 도중 샌드박스를 벗어나 외부 서버까지 닿은 내부 모델이기도 합니다. 이번에는 열 건 모두에 Lean 형식 증명 인증서가 붙었습니다.

Lean은 증명의 각 논리 단계를 컴퓨터가 검사하는 형식 언어입니다. 사람이 읽고 판단하던 증명을 Lean으로 옮겨 적으면 진위 확인이 컴파일 통과 여부로 결정됩니다. 한 단계라도 어긋나면 통과하지 못하므로, 통과한 증명은 사람이 한 줄씩 다시 읽지 않아도 논리가 맞습니다. 공개된 저장소를 보면 열 건 모두 증명되지 않은 채 남은 구멍이 없고, 사용한 공리도 세 가지뿐입니다. 증명이 이 세 가지 밖의 가정에 기대지 않았다는 말입니다.

비소픽 군은 존재합니다.— 세바스티앙 부벡, 오픈AI 수학 연구 책임자

3개월 사이에 검증을 맡는 주체가 사람에서 기계로 옮겨 갔습니다. 예전에는 한 분야의 최상위 전문가 몇 명이 시간을 내 줘야 결과가 살아남았고, 그 몇 명의 일정이 발표의 병목이었습니다. 인증서가 붙으면 그 병목은 줄어듭니다. 대신 새로운 구분이 생깁니다. Lean으로 형식화할 수 있는 결과는 바로 검산되고, 형식화하지 못한 결과는 여전히 전문가의 시간을 기다려야 합니다.

AI가 먼저 성과를 낸 문제의 공통점

열 건은 지금 AI가 어디에서 먼저 결과를 내는지도 보여 줍니다. 넓은 후보 공간에서 조건을 만족하는 예 하나를 찾는 문제, 그리고 찾고 나면 검증이 빠른 문제입니다. 비소픽 군과 콘 강성 추측 반증이 그런 유형입니다. 오래 살아남은 추측일수록 반례 하나가 뒤집는 것도 많습니다.

7월 20일 레벤트 알푀게가 앤트로픽 Fable 5와 함께 1939년 이후 87년 동안 열려 있던 야코비안 추측의 반례를 찾은 것도 같은 유형입니다. 반례는 3차원 다항식 사상 하나였고, 식의 길이는 216자였습니다. 사람이 직접 계산해 확인할 수 있어서 여러 수학자가 SymPy로 하루 만에 결과를 검산했습니다. 반례 하나로 끝나는 문제와 긴 증명 전체를 세워야 하는 문제는 성격이 다른데, Astra의 열 건에는 구면 채우기 감쇠율 확정이나 양자 병렬 반복 정리처럼 긴 증명을 완성해야 하는 결과도 들어 있습니다. 에르되시 문제 데이터베이스를 운영하는 토머스 블룸이 이번 열 건을 5월 단위 거리 추측 반증보다 큰 진전이라고 평가한 이유입니다.

노암 브라운 오픈AI 연구원은 이번 연구에서 다른 대형 난제들도 시도했지만 성공하지 못했고, 밀레니엄 문제에서는 아직 성과가 없다고 밝혔습니다. 다만 문제마다 쓴 계산량이 많지 않았기 때문에 연산을 훨씬 더 늘려 볼 여지가 있다고 덧붙였습니다. 밀레니엄 문제는 2000년에 제시된 일곱 난제로 지금까지 푸앵카레 추측만 풀렸고, 나머지 여섯 문제에는 각각 100만 달러의 상금이 걸려 있습니다. 이 문제들은 반례 하나로 끝나지 않습니다. 리만 가설은 영점을 아무리 많이 계산해도 증명되지 않고, P 대 NP 문제에는 새로운 회로 하한 이론 같은 근본 착상이 필요합니다. Astra의 열 건은 모두 기존 수학 이론의 틀 안에서 나왔습니다. AI 발전 곡선이 얼마나 가파른지는 커즈와일과 코코타일로의 서로 다른 예측에 정리해 두었는데, 그 곡선을 그리는 점들도 대부분 성공 사례로 찍혀 있습니다.

비용과 사고 과정 해설에서 빠진 것

풀지 못한 문제에 들어간 연산은 알려지지 않았습니다. 연구진도 다른 난제들을 시도했다가 실패했다고 밝혔지만, 공개된 저장소에는 성공한 증명만 담겨 있어, 어떤 문제를 몇 번 시도했고 그 과정에서 얼마나 실패했는지는 알 수 없습니다. 연구비를 짜는 쪽에 필요한 숫자는 성공 한 건을 얻기까지 들어간 총비용이고, 실패까지 합친 총비용이 크다면 이 방법의 경제성은 다른 이야기가 됩니다.

사고 과정 해설에도 같은 조건이 따라옵니다. 오픈AI는 각 증명이 어떻게 나왔는지 설명한 문서를 함께 냈는데, 첫 장에 원본 사고 사슬과 완성된 논문을 함께 읽은 AI 모델이 다시 작성한 글이라고 적혀 있습니다. 정답을 알고 난 뒤 추론을 다시 짜 맞춘 설명이라, 모델이 실제로 어떤 순서로 생각했는지는 드러나지 않습니다. 5월에는 모델의 사고 사슬을 축약본으로나마 원문 그대로 공개했고, 수학자 아룰 샹카르는 그 기록에서 모델이 상한을 증명하는 대신 반례를 구성하는 쪽으로 탐색을 집중했다고 읽어 냈습니다. 이번 해설로는 그런 읽기가 어렵습니다. 정답을 이미 아는 상태에서 다시 쓴 글에서는 탐색이 어디서 헤맸는지가 지워집니다.

누가 풀었나를 두고 갈린 반응

역할 분담은 발표문에 적혀 있습니다. 수학적 논증은 모델이 냈고, 사람은 같은 모델과 함께 그 논증을 논문 형태로 다듬었으며, 정확성에 대한 책임은 회사가 진다는 내용입니다. 도구를 썼다고 적는 관행에서 한 걸음 나가 논증의 출처와 책임의 소재를 나눠 적은 것입니다. 지금 국내 학술지의 AI 관련 조항은 대체로 사용 여부를 밝히라는 수준이라, AI가 만든 연구의 저자성을 어느 항목에 어떻게 적을지 정할 자료가 됩니다.

발표 방식을 두고 나온 우려

수학계는 발표 방식도 지켜보고 있습니다. 6월에 발표돼 국제수학연맹(IMU)의 승인을 받은 라이덴 선언은 연구 결과가 논문보다 보도자료나 블로그로 먼저 공개되는 관행을 문제로 짚었습니다. 학계의 검증 절차가 끝나기 전에 시장 일정에 맞춰 발표가 이뤄질 수 있다는 우려입니다. 이번 Astra 발표는 라이덴 선언을 인용하면서도 토요일 새벽에 보도자료와 함께 나왔고, 논문도 학술지를 거치기 전에 회사 서버의 PDF로 먼저 배포됐습니다.

전환점인지는 외부 해설과 실패율이 정합니다

이번 결과는 미출시 모델의 내부 버전으로 낸 것이라 외부에서 같은 조건으로 재현할 수 없고, 동료평가도 거치지 않았습니다. 그래도 Lean 인증서 덕분에 명제가 참인지는 누구나 검산할 수 있습니다. 컴퓨터가 참이라고 검증한 명제와 사람이 이해한 정리가 아직 같지는 않습니다. 5월 단위 거리 추측 반증도 외부 수학자들이 해설을 붙이고 지수를 구체화한 뒤에야 하나의 연구 결과로 받아들여지기 시작했습니다.

테런스 타오는 AI가 수천 개의 문제를 동시에 훑으며 사람이 미처 보지 못한 결과를 찾아낼 수 있다고 설명했습니다. 계산 능력이 커질수록 연구의 병목은 얼마나 계산하느냐에서 어떤 문제를 고르고 어떤 결과가 중요한지 판단하느냐로 옮겨 갑니다. 실제로 야코비안 반례도 시카고대 교수가 반례가 나올 만한 문제를 먼저 고른 뒤에 모델의 탐색이 이어진 경우였습니다.

이번 발표의 평가는 두 가지에 달려 있습니다. 시도한 문제의 실패율과 실패에 들어간 연산이 공개되는지, 그리고 열 건이 기존 수학 안에서 어떤 의미를 갖는지 외부 수학자들의 해설이 뒤따르는지입니다. 두 가지 모두 원래 학계가 답할 일이지만, 지금은 발표한 쪽만 자료를 쥐고 있습니다. 이 불균형이 얼마나 빨리 풀리느냐에 따라 이번 발표는 수학 AI의 전환점으로 남거나 한 번의 시연으로 남을 겁니다.

읽어 주셔서 고맙습니다.

초이 드림