오픈AI는 내부 모델 ‘아스트라(Astra)’가 수학과 이론컴퓨터과학의 공개 문제 10개에서 낸 연구 성과를 발표했다. 아스트라는 새로운 증명과 반례, 기존보다 강한 수학적 경계를 제시했으며, 결과는 249쪽 논문과 린(Lean) 형식 검증 코드로 공개됐다. 이번 성과는 정답이 정해진 시험을 푼 사례가 아니라, AI가 문제 탐색과 논증 작성부터 형식 검증까지 연구 과정에 참여한 사례다.
오픈AI는 결과를 249쪽 논문으로 묶었다. 각 논증은 린(Lean)이라는 정리 증명기로 다시 검사할 수 있도록 코드로도 공개했다. 눈여겨볼 대목은 ‘AI가 문제 10개를 풀었다’는 숫자 자체가 아니다. AI가 문제를 탐색하고 논증을 작성한 데 이어 형식 검증까지 연구 과정 전반에 참여했다는 점이다.
먼저 짚어볼 핵심
- 아스트라는 서로 다른 8개 분야의 공개 문제 10개에서 새로운 연구 결과를 냈다.
- 새로운 상한과 하한, 존재 증명, 오래된 추측을 뒤집는 반례가 결과에 포함됐다.
- 인간 연구자들은 같은 모델을 활용해 이 결과를 논문으로 정리했다.
- 모델은 각 논증을 린 코드로 형식화했고, 컴퓨터가 논리 단계를 검사할 수 있게 했다.
- 완성된 논문과 함께 풀이 아이디어의 전개 과정, 린 검증 코드도 공개됐다.
시험 문제를 푸는 AI와 무엇이 다른가
학교 시험은 대개 정답이 정해져 있다. 학생이 그 답에 이르는 과정을 평가한다. 연구 문제는 다르다. 정답부터 알려져 있지 않고, 어떤 접근법이 통할지도 모른다. 때로는 오랫동안 옳다고 여긴 예상이 틀렸음을 밝혀야 한다.
논문이 다룬 문제들은 적어도 10년 동안 핵심 결과에 별다른 진전이 없었고, 대부분은 그보다 훨씬 오래됐다. 아스트라는 기존 풀이를 재현하는 데 그치지 않고 새로운 논증이나 반례를 제시했다. 이번 성과를 ‘수학 문제 풀이 성능’이 아니라 ‘연구 과정에 참여하는 능력’의 사례로 봐야 하는 이유다.
10개 연구 성과를 쉽게 이해하기
1. 고차원 구면 패킹: 보이지 않는 차원에 공을 얼마나 촘촘히 넣을 수 있을까
같은 크기의 공을 상자에 넣으면 공 사이에 빈틈이 남는다. 아무리 촘촘하게 쌓아도 상자를 완전히 채울 수는 없다. 수학자들은 이 익숙한 문제를 우리가 사는 3차원에서 수십 차원, 수백 차원으로 넓혀 연구한다.
이번 연구는 고차원에서 공을 채울 수 있는 최대 밀도에 새로운 상한을 제시하고, 콘–엘키스(Cohn–Elkies) 방법이 도달할 수 있는 한계를 정확히 밝혔다. 1978년 이후 고차원 구면 패킹의 일반적인 지수 경계를 처음 개선한 결과다.
2. 이진 코드와 구면 코드: 잡음 속에서도 메시지를 구별하는 간격
휴대전화나 우주선이 데이터를 보내는 동안 일부 신호가 손상될 수 있다. 이때 원래 메시지를 알아보려면 서로 다른 신호 사이에 충분한 간격이 필요하다. 오류정정코드는 그 간격을 수학적으로 설계하는 기술이다.
논문은 정해진 최소 간격을 유지하면서 만들 수 있는 이진 코드와 구면 코드의 최대 크기에 대해, 기존보다 지수적으로 강한 상한을 제시했다. 특정 조건에서 ‘서로 안전하게 구별할 수 있는 신호의 수’가 어디까지 가능한지를 이전보다 엄격하게 제한한 셈이다.
3. 비소픽 군: 무한한 규칙을 작은 모형으로 항상 흉내 낼 수 있을까
‘군’은 대칭과 움직임의 규칙을 다루는 수학 구조다. 아무리 복잡한 무한 군이라도 유한한 순열 모형으로 갈수록 정확하게 흉내 낼 수 있는지, 수학자들은 오랫동안 답을 찾아왔다.
이번 연구는 그런 방식으로 근사할 수 없는 비소픽 군을 실제로 구성했다. 모든 군을 유한한 모형으로 근사할 수 있다는 가능성을 부정하는 존재 증명이다.
4. 코네스(Connes) 강직성 추측: 같은 지문을 가진 서로 다른 수학 구조
서로 다른 물체도 빛을 비추는 방향에 따라 같은 그림자를 만들 수 있다. 이와 비슷하게 서로 다른 군이 같은 폰 노이만(von Neumann) 대수라는 ‘그림자’를 가질 수 있는지가 이 문제의 핵심이다.
코네스는 특정 조건에서 그 그림자만으로 원래 군을 알아낼 수 있을 것이라고 예상했다. 그러나 논문은 서로 다른 군들이 같은 폰 노이만 대수를 갖는 사례를 구성해 이 추측에 반례를 제시했다.
5. 산술회로 복잡도: 계산을 아무리 영리하게 해도 필요한 최소 단계
산술회로는 덧셈과 곱셈 같은 연산을 이어 붙인 계산 설계도다. 겉으로는 간단해 보이는 계산도 입력이 커지면 엄청나게 많은 단계를 거쳐야 할 수 있다.
논문은 ‘퍼머넌트’라는 중요한 값을 계산하는 산술회로와 산술식에 새로운 복잡도 하한을 증명했다. 더 좋은 알고리즘을 아직 찾지 못했다는 의미가 아니다. 정해진 계산 방식에서는 일정한 양 이상의 작업이 반드시 필요하다는 결론이다.
6. 양자 병렬 반복: 어려운 게임을 반복하면 성공 확률은 얼마나 줄어들까
한 번의 게임은 운 좋게 이길 수 있다. 같은 종류의 게임을 여러 번 동시에 치르면 전체에 성공할 확률은 얼마나 빨리 낮아질까? 고전적인 게임에서는 잘 알려진 원리가 있지만, 양자 얽힘을 이용하는 참가자에게도 성립하는지를 밝히기는 훨씬 어렵다.
논문은 모든 유한한 2인 양자 게임에서 성공 확률이 반복 횟수에 따라 지수적으로 감소한다는 정리를 증명했다. 일부 특별한 게임에서만 알려졌던 원리를 일반적인 경우까지 넓혔다.
7. 최근접 벡터 문제: 격자에서 가장 가까운 점을 찾는 일은 얼마나 어려운가
모눈종이에서는 한 점과 가장 가까운 격자점을 쉽게 찾을 수 있다. 차원이 수백 개로 늘어나면 상황이 달라진다. 최근접 벡터 문제는 복잡한 고차원 격자에서 목표점에 가장 가까운 격자점을 찾는 문제다.
이번 결과는 정답을 정확히 찾는 일뿐 아니라 어느 정도 가까운 답을 구하는 일도 매우 어렵다는 새로운 다항식 수준의 근사 난이도를 제시했다. 최근접 벡터 문제는 격자 이론과 포스트양자 암호 연구의 중요한 기초 문제다.
8. 에르하르트(Ehrhart) 부피 추측: 격자점 하나만 품은 도형의 최대 크기
격자점이 찍힌 공간에 볼록한 도형을 하나 그려 보자. 도형 안에는 무게중심에 놓인 격자점 하나만 들어가야 한다. 이 조건을 지키면서 도형을 얼마나 크게 만들 수 있는지가 문제다.
논문은 모든 차원에서 가능한 최대 부피를 정확히 결정했다. 특정한 도형이 가장 크다는 예상에 정확한 경계를 제시했다.
9. 다색 램지 수: 같은 색 삼각형을 피하며 얼마나 큰 관계망을 만들 수 있을까
여러 사람을 선으로 모두 연결하고, 선마다 여러 색 가운데 하나를 칠한다고 해보자. 사람이 충분히 많아지면 세 사람이 같은 색 선으로 서로 연결된 삼각형이 반드시 생긴다.
이번 연구는 색의 수가 늘어날 때 같은 색 삼각형을 피할 수 있는 관계망이 기존에 알려진 것보다 훨씬 커질 수 있음을 증명했다. 에르되시 문제 183을 해결하고 다색 삼각형 램지 수의 성장 규모도 밝혔다.
10. 극단 그래프 이론: 오래된 예상이 틀렸음을 보여주는 두 반례
그래프 이론에서는 점과 선으로 이뤄진 관계망이 아주 커지면 특정 구조가 반드시 나타날 것이라고 예상하곤 한다. 그러나 모든 예상이 맞는 것은 아니다.
논문은 에르되시–시모노비츠의 콤팩트성 추측과 별도의 퇴화도 추측에 각각 반례를 구성했다. 이로써 에르되시 문제 146과 180이 해결됐다.
린 검증은 왜 중요한가
249쪽짜리 수학 논문을 검토하기는 쉽지 않다. 긴 증명에서는 작은 가정 하나가 빠지거나, 앞 단계에서 도출되지 않은 결론이 눈에 띄지 않게 끼어들 수 있다.
린은 증명을 잘게 나눈 뒤, 각 논리 단계가 정해진 규칙에 따라 앞 단계에서 올바르게 이어지는지 검사한다. 선생님이 답만 채점하지 않고 풀이의 모든 줄을 살펴보는 것과 비슷하다. 이번 연구는 10개 결과의 린 인증 코드를 논문과 함께 공개했다. 다른 연구자도 코드를 내려받아 직접 검사할 수 있다.
그렇다고 ‘컴퓨터가 수학적 의미와 중요성까지 모두 판단했다’는 뜻은 아니다. AI가 만든 긴 논증을 그대로 믿는 대신, 그 논리 구조를 독립적으로 재검사할 수 있게 됐다는 데 의미가 있다.
왜 이번 논문이 눈에 띄는가
무엇보다 한 분야에서 나온 우연한 성공으로 보기 어렵다. 10개 결과는 기하학, 부호 이론, 군론, 연산자 대수, 계산복잡도, 양자정보, 격자 이론, 조합론처럼 서로 다른 분야에 걸쳐 있다. 한 가지 풀이 유형을 반복한 경우보다 훨씬 넓은 연구 능력을 보여준다.
연구 결과와 검증 수단을 함께 공개한 점도 눈에 띈다. 사람이 읽을 수 있는 논문, 아이디어가 발전한 과정을 담은 해설, 컴퓨터가 검사할 수 있는 린 코드가 한꺼번에 제공된다. 결과만 발표한 것이 아니라 검증 과정까지 열어둔 셈이다.
AI가 맡은 역할도 달라졌다. 지금까지는 논문 검색과 요약, 번역, 코드 작성에 주로 쓰였다면, 이번에는 문제 탐색과 새로운 논증 작성, 논문 정리와 형식 증명까지 연구 과정에 참여했다.
연구의 역할 분담이 달라졌다
이번 성과를 ‘AI가 수학자를 대체했다’고만 설명하면 중요한 부분을 놓친다. 오픈AI에 따르면 수학적 논증은 모델이 생성했고, 인간은 같은 모델을 활용해 논문으로 정리했다. 모델은 이어서 논증을 린으로 형식화했다. 사람과 AI, 형식 검증 도구가 역할을 나눠 진행한 연구다.
수학자들은 이제 공개된 결과의 중요성을 평가하고, 아이디어를 다른 문제로 확장하며, 더 간결하고 이해하기 쉬운 설명을 만들어 갈 것이다. 아스트라의 성과는 완결된 결론이라기보다 AI를 활용한 수학 연구가 어떤 모습으로 자리 잡을지 보여주는 출발점에 가깝다.
AI는 지식을 설명하는 데서 한 걸음 더 나아가 새로운 지식의 후보를 만들고, 이를 검증 가능한 형태로 제시하기 시작했다. 249쪽 논문과 린 코드의 동시 공개는 그 변화를 구체적으로 보여준다.
자주 묻는 질문
Q1. 아스트라는 몇 개 문제에서 연구 성과를 냈나?
A. 아스트라는 서로 다른 8개 분야의 공개 문제 10개에서 새로운 연구 결과를 냈다. 결과에는 새로운 상한과 하한, 존재 증명, 오래된 추측을 뒤집는 반례가 포함됐다.
Q2. 이번 연구 결과는 어떻게 공개됐나?
A. 오픈AI는 결과를 249쪽 논문으로 묶어 공개했다. 풀이 아이디어의 전개 과정과 각 논증을 형식화한 린 검증 코드도 함께 제공했다.
Q3. 린 검증 코드는 무엇을 확인하나?
A. 린은 증명을 논리 단계로 나눠 각 단계가 정해진 규칙에 따라 앞 단계에서 올바르게 이어지는지 검사한다. 다만 수학적 의미와 중요성까지 컴퓨터가 모두 판단한다는 뜻은 아니다.
직접 확인하기
- 249쪽 논문 원문: Ten Advances in Mathematics and Theoretical Computer Science
- 오픈AI 공식 발표
- 풀이 아이디어 해설: How the Ideas Came Together
- 10개 결과의 린 검증 코드