“불가능할 줄 알았는데”… 대학 최고 난이도 수학 시험, AI가 12문제 완벽 증명

미국 AI 스타트업 액시엄(Axiom)이 발표한 리포트에 따르면, AI 수학 증명 시스템이 세계에서 가장 어려운 대학생 수학 대회로 꼽히는 퍼트넘(Putnam) 시험 2025년도 문제 12개를 전부 풀었다. 액시엄이 개발한 ‘액시엄프루버(AxiomProver)’는 시험에서 시험 시간 내 8문제를 해결했고, 나머지 4문제도 추가 시간을 들여 완벽하게 증명했다.

퍼트넘 시험은 매년 12월 미국과 캐나다 대학생들이 참가하는 수학 경시대회로, 참가자 절반 이상이 0점에 가까운 점수를 받을 정도로 난이도가 높다. 액시엄프루버가 이 문제들을 푼 방식은 특별했다. ‘린(Lean)’이라는 프로그래밍 언어를 사용해 모든 풀이 과정을 컴퓨터가 검증할 수 있게 만든 것이다. 단순히 답만 맞춘 게 아니라 모든 계산 단계의 정확성을 기계적으로 입증했다는 의미다.

액시엄은 전체 증명 과정을 공개하며 “AI와 인간이 수학 문제를 완전히 다르게 접근한다”는 흥미로운 분석을 내놨다.


사람에게는 쉬운 문제, 컴퓨터 언어로는 엄청 복잡하다

사람 눈에는 쉬워 보이는 문제도 컴퓨터가 이해할 수 있게 번역하면 상상 이상으로 복잡해진다. A2 문제는 특정 범위에서 어떤 함수 값이 항상 음수임을 보이는 미적분 문제였다. 그래프를 보면 한눈에 알 수 있는 내용이다. 그런데 이걸 린 언어로 작성하자 60줄이 넘는 코드가 필요했다. B2 문제도 마찬가지로 단순한 증명에 60줄 이상이 들어갔다. 

더 극단적인 예가 A5 문제다. 숫자를 배열하는 방법의 개수를 세는 문제로, 인간 수학자는 핵심 아이디어를 몇 문단으로 설명할 수 있다. “가장 큰 숫자를 기준으로 나눠서 생각한다”는 자연스러운 접근법이다. 그런데 이걸 린으로 옮기자 무려 2,054줄의 코드가 필요했고, 만드는 데 8시간 반이 걸렸다. 액시엄은 “사람에게는 당연해 보이는 증명을 컴퓨터가 이해할 수 있게 바꾸려면 이 정도는 감수해야 한다”고 설명했다. 컴퓨터는 아무리 사소한 경우라도 모두 하나하나 설명해줘야 하기 때문이다.


AI가 불가능하다던 조합 문제와 도형 문제를 풀었다 

조합론 문제는 역사적으로 AI의 약점으로 꼽혀왔다. 2024년 국제수학올림피아드(IMO)에서 풀리지 않은 2개 문제, 2025년 IMO의 미해결 문제 모두 조합론 분야였다. 많은 AI 개발팀은 아예 이 영역을 포기했을 정도다. 기하학 역시 제대로 다루려면 별도의 기하 엔진이 필요한데, 액시엄프루버는 아직 이를 갖추지 못했다.

그래서 액시엄 팀도 A3(조합론)과 B1(기하학) 문제는 AI가 풀 수 없을 것으로 예상했다. 그런데 액시엄프루버가 두 문제를 모두 자율적으로 해결했다. 이는 조합론과 기하학이 갑자기 쉬워졌다는 의미가 아니라, 이 분야에 대한 기존의 비관론이 항상 맞는 것은 아니라는 점을 보여준다.

A3은 앨리스와 밥이 숫자 문자열로 게임하는 문제였다. 다행히 모든 경우의 수를 일일이 따질 필요 없이 밥이 이기는 간단한 방법이 존재했다. 밥은 앨리스의 수에 신경 쓰지 않고 정해진 전략만 기계적으로 실행하면 됐다. 덕분에 컴퓨터가 추적할 상태도 적고 복잡한 분기 추론도 필요 없어서 린에서 처리하기 쉬웠다.

더 흥미로운건 B1 문제다. 평면을 빨강과 초록으로 칠하는 문제였는데, 액시엄프루버는 순전히 도형 방식으로 이를 해결했다. 아이러니하게도 AI는 그림을 전혀 그리지 않았다. 수학자들은 AI가 작성한 코드를 이해하기 위해 직접 손으로 그림을 그려야 했지만, AI는 “같은 반지름의 원 두 개가 정확히 두 점에서 만난다”는 사실을 순전히 숫자와 기호만으로 추론했다.


인간 수학자들은 실패했지만, AI는 5시간 만에 해결 

A6 문제는 액시엄 수학자들 대부분을 좌절시켰다. 복잡한 수학 이론이 필요한 문제로, 한 수학자는 올바른 방향을 알고 있었지만 끝까지 풀지는 못했다. 아이디어를 아는 것과 실제로 완성하는 것은 완전히 다른 문제였다.

액시엄프루버는 이 문제를 5시간 동안, 12개 문제 중 두 번째로 많은 계산량을 써서 해결했다. 특히 복잡한 수식의 미분을 처리하는 방식이 독특했다. 인간이라면 절대 시도하지 않을 비효율적인 접근이었지만 정확한 답을 도출했다. 액시엄 측은 “직접 계산으로 밀고 나가는 방식도 나름의 효율성을 갖는다”고 설명했다.

사람은 숫자로, AI는 도형으로… 완전히 다른 사고방식 

A4 문제에서는 인간과 AI의 접근 방식이 극명하게 갈렸다. 행렬의 최솟값을 구하는 문제였다. 대부분의 수학자들은 본능적으로 방정식을 풀려고 했다. 한 수학자는 답이 숫자가 커질수록 증가할 거라 예상했다. 다른 수학자는 작은 숫자부터 시작해서 답이 3일 거라고 추측했다.

반면 액시엄프루버는 완전히 다른 각도로 접근했다. 복잡한 수식을 3차원 공간의 화살표들로 바꿔서 생각한 것이다. 마치 수학 문제를 레고 블록처럼 시각화한 셈이다. 이렇게 관점을 바꾸자 문제가 훨씬 간단해졌다. “3차원 공간에서 이웃한 화살표끼리만 직각을 이루는 배치가 가능할까?”라는 문제로 바뀐 것이다. 흥미로운 점은 그 이후 과정이다. AI는 대부분의 시간을 이 화살표 배치가 실제로 작동하는지 하나하나 확인하는 데 사용했다. 인간 수학자라면 충분히 명백하다고 판단해 그냥 넘어갈 부분이였만, AI는 모든 논리적 단계를 빠짐없이 검증하는 방식으로 작동했다.

B4 문제는 이런 차이를 더욱 선명하게 보여준다. 한 수학자는 답을 그림 한 장으로 설명했다. 그림을 보는 순간 “아, 이래서 답이 맞구나”하고 이해가 된다. 하지만 컴퓨터는 그림을 ‘이해’하지 못한다. 따라서 그림 대신, 액시엄프루버는 1,061줄의 코드를 작성해 가능한 모든 경우를 하나하나 따졌다. 간결한 풀이는 아니지만, 틀릴 가능성이 전혀 없는 확실한 방법이었다.

AI와 인간, 서로 다른 강점을 합치면 

액시엄은 이번 성과가 중요한 질문을 던진다고 말한다. “AI에게 어려운 수학 문제란 무엇인가?” 사람에게 어려운 것과 AI에게 어려운 것은 다르다. 사람은 경우의 수가 많은 문제가 지루하고, 한 가지 기발한 아이디어가 필요한 문제에서 막힌다는 걸 안다. 하지만 AI는 어떤 문제를 어려워하는지 아직 명확하지 않다. 어떤 특징이 자동 증명 프로그램을 힘들게 하는지에 대한 연구가 필요하다. 

바로 이 차이 때문에 협업이 의미 있다. 지금은 사람이 문제를 주면 AI가 증명을 찾는 단순한 방식이다. 하지만 더 발전된 형태를 상상할 수 있다. AI가 실시간으로 사람의 아이디어를 검증하고, 사람이 AI의 결과를 보고 방향을 조정하는 것이다. 서로의 장점을 살리는 것이다.

액시엄이 그리는 미래는 사람의 직관이 AI 검증으로 뒷받침되고, AI 검증이 다시 사람의 직관에 영감을 주는 세상이다. 수학 경시대회를 넘어 실제 수학 연구에서도 이런 협업을 시도하고 싶다고 밝혔다. 경시대회 문제는 정해진 답이 있지만, 연구는 다르다. 새로운 개념을 만들고, 이론을 세우고, 문제를 바라보는 관점을 선택해야 한다. 어떤 증명이 맞는지가 아니라 어떤 접근이 문제를 녹이는지를 찾는 게 핵심이다. 

FAQ (※ 이 FAQ는 본지가 리포트를 참고해 자체 작성한 내용입니다.) 

Q1. 퍼트남 시험이 얼마나 어려운가요? 

A. “세계에서 가장 어려운 대학 수준 수학 시험”으로 꼽힙니다. 매년 수천 명이 응시하지만 만점자는 거의 나오지 않습니다. AI가 12문제를 전부 풀었다는 건 형식 증명 기술이 상당한 수준에 도달했다는 의미입니다. 

Q2. 린(Lean)이란 무엇이고 왜 중요한가요? 

A. 린은 수학 풀이를 컴퓨터가 검증할 수 있는 형태로 작성하는 프로그래밍 언어입니다. 린을 쓰면 풀이의 모든 단계를 컴퓨터가 자동으로 확인해서 실수나 오류를 잡아낼 수 있습니다. AI가 린으로 문제를 풀었다는 건 단순히 답을 찾은 게 아니라 완벽하게 증명했다는 뜻입니다. 

Q3. AI가 수학 문제 푸는 것과 사람이 푸는 것의 차이는 뭔가요? 

A. 사람은 직관과 그림, 간단한 설명으로 문제를 이해하고 풀지만, AI는 모든 논리 단계를 하나하나 명시해야 합니다. 예를 들어 사람에게 몇 문단이면 충분한 증명이 AI에게는 2,000줄 넘는 코드가 될 수 있습니다. 또한 사람과 AI는 완전히 다른 방법을 선택하기도 하는데, 사람이 방정식으로 풀 문제를 AI가 도형으로 푸는 경우도 있습니다. 

기사에 인용된 리포트 원문은 Axiom에서 확인가능하다. 

리포트명: AxiomProver Solves All Problems at Putnam 2025: Proof Release & Commentary 

이미지 출처: 이디오그램 생성 

해당 기사는 챗GPT와 클로드를 활용해 작성되었습니다.