OpenAI 내부 모델이 장기 미해결 수학 문제 10건에 새 결과를 냈어요

OpenAI 내부 모델이 장기 미해결 수학 문제 10건에 새 결과를 냈어요

AI 뉴스 썸네일

OpenAI가 차기 주요 모델의 내부 버전인 Astra로 수학과 이론 컴퓨터 과학의 공개 문제 10건에서 새로운 결과를 얻었다고 밝혔어요. 각 문제는 핵심 진전이 최소 10년 동안 없었던 과제예요. 모델은 해법을 찾았고, 사람은 논문 작성과 정확성 검토를 맡았어요. 모델이 다시 각 논증을 Lean 인증서로 형식화했다는 점도 눈에 띄어요. 1

핵심 요약

구분	핵심	왜 볼 만한가요
연구 범위	고차원 기하학, 군론, 회로 복잡도, 양자 게임, 격자 암호 등 10개 문제를 다뤘어요	한 분야의 벤치마크 풀이를 넘어 여러 전공의 공개 문제에 결과를 냈어요
작업 분담	Astra가 수학적 논증을 만들고, 사람이 논문 준비와 검토를 맡았어요	AI의 기여와 인간의 책임을 어떻게 나눌지 구체적인 사례를 남겼어요
형식 검증	모델이 각 논증을 Lean 인증서로 옮겼어요	자연어 증명의 오류를 줄일 수 있는 기계 검증 경로를 함께 제시했어요
비용	해법 탐색에 Sol API 가격 기준 약 2,000달러 상당의 토큰을 썼어요	결과 10건의 탐색 비용은 공개됐지만 전체 연구비와 시도 횟수는 따로 봐야 해요

1. 한 분야가 아닌 10개 장기 과제를 함께 다뤘어요

공개된 결과는 구 포장과 이진·구면 코드의 경계 개선부터 시작해요. 군론에서는 비-sofic 군의 존재를 보이는 구성을 제시했고, 특정 군이 von Neumann 대수에 의해 유일하게 결정된다는 Connes 강성 추측에는 반례를 냈다고 설명해요. 이론 컴퓨터 과학에서는 영구행렬 계산을 위한 산술 공식 하한을 `n⁴/log n` 차수로 높였어요. 일반적인 2인 양자 게임에는 지수적 병렬 반복 정리를 제시했어요. 2

암호와 조합론에 닿는 결과도 있어요. 포스트 양자 암호와 연결된 최근접 벡터 문제에서 다항식 배수 근사의 난해성을 다뤘어요. 무게중심만 내부 격자점으로 갖는 볼록체의 최대 부피를 모든 차원에서 정하는 Ehrhart 부피 추측에도 답했다고 밝혔어요. 다색 삼각형 Ramsey 수와 극값 그래프 이론에서는 Erdős 문제 146번, 180번, 183번을 해결했다고 정리했어요.

728x90

이 목록을 한 줄짜리 "AI가 난제를 풀었다"로 받아들이면 세부 차이가 사라져요. 어떤 결과는 오랜 추측의 반증이고, 어떤 결과는 기존 경계를 개선한 정리예요. 비-sofic 군처럼 존재 자체가 공개 문제였던 항목도 있어요. 결과마다 학술적 무게와 후속 검증 범위가 다르므로, 분야별 연구자가 논증을 확인하고 학계의 평가를 거쳐야 해요.

자연어 증명 뒤에 Lean 인증서를 붙였어요

OpenAI는 모델의 자연어 답변만 공개하지 않았어요. 사람이 같은 모델을 활용해 논문을 준비한 뒤, 모델이 각 논증을 Lean으로 형식화했다고 설명해요. Lean은 정의와 추론 규칙을 기계적으로 확인하는 정리 증명 도구예요. 형식화된 인증서는 추론 단계가 규칙에 맞는지 검사하는 데 도움을 줘요. 관련 코드는 공개 저장소에서 확인할 수 있어요. 3

다만 Lean 인증서가 연구의 모든 판단을 대신하지는 않아요. 형식화에 사용한 정의가 원래 문제와 정확히 일치하는지, 새 결과가 기존 문헌과 어떤 관계인지, 증명이 실제로 새로운 아이디어를 담았는지는 사람이 따로 살펴야 해요. 기계 검증은 논리적 빈틈을 줄이는 장치이고, 학술적 가치 평가는 연구 공동체의 검토가 필요해요.

2,000달러는 전체 연구비가 아니에요

OpenAI가 제시한 약 2,000달러는 Sol API 요금으로 환산한 해법 탐색 토큰 비용이에요. 모델 훈련비, 문제 선정, 연구자의 검토 시간, 논문 작성, 형식화 점검까지 모두 더한 총비용으로 읽으면 안 돼요. 몇 개의 문제를 시도했고 실패한 문제에 얼마나 많은 연산을 썼는지도 이 숫자만으로는 알 수 없어요.

비용 수치는 재현성을 판단할 때 필요한 정보 중 하나예요. 문제별 시도 횟수와 중단 기준, 모델에 제공한 문헌과 힌트, 사람의 개입 시점이 함께 공개돼야 다른 연구팀이 같은 조건을 비교할 수 있어요. 이번 발표는 결과와 논문, Lean 저장소를 공개했지만, 탐색 과정 전체를 평가하려면 더 자세한 실행 기록이 필요해요.

AI의 이름과 사람의 책임을 따로 적었어요

OpenAI는 수학적 논증을 Astra가 생성했다고 명시했어요. 사람은 논문 준비와 형식화 지원, 최종 정확성에 책임을 진다고 설명해요. AI가 만든 증명을 사람의 단독 저작으로 표시하면 실제 기여가 흐려지기 때문에 생성 주체를 분명히 밝혀야 한다는 입장이에요.

이 방식은 학술 저자 기준에 새 질문을 던져요. 모델은 책임을 질 수 없으므로 논문의 저자가 되기 어렵지만, 결과 생성에 큰 몫을 했다면 도구 한 줄로만 처리하기도 어려워요. 연구자는 문제 선정, 검증, 문헌 비교, 오류 수정에 쓴 작업을 기록해야 해요. 학회와 저널도 AI가 만든 핵심 논증을 어떤 항목에 공개할지 기준을 더 구체적으로 정할 필요가 있어요.

왜 중요한가요

이번 발표에서 개발자와 연구자가 볼 지점은 정답 개수보다 작업 방식이에요. 모델이 후보 논증을 탐색하고, 사람이 결과를 논문으로 다듬고 검토한 다음, 정리 증명 도구가 논리 구조를 검사했어요. 자연어 생성과 인간 검토, 형식 검증을 연결한 흐름은 수학뿐 아니라 보안 프로토콜, 컴파일러, 알고리즘 검증에도 적용할 수 있어요. 3

성과의 범위는 신중하게 읽어야 해요. 기업의 발표만으로 10건 모두가 학계에서 최종 확정됐다고 볼 수는 없어요. 분야별 연구자가 논문과 Lean 코드를 검토하고, 기존 문헌과 비교하고, 독립적으로 재현하는 과정이 남아 있어요. 그 검토를 통과한다면 AI가 이미 알려진 정리를 설명하는 수준에서 벗어나 새로운 연구 후보를 만들고 검증 가능한 형태로 내놓았다는 사례가 돼요.

연구팀은 비슷한 시스템을 도입할 때 성공 사례만 세기보다 실패 기록도 함께 남겨야 해요. 시도한 문제 수, 문제별 계산량, 사람이 준 힌트, 수정 횟수, 형식 검증 통과 여부를 기록하면 모델의 실제 기여를 더 정확히 비교할 수 있어요. 비용과 정확성, 재현성을 한꺼번에 공개해야 다른 연구자도 결과를 믿고 이어서 연구할 수 있어요.

참고 자료

1. 수학과 이론 컴퓨터 과학의 10가지 진전 — GeekNews
2. Ten advances in mathematics — OpenAI
3. openai/ten-proofs — GitHub
4. Ten Proofs — OpenAI 논문