OpenAI, 차세대 모델 ‘Astra’ 수학·이론컴퓨터과학 난제 10건 해법 공개

OpenAI 공식 발표에 따르면 회사는 차세대 모델 ‘Astra’의 내부 버전으로 수학과 이론컴퓨터과학의 장기 미해결 문제 10건에 대한 새로운 결과를 도출했다. OpenAI는 이들 문제가 적어도 10년 동안 핵심 결과에서 진전이 없었고, 대부분은 더 오랫동안 풀리지 않았다고 설명했다.

발표된 결과는 고차원 구 채우기와 이진·구면 부호, 군론, 연산자 대수, 산술 회로 복잡도, 양자 복잡도, 격자 암호, 극대 조합론 등 여러 분야에 걸쳐 있다. OpenAI는 비소픽 군의 존재를 보이는 구성과 콘스 강성 추측의 반례, 다색 삼각형 램지 수의 초지수적 하한 등을 포함했다고 밝혔다.

연구 과정에서 수학적 논증은 Astra가 생성했다. 이후 사람이 같은 모델을 활용해 논문 형태로 정리했고, 모델이 각 논증을 Lean 형식 증명서로 옮겼다는 것이 회사의 설명이다. OpenAI는 사람이 작성한 결과로 표기하면 실제 생성 과정을 왜곡할 수 있다며, 논증은 모델이 만들었고 회사가 준비와 형식화 및 정확성에 책임을 진다고 밝혔다.

OpenAI가 공개한 GitHub 저장소에는 10개 결과의 Lean 4 형식화 파일이 올라와 있다. 저장소는 Lean 4.32.0과 mathlib, Lake를 사용하며 전체 증명을 한 번에 빌드하거나 문제별 모듈을 따로 확인할 수 있도록 구성됐다. 논문과 모델의 추론 과정을 설명한 별도 자료도 함께 공개됐다.

주요 결과 중 하나는 모든 군이 유한 순열로 근사될 수 있는지를 묻는 군론 문제와 관련된다. OpenAI는 비소픽 군을 구성해 해당 질문에 답했다고 주장한다. 또 특정 군이 폰 노이만 대수에 의해 유일하게 결정된다는 콘스 강성 추측에 대해서도 반례를 제시했다고 밝혔다.

형식 증명서 공개는 주장된 논증을 기계적으로 점검할 수 있는 경로를 제공한다. 다만 Lean 코드가 공개됐다는 사실만으로 각 결과의 수학적 의미와 기존 연구와의 관계에 대한 평가가 끝나는 것은 아니다. 장기 미해결 문제 해결이라는 중대한 주장은 각 분야 연구자의 독립적인 검토와 후속 논의를 거쳐야 한다.

이번 발표는 생성형 AI가 기존 연구를 요약하거나 계산을 보조하는 수준을 넘어 새로운 수학적 논증을 제안하고 형식 검증 자료까지 만드는 방향으로 이동하고 있음을 보여준다. 동시에 AI가 만든 연구 성과의 저자 표시와 책임, 검증 절차를 수학계가 어떻게 정립할지에 대한 논의도 커질 전망이다.

출처: OpenAI 공식 발표 https://openai.com/index/ten-advances-in-mathematics/
출처: OpenAI 공식 GitHub 저장소 https://github.com/openai/ten-proofs
출처: OpenAI 공개 논문 https://cdn.openai.com/pdf/ten-proofs-oai.pdf
출처: OpenAI 추론 과정 해설 https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf