OpenAI, 미출시 Astra 모델의 수학 결과 372건을 GitHub에 추가 공개

뉴스 요약

OpenAI가 GitHub에 훨씬 더 큰 규모의 두 번째 수학 결과 묶음을 공개했습니다. 총 372건의 명제로, 모두 회사가 차기 주요 출시작이라 부르는 내부 모델 Astra의 성과로 알려져 있습니다. 미국 동부 시간 기준 2026년 10월 6일 보도에 따르면, 각 결과는 수학 또는 이론 컴퓨터 과학 분야의 미해결 문제를 해결하거나 크게 진전시킨 것으로 전해집니다. 많은 결과가 Lean 프로그래밍 언어로 작성된 기계 검증 가능 증명을 포함하고 있지만, 모델 자체가 아직 공개되지 않아 외부 연구자들은 해당 결과가 어떻게 도출되었는지 재현할 수 없는 상황입니다.

OpenAI가 공개한 내용

이번 새 공개는 미국 동부 시간 기준 2026년 8월 1일에 발표된 OpenAI의 첫 번째 공지 "수학 및 이론 컴퓨터 과학 분야의 10가지 진전" 이후 약 두 달 만에 이루어졌습니다. 첫 번째 묶음은 군론, 연산자 대수, 코딩 이론, 극단 조합론을 포함한 8개 분야에 걸친 오랜 난제 10개를 다루었습니다. 당시 249쪽 분량의 원고와 Lean 4 인증서가 공개 GitHub 저장소에 함께 제공되었으며, OpenAI는 사용된 토큰 비용이 자사 API 요금 기준으로 약 2,000달러에 해당한다고 밝혔습니다.

10월 공개분은 이전보다 37배 이상 규모가 큽니다. 보도에 따르면 372건의 결과가 포함되었으며, 여기에는 4차원 카케야 추측의 해결, 널리 사용되는 일부 컴퓨터 알고리즘의 개선, 리만 가설과 관련된 부분적 진전이 포함된 것으로 알려졌습니다. OpenAI는 거의 모든 결과가 단일 AI 에이전트에 입력된 단 하나의 프롬프트에서 나왔다고 설명합니다. 회사는 개별 프롬프트나 결과별 연산량은 공개하지 않고 평균 연산 시간만 밝혔습니다.

Lean 증명이 중요한 이유

Lean은 증명 보조 도구로, 증명의 모든 논리적 단계를 기계적으로 검사하는 프로그램입니다. 어떤 결과가 Lean으로 형식화되면 독자는 저자를 믿을 필요가 없습니다. 소프트웨어가 증명을 받아들이거나 거부하기 때문입니다. Scientific American은 Lean 검증이 완료된 증명은 사실상 정확하다고 볼 수 있다고 보도했습니다.

이는 컴퓨터가 검사하는 수학이 어떻게 작동하는지 보여주는 유용한 교육 사례입니다. Lean 증명은 특정 명제가 그 가정으로부터 도출됨을 보장합니다. 그러나 그 명제가 인간 독자가 의도한 의미대로 형식화되었는지는 보장하지 않으며, 증명이 어떻게 발견되었는지에 대해서는 아무런 정보도 제공하지 않습니다.

수학자들의 반응

반응은 엇갈리고 있습니다. MIT의 Andrew Sutherland는 모델이 공개되어 다른 이들이 작업을 재현할 수 있을 때까지, 단일 에이전트로 한 번에 문제를 해결했다는 주장은 검증되지 않은 것으로 취급해야 한다고 말했습니다. 토론토 대학교의 Daniel Litt은 학계가 이러한 문제들의 답을 원한다면, 그 해답을 만들어낼 수단을 한 기업이 쥐고 있도록 의존할 이유가 거의 없다고 주장했습니다. Terence Tao는 현재 AI 연구소들이 결과를 생성해 내는 속도를 비판하며 이를 "미쳤다"고 표현했습니다.

Scientific American은 또한 OpenAI가 독립 자문단의 권고를 완전히 따르지 않았으며, 일부 결과는 여러 차례의 시도가 필요했을 수 있고, 일부 내용은 OpenAI 소속 수학자들조차 아직 이해하지 못하고 있다고 지적했습니다. 수백 건의 결과를 검토하는 일은 인간 전문가 집단에게도 무거운 부담입니다.

첫 번째 공개분에서 불거진 인용 논란

미국 동부 시간 기준 2026년 8월 6일, Scientific American은 일부 전문가들이 처음 공개된 10건의 결과 중 2건에서 Astra가 선행 연구를 제대로 인용하지 못했다고 지적했다고 보도했습니다. 예시바 대학교의 Stephen Miller는 자신의 2016년 연구에 나온 구 쌓기 논증이 마치 새로운 것인 양 제시되었다고 말했습니다. 군론의 소픽성에 관한 또 다른 결과는 2016년과 2019년에 발표된 논문들의 아이디어를 충분한 출처 표기 없이 결합한 것으로 알려졌습니다. 케임브리지 대학교의 Francesco Fournier-Facio는 이번 공지가 최근의 중요한 연구 동향을 간과했다고 지적했고, 드레스덴 공과대학교의 Andreas Thom은 해당 군론 증명이 창의적이면서도 동시에 기초적인 수준이라고 평가했습니다.

OpenAI는 이러한 문제를 인정했습니다. 대변인은 회사가 일반적인 학술 관행에 따라 해당 주 내에 소규모 수정을 진행할 것이라고 밝혔습니다.

앞으로 주목할 점

세 가지 질문이 이번 결과들이 어떻게 받아들여질지를 결정할 것입니다. 첫째, 372건의 명제 중 몇 건이 독립적인 검토를 통과해 정식 문헌으로 인정받을 것인가. 둘째, OpenAI가 Astra를 공개하여 단일 프롬프트 주장을 검증할 수 있게 할 것인가. 셋째, 해당 학계가 선행 연구 인용과 AI 지원 발견에 대한 기여 인정 규범을 마련할 것인가. 학생과 교육자에게 이번 사안은 형식 검증이 지닌 가능성과 인간 동료 검토가 여전히 필요하다는 점을 모두 보여줍니다.

출처 참고 사항

조사 과정에서 이번 공개에 관한 The Verge의 보도는 확인할 수 없었으므로, 위 세부 내용은 Scientific American 및 OpenAI의 8월과 10월 공지를 다룬 기타 보도에서 발췌했습니다. 특정 결과에 대한 주장은 OpenAI 측에서 나온 것이며, 모두 독립적으로 확인된 것은 아닙니다.