오픈AI가 내부 최전선 모델이 만들어낸 수학 논문 722편을 공개했다. 정작 그 모델의 이름도, 가격도, API도 공개되지 않았다. 외부 검증은 아직 이뤄지지 않았다.
오픈AI가 722편을 공개한 방식
10월 6일 오픈AI는 깃허브에 'openai/math' 저장소를 열고, '수학 분야 AI 진전 공유'라는 글을 함께 발표했다. 저장소에는 수학 논문 722편이 담겼고, 이는 372개 연구 계열(family)로 묶인다. 회사는 이 결과가 수학과 이론 컴퓨터과학의 중요한 미해결 문제를 해결하거나 실질적으로 진전시켰다고 밝혔다.
논문을 만든 것은 오픈AI의 내부 최전선 모델이다. 이름이 붙지 않았고, 가격도 API도 공개되지 않았다. 오픈AI는 앞으로 이 모델을 책임 있게 공개하기 위해 준비 중이라고만 설명했다.
'이름 없는 모델'이 핵심인 이유
그럼 논문을 쓴 모델은 무엇일까? 이번 발표에서 가장 눈에 띄는 건 결과의 양이 아니라 주체다. 논문을 쓴 모델이 정체를 드러내지 않는다. 어느 모델이, 어떤 설정으로, 얼마의 컴퓨팅을 써서 이 결과를 냈는지 개발자는 알 수 없다. 오픈AI는 결과를 만든 모델을 조만간 공개하겠다고 했지만 시점은 밝히지 않았다.
대신 회사는 결과에 이르는 과정 일부를 공개했다. 모델의 추론 과정을 요약한 10편의 자료와, 챗GPT 프로 사용량 기준으로 환산한 컴퓨팅 추정치, 시도한 문제 수 통계를 함께 올렸다. 평균적으로 결과 하나에 챗GPT 프로 추론 약 3시간 분량의 컴퓨팅이 들어갔다고 한다.
Lean 형식화로 컴퓨터가 검증하게 하다
오픈AI가 함께 올린 것이 린(Lean) 형식화다. 린은 수학 증명을 컴퓨터가 검사할 수 있게 만든 프로그래밍 언어다. 자연어로 쓴 논증을 논리 구조로 바꿔, 사람이 아니라 프로그램이 맞는지 확인하게 하는 방식이다.
저장소에는 많은 증명의 린 형식화가 들어 있다. 회사는 더 많은 형식화를 확보하는 대로 저장소를 갱신하겠다고 밝혔다. 린 형식화는 이 묶음에서 가장 강한 형태의 근거로 꼽힌다. 컴퓨터가 검증한 부분이라면 사람이 일일이 따라가며 확인할 필요가 줄어들기 때문이다.
다만 형식화되지 않은 논문도 있다. 저장소의 형식화 목록에는 주요 결과가 형식화된 논문만 올라 있다. 모든 주장이 컴퓨터 검증을 거친 건 아니다.
수학계에 던진 파장
오픈AI는 결과 공개 방식에 대해 미고등연구소(IAS)의 수학·인공지능 자문단과 협의해 왔다고 밝혔다. 자문단의 공개 권고를 참고해 저장소 형태로 결과를 내놓았다는 설명이다.
일부 보도에서는 오픈AI가 나비에-스토크스 방정식의 밀레니엄 난제에 대한 AI 생성 풀이도 함께 공개했다고 전한다. 다만 이런 개별 주장의 수학적 타당성은 아직 독립적으로 검증되지 않았다.
일반 독자에게 무슨 의미인가
수학 난제 해결은 당장 일상과 거리가 멀어 보인다. 하지만 이번 발표가 남기는 신호는 분명하다. AI가 사람이 이해할 수 있는 형태로, 검증 가능한 수학 결과를 대량으로 만들어내기 시작했다는 점이다.
동시에 한계도 드러난다. 결과를 만든 모델이 공개되지 않았고, 외부 검증도 이뤄지지 않았다. "AI가 난제를 풀었다"는 주장과 "그 풀이가 맞다고 독립적으로 확인됐다"는 사실 사이에는 아직 거리가 있다.
앞으로 지켜볼 것
첫째, 이름 없는 모델의 정체다. 오픈AI가 언제 어떤 형태로 이 모델을 공개하는지가 관건이다. 둘째, 외부 검증이다. 수학자들이 린 형식화를 직접 실행해 어떤 결과가 통과하고 어떤 결과가 걸리는지 확인하는 절차가 남아 있다. 오픈AI는 관련 워크숍과 학회, 프로그램을 지원하겠다고 밝혔다.
