오픈AI의 미공개 모델 '아스트라', 단돈 2천 달러로 27년 수학 난제를 풀다

오픈AI가 아직 출시하지 않은 차세대 모델 '아스트라(Astra)'를 통해 수학계와 이론전산학계가 수십 년간 풀지 못한 난제 10개를 해결했다고 발표했다. 단순한 주장이 아니라 형식 증명 언어 '린(Lean) 4'로 기계 검증까지 마친 결과물을 함께 공개하면서, 학계와 AI 업계 모두에서 큰 관심을 받고 있다.

비공개 모델 아스트라는 무엇인가

아스트라는 오픈AI가 "다음 주요 모델"이라고만 소개했을 뿐 정식 출시 일정은 밝히지 않은 모델이다. 오픈AI 수학 연구를 이끄는 세바스티앙 뷔벡은 자신의 소셜미디어에서 아스트라를 "여러 에이전트가 장시간 협업하며 긴 작업을 수행하도록 만들어진 모델 계열"이라고 설명했다. 단발성 질문에 답하는 방식이 아니라, 여러 에이전트가 오랜 시간 문제를 나눠 맡아 탐색하고 검증하는 구조라는 뜻이다. 업계에서는 이를 두고 차기 플래그십 모델, 이른바 'GPT-6' 계열의 예고편이 아니냐는 추측도 나온다.

27년 만에 답을 찾은 '비소픽군' 문제

아스트라가 해결한 10개 문제 중 가장 주목받는 것은 '비소픽군(non-sofic group)'의 명시적 구성이다. 소픽군이란 유한한 순열 시스템으로 근사할 수 있는 군을 말하는데, 1999년 수학자 미하일 그로모프가 이 개념을 제시한 이후 "모든 가산 이산군이 소픽군인가"라는 질문은 27년간 군론의 핵심 미해결 과제로 남아 있었다. 아스트라는 이 질문에 대한 반례, 즉 소픽하지 않은 군을 실제로 구성해 보임으로써 답을 내놓았다.

콘느 강성 추측의 반증

두 번째로 꼽히는 성과는 필즈상 수상자 알랭 콘느가 1980년 제기한 '콘느 강성 추측'에 대한 반증이다. 폰 노이만 대수 분야의 오래된 질문으로, 이 역시 수십 년간 뚜렷한 진전이 없었던 주제다. 이 밖에도 고차원 구 채우기(sphere packing) 문제에서 1978년 이후 처음으로 개선된 지수를 제시했고, 산술 회로 복잡도, 다색 그래프의 단색 삼각형 문제, 양자 병렬 반복 정리 등 이론전산학 전반에 걸친 결과를 함께 내놓았다.

어떻게 검증했나 - 린 인증서와 249쪽 논문

오픈AI가 이번 발표에서 특히 강조한 부분은 검증 가능성이다. 각 증명마다 기계로 확인할 수 있는 린 4 인증서를 함께 공개했고, 추론 과정을 보여주는 사고 과정(chain-of-thought) 기록도 첨부했다. 전체 내용은 249쪽 분량의 논문으로 정리돼 깃허브에 공개됐다. AI가 내놓은 답을 사람이 다시 일일이 검산하는 대신, 형식 증명 시스템이 논리적 오류 여부를 기계적으로 판정할 수 있게 한 것이다.

비용은 단 2천 달러

더 눈길을 끄는 대목은 비용이다. 오픈AI에 따르면 열 개 문제를 모두 푸는 데 든 총 연산 비용은 자사 API 요금 기준으로 약 2천 달러에 불과했다. 박사급 연구자 여러 명이 수년에 걸쳐 매달려도 풀릴지 장담할 수 없던 문제들을, 커피값 수준의 비용으로 해결했다는 점에서 연구 생산성 측면의 파급력이 크다는 평가가 나온다.

학계의 반응은 엇갈린다

반응은 호평과 신중론이 함께 나온다. 필즈상 수상자 팀 가워스는 공개된 증명 중 하나에 대해 "망설임 없이 정상급 수학 저널에 게재를 추천했을 것"이라고 평가했다. 반면 일부 연구자들은 오픈AI가 문제를 선정한 기준, 즉 AI가 풀기 유리한 유형의 문제만 골랐을 가능성이나 결과의 재현성에 대한 의문을 제기하고 있다. 린으로 검증됐다는 사실이 증명의 정확성은 보장하더라도, '아스트라가 실제로 얼마나 자율적으로 문제를 풀었는가'는 별개의 질문이라는 지적이다.

• 비소픽군 명시적 구성 - 27년 만의 해답
• 콘느 강성 추측 반증 - 1980년 이후 미해결
• 고차원 구 채우기 지수 개선 - 1978년 이후 첫 진전
• 산술 회로 복잡도, 양자 병렬 반복 정리 등 다수 결과 포함

왜 지금 공개했나

이번 발표 시점도 눈여겨볼 부분이다. 구글 제미나이의 '딥씽크'가 수학·추론 벤치마크에서 두각을 나타내고, 중국의 오픈소스 모델들도 빠르게 격차를 좁히는 상황에서, 오픈AI가 아직 정식 출시하지 않은 모델의 잠재력을 미리 보여주는 전략으로 풀이된다. 정식 제품이 아니라 "이 정도 능력을 갖춘 모델을 준비 중"이라는 예고 형태로 공개함으로써 경쟁사와의 기술 격차를 부각하려는 의도가 담겨 있다는 분석이다.

남은 과제

아스트라의 정식 출시 일정이나 공개 범위는 아직 밝혀지지 않았다. 형식 검증을 통과한 증명이라는 점에서 결과 자체의 신뢰도는 높지만, 이런 성과가 특정 유형의 문제에 국한된 것인지, 아니면 폭넓은 수학 연구 전반으로 확장 가능한지는 앞으로 더 지켜봐야 할 대목이다. 다만 형식 증명과 AI 추론을 결합해 검증 가능한 방식으로 난제를 공략하는 흐름 자체는, 향후 수학 연구 방법론에 적지 않은 영향을 줄 것으로 보인다.