OpenAI 차세대 모델 '아스트라', 수학·이론 컴퓨터 과학 10대 미해결 난제 해결 및 Lean 공식 증명 공개

OpenAI가 차세대 플래그십 AI 모델인 '아스트라(Astra)'의 내부 연구 버전을 활용해 수학 및 이론 컴퓨터 과학(TCS) 분야에서 수십 년간 진전이 없었던 10대 미해결 난제를 해결했다고 공식 발표했습니다. 이번 성과는 지난 5월 에르뢰시 단위 거리 추측 반증에 이은 후속 연구로, 프론티어 AI가 단순한 코드 생성을 넘어 심층적인 고차원 수학적 추론과 이론적 체계 구축을 자율적으로 수행할 수 있음을 입증한 중대한 이정표로 평가받습니다.

발표된 10대 난제는 고차원 기하학, 부호 이론, 산술 회로 복잡도, 군론, 작용소 대수, 양자 복잡도, 격자 암호학, 극단 조합론 등 현대 수학과 컴퓨터 과학의 핵심 분야를 포괄합니다. 주요 성과로는 콘-엘키스(Cohn-Elkies) 임계치까지 고차원 구 채우기 밀도 상한을 새롭게 규명한 연구, 군론의 오랜 미해결 과제였던 '비소픽 군(Non-sofic groups)'의 존재성 증명, 폰 노이만 대수 관련 '콘의 강성 추측(Connes’s rigidity conjecture)' 반증, 그리고 포스트 양자 암호의 이론적 기반이 되는 '최근접 벡터 문제(Closest Vector Problem)'의 다항식 인자 근사 난이도 규명 등이 포함되었습니다. 또한 에르뢰시 183번(다색 램지 수), 146번 및 180번(극단 수 추측) 문제도 성공적으로 해결되었습니다.

기술적 관점에서 주목할 점은 연산 효율성과 엄밀한 검증 프로세스입니다. OpenAI에 따르면 이들 문제를 해결하는 데 소요된 총 추론 토큰 비용은 자사의 Sol API 단가 기준으로 문제당 약 2,000달러 수준에 불과했습니다. 모델이 도출한 수학적 논증은 연구진과의 협업을 통해 논문 형태로 정리되었을 뿐만 아니라, 린(Lean) 대화형 정리 증명기를 활용해 기계 검증이 가능한 정형 증명서(Lean certificate) 형태로 완전하게 변환되었습니다. OpenAI는 연구의 재현성과 투명성을 높이기 위해 각 해법에 대한 모델의 사고 과정(Reasoning Walkthrough) 전문과 Lean 소스코드를 GitHub 저장소에 전면 공개했습니다.

OpenAI는 AI의 학술 연구 기여에 따른 윤리적 책임과 학계와의 협력 원칙도 강조했습니다. 라이덴 AI-수학 선언(Leiden Declaration)의 취지를 존중하여 AI 시스템이 생성한 증명에 대해 인간의 단독 저작권을 주장하지 않고 기여도를 정직하게 명시하기로 했습니다. 아울러 10만 명의 수학자 및 과학자에게 최신 모델 접근 권한을 무상 제공하는 'ChatGPT for Academic Researchers' 이니셔티브를 통해 과학 연구 생태계 지원을 지속적으로 확대할 방침입니다.

연구 논문 전문 및 모델의 추론 과정 기록, Lean 형식 증명 코드는 OpenAI 공식 웹사이트와 GitHub 저장소(openai/ten-proofs)에서 확인할 수 있습니다.