본문으로 건너뛰기
IFAI

연구

OpenAI 차세대 모델 'Astra', 10개 수학 난제 해결…증명은 Lean 검증 마쳐

게시 확산 지수 39

OpenAI는 차세대 주력 모델 'Astra'의 내부 버전을 통해 10개의 수학 및 이론 컴퓨터 과학 미해결 난제를 해결하거나 대폭 진전시켰다고 발표했다. 콘 강성 추측 반증과 에르되시 문제 3건 해결 등이 포함되며, 추론 비용은 Sol API 기준 약 2,000달러에 불과했다. 모든 증명은 Lean으로 공식 검증되었다.

OpenAI 차세대 모델 'Astra', 10개 수학 난제 해결…증명은 Lean 검증 마쳐
이미지: openai.com

AI가 아무리 똑똑해도 이미 인류가 써둔 지식을 요약하는 데 그칠 뿐, 백년 가까이 풀리지 않은 순수 수학 난제를 스스로 푸는 건 먼 미래의 일이라고 여겨졌습니다. 하지만 이 상식이 깨졌을지도 모릅니다.

OpenAI는 차세대 주력 모델 제품군의 내부 버전인 'Astra'를 사용해 수학 및 이론 컴퓨터 과학 분야의 10대 미해결 난제를 해결하거나 대폭 진전시켰다고 발표했습니다. 10개 문제 모두 최소 10년 이상, 길게는 30년 가까이 학계에서 풀리지 않던 문제들이었습니다.

더 놀라운 건 비용입니다. Sol API 요율 기준으로 환산했을 때, Astra가 이 10개 문제의 해법을 찾아내는 데 쓴 전체 토큰 비용은 고작 2,000달러 안팎에 불과했습니다.

콘 강성 추측 반증부터 에르되시 문제까지

이번에 Astra가 풀어낸 문제들은 고차원 기하학, 부호 이론, 연산 회로 복잡도, 군론, 작용소 대수, 양자 복잡도, 격자 암호학, 극값 조합론에 걸쳐 있습니다.

예컨대 군론 분야에서는 1999년 이후 수학자들이 찾아 헤매던 '비(非) 소픽 군(non-sofic group)'의 존재를 입증하는 구조를 실제로 구성해 냈습니다. 또한 작용소 대수학의 유명 난제인 알랭 콘(Alain Connes)의 강성 추측을 반증했고, 에어하트(Ehrhart) 부피 추측을 전 차원에서 규명했습니다. 여기에 헝가리 수학자 파울 에르되시가 남긴 문제 중 146번, 180번, 183번 3건도 한꺼번에 해결했습니다.

포스트 양자 암호의 핵심인 최근접 벡터 문제(CVP)의 다항식 인자 근사 난해성을 입증하고, 고차원 구 채우기 상한선을 새롭게 갱신하는 등 각 분야의 굵직한 난제들이 포함되었습니다.

OpenAI에 따르면 수학적 논증은 Astra가 독자적으로 도출했으며, 연구팀은 해당 모델과 협력해 논문 초안을 작성했습니다. 이어 Astra가 모든 증명을 컴퓨터 증명 검증 시스템인 'Lean' 인증서로 형식화해 완벽하게 검증을 마쳤습니다. 공식 발표와 함께 모델의 사고 과정(CoT) 기록도 함께 공개되었습니다.

업계 반응도 즉각적이었습니다. 발표 24시간 만에 Anthropic의 Levent Alpoge는 자사 모델 Fable을 활용해 일반적인 프롬프트와 오프라인 환경에서 10개 문제 중 5개의 증명을 그대로 재현해 냈다고 밝혔습니다.

저자권 논쟁과 라이덴 선언

핵심 증명을 AI가 해냈다면 논문 저자는 누가 되어야 할까요? OpenAI는 'AI와 수학에 관한 라이덴 선언' 등 학계의 우려를 존중한다며 저자권 문제를 분명히 짚었습니다.

시스템이 도출한 증명에 인간 저자명을 올리는 것은 AI의 기여와 인간의 지적 노동 모두를 왜곡하는 일이라는 입장입니다. OpenAI 연구진은 Lean을 통한 형식화와 논문 작성, 정합성 검증에 책임을 지되, 수학적 아이디어와 논증 자체는 Astra의 공으로 돌렸습니다. 학계에서는 기계가 사고를 전담한 이 성과를 두고 '필즈상 감이냐'는 논쟁까지 번지고 있습니다.

왜 중요한가

저희가 보기에 이번 발표에서 가장 충격적인 숫자는 난제의 이름이 아니라 '2,000달러'입니다.

그동안 프론티어 AI를 통한 과학 연구는 천문학적인 컴퓨팅 자원을 쏟아부을 수 있는 빅테크의 전유물처럼 보였습니다. 하지만 지난 수십 년간 막혀 있던 10개의 수학 난제를 뚫어내는 비용이 고작 2,000달러라면 이야기가 완전히 달라집니다. 일선 연구실이나 개별 수학자도 본인이 세운 가설 검증을 AI 추론 파이프라인에 맡길 수 있는 시대가 열린 셈입니다.

경쟁 측면에서도 Anthropic이 하루 만에 절반을 재현해 낸 점을 보면, 최상위 모델 간의 심층 논리 추론 격차는 생각보다 크지 않습니다. 이제 승부처는 단순 텍스트 생성이 아니라, 고도화된 추론 모델과 Lean 같은 형식 검증기를 결합해 '환각이 없는 검증된 지식'을 뽑아내는 실전 워크플로 구축으로 넘어갔습니다.

엄밀함의 끝판왕인 순수 수학에서 이 고리가 입증된 만큼, 향후 신약 물질 발굴이나 신소재 설계 등 인접 과학 분야로 이 방식이 번져나갈 때 연구 속도는 이전과 비교할 수 없을 만큼 빨라질 것으로 보입니다.

출처 (2)

  1. [1]
    openai.com(새 탭에서 열림)원문openai.com
  2. [2]
    youtube.com(새 탭에서 열림)보도youtube.com

매일 AI 콘텐츠 픽