오픈AI, 미해결 수학·이론컴퓨터과학 문제 10개를 AI로 풀었다고 공개

• 오픈AI가 내부 차세대 모델 ‘아스트라’로 수학·이론컴퓨터과학의 장기 미해결 문제 10개에서 새 결과를 만들었다고 공개함

  • 대상은 고차원 기하, 코드 이론, 군론, 연산자 대수, 양자 복잡도, 격자 암호, 극값 조합론까지 꽤 넓음
  • 오픈AI 기준으로는 최소 10년 이상 핵심 결과에 진전이 없던 문제들이고, 상당수는 그보다 훨씬 오래 묵은 문제라고 함

• 이번 발표의 포인트는 ‘벤치마크 점수’가 아니라 실제 연구 문제를 모델 개발 중 평가에 넣었다는 점임

  • 오픈AI는 앞서 에르되시 단위거리 추측(Erdos unit-distance conjecture)의 AI 생성 반례를 공개했고, 그 뒤로 관련 후속 연구가 이미 나왔다고 설명함
  • 이번에는 그 연장선에서 10개 결과를 묶어 공개한 셈이라, “AI가 연구 보조를 넘어 결과 생성까지 갈 수 있나?”라는 질문을 정면으로 던짐

• 공개된 결과 목록이 꽤 세다. 그냥 예제 풀이가 아니라 각 분야 커뮤니티가 신경 쓸 만한 항목들임

  • 고차원 구 채우기(sphere packing)에서는 Cohn-Elkies 임계값까지 내려가는 새 상한을 제시했다고 함
  • 이진 코드와 구면 코드에서는 최소 거리 조건에서 가능한 코드 크기에 대해 지수적으로 개선된 경계를 냈다고 함
  • 비소픽 군(non-sofic groups)의 존재를 보이는 구성도 포함됐는데, 군론의 중심 질문 하나를 건드린 결과임
  • Connes의 강성 추측(rigidity conjecture)에 대해서는 특정 군이 폰 노이만 대수(von Neumann algebra)로 유일하게 결정된다는 오래된 추측을 반박했다고 함

• 이론컴퓨터과학 쪽 결과도 만만치 않음

  • 영구식(permanent)을 계산하는 산술 회로와 산술 공식에 대해 새 하한을 제시했고, 산술 공식 하한은 n^4/log n 규모라고 밝힘
  • 일반적인 두 플레이어 양자 게임에 대해 지수적 병렬 반복 정리(exponential parallel repetition theorem)를 냈다고 함
  • 최근접 벡터 문제(Closest Vector Problem)에 대해서는 다항식 배수 근사 난이도를 보였다고 설명하는데, 이건 격자 기반 포스트 양자 암호와 연결되는 주제임

• 조합론 쪽에서도 에르되시 문제가 여러 개 등장함

  • 다색 삼각형 램지 수(multicolor triangle Ramsey numbers)에 대해 초지수(superexponential) 하한을 제시해 에르되시 문제 183을 해결했다고 함
  • 극값 그래프 이론의 compactness 추측과 degeneracy 추측 관련 결과로 에르되시 문제 146, 180도 다뤘다고 밝힘

• 검증 방식도 신경 쓴 흔적이 있음. 오픈AI는 결과를 ‘AI가 만들고 사람이 정리한 뒤, Lean으로 형식화했다’고 설명함

  • 수학 논문은 그럴듯한 문장만으로는 부족하니까, 기계 검증 가능한 Lean 인증서를 붙인 게 핵심임
  • 동시에 모델이 자신의 사고 과정을 설명한 내레이션도 각 풀이와 함께 공개한다고 함

• 저자성과 책임 문제도 피하지 않았음

  • 오픈AI는 AI가 전적으로 생성한 증명을 인간 저작물처럼 표시하는 건 시스템의 기여와 인간 지적 노동의 성격을 둘 다 왜곡한다고 말함
  • 원고 정리와 Lean 형식화에는 사람이 개입했지만, 수학적 논증 자체는 시스템이 생성했다고 선을 그음
  • 결과의 정확성에 대해서는 오픈AI가 책임을 지겠다고 밝히면서도, 수학 커뮤니티가 직접 맥락화하고 검토해달라는 입장을 냄

• 배경에는 ‘ChatGPT for Academic Researchers’도 있음

  • 오픈AI는 과학자와 수학자 10만 명에게 자사 최고 모델을 무료 제공하는 이니셔티브를 최근 발표했다고 언급함
  • AI 연구 도구가 강해질수록 일부 기관만 접근하는 구조가 되면 학문 생태계가 흔들릴 수 있으니, 접근권 문제를 같이 제기한 셈임

---

기술 맥락

• 이번 발표에서 핵심 선택은 “AI가 만든 증명을 Lean으로 형식화한다”는 부분이에요. 수학 문제는 답이 그럴듯해 보여도 중간 논리가 틀리면 끝이라서, 자연어 논문만 공개하면 커뮤니티가 받아들이기 어려웠을 거예요.

• 왜 Lean이 중요하냐면, 검증 책임을 사람의 직관에만 맡기지 않고 기계가 확인 가능한 형태로 바꾸기 때문이에요. 특히 AI 모델은 환각(hallucination) 리스크가 있으니, 형식 증명 시스템을 붙이는 게 결과 신뢰도의 최소 방어선이 돼요.

• 또 하나의 포인트는 비용이에요. 오픈AI는 전체 풀이 탐색 비용을 약 2천 달러라고 밝혔는데, 이 숫자는 연구 자동화가 실제로 경제성을 가질 수 있는지 따질 때 꽤 중요한 기준점이에요.

• 다만 이게 곧바로 “수학자가 필요 없어졌다”는 뜻은 아니에요. 원고 정리, 결과의 의미 해석, 기존 연구와의 연결, 후속 연구 방향은 여전히 커뮤니티가 해야 하는 일이거든요.