많은 관심이 'CES’에 집중됐던 지난주, 그러나 AI와 수학 커뮤니티에서는 몇가지 발표로 술렁였습니다.
액시엄 매스(Axiom Math)라는 AI 스타트업은 8일(현지시간) '액시엄프로버(AxiomProver)'라는 AI 도구로 세계에서 가장 어렵다는 수학경시대회 ‘퍼트넘 2025(Putnam 2025)’ 문제 12개를 모두 완벽하게 해결했다고 발표했습니다.
여기에는 린(Lean)이라는 도구가 활용됐습니다. 이는 수학적인 주장과 증명을 컴퓨터가 이해하고 검증할 수 있도록 짜인 코드를 말합니다. 즉, 사람이 수학적 증명을 린 코드로 작성하면, 이를 기계가 논리적 단계가 오류 없이 정확한지 자동으로 검사해 오류를 잡아냅니다.
액시엄프로버가 인간 도움 없이 퍼트넘의 12개 문제를 모두 해결하고 형식적으로 검증된 린 증명을 생성했다며, 이는 AI가 복잡한 비정형 문제에 대해 인간 수준의 추론 능력을 보였다는 뜻이라고 설명했습니다.
7일에는 에이스퍼(AceFur)라는 X 아이디를 사용하는 케임브리지대학교 수학과 학생이 이전에는 해결되지 않았던 에르되시(Erdős) 문제 728번을 오픈AI의 'GPT-5.2’가 자율적으로 해결했다고 밝혔습니다.
이 문제는 팩토리얼과 관련된 특정 나눗셈 및 부등식 조건을 만족하는 무한히 많은 정수 a, b, n의 존재에 관한 것입니다. 에르되시 문제는 헝가리 수학자 폴 에르되시가 제시한 것으로, 오랜 기간 수학자 사이에서 연구된 복잡한 정수론 문제입니다. 따라서 AI가 이를 풀 수 있느냐는 이전부터 큰 관심이었습니다.
이 학생은 GPT-5.2가 초기 해법과 증명을 생성했고, 이후 AI 스타트업 하모닉(Harmonic)이 개발한 '아리스토텔레스(Aristotle)'라는 시스템으로 검증했다고 설명했습니다. 아리스토텔레스도 액시엄과 같은 린을 사용해 내용을 검증합니다.
이어 닐 소마니 이클립스 랩스 창립자도 링크드인을 통해 이제까지 풀리지 않았던 에르되시 문제 397번을 증명했으며, 이는 세계적인 수학자인 테렌스 타오 UCLA 교수가 인정했다고 밝혔습니다. 역시 증명은 'GPT-5.2 프로’로 생성됐고, 하모닉을 통해 검증됐습니다.
하모닉도 지난해 11월 아리스토텔레스 시스템으로 거의 30년 동안 미해결 상태로 남아 있던 에르되시 문제 124번을 해결했다고 주장한 바 있습니다.
일련의 사례들은 GPT-5.2를 비롯해 최근 프론티어 모델의 수학 성능이 어디까지 발전했는지를 잘 보여주고 있습니다.
이전에도 대형언어모델(LLM)이 일부 분야에서 인간을 앞선다는 말은 자주 등장했습니다. 그러나 초기에는 LLM이 방대한 지식을 학습하고 그대로 출력하는 수준이었다면, 지난해부터는 추론이 본격 연구되며 양상이 변했습니다. 지난해 5월 국제수학올림피아드(IMO)에서 오픈AI와 구글이 모두 금메달 성적을 거뒀다는 것이 기폭제가 됐습니다.
이제는 AI가 수학과 같은 분야에서 어느 정도의 수준에 도달했는지를 엿볼 수 있게 합니다. 그리고 더 중요한 것은 AI의 활용에 대한 새로운 통찰력을 제공한다는 점입니다.
우선 퍼트넘 문제는 매우 어렵지만, 이미 해답이 알려진 경시 대회 문제입니다. 하지만, 에르되시 문제는 수십년 동안 인간 수학자들이 해결하지 못한 미해결 난제입니다. AI가 이를 해결했다는 주장은, AI가 단순히 훈련 데이터를 모방하는 것을 넘어 새로운 수학적 지식을 창출할 수 있다는 것을 말합니다.
그리고 이들이 밝힌 각종 자료에 따르면, GPT-5.2나 하모닉 시스템은 자율적으로 문제를 분석하고 필요한 아이디어를 생성하며 증명을 구성했습니다. 이는 AI가 인간의 지시를 따르는 도구를 넘어, 급증한 추론 능력으로 이전 모델로는 불가능했던 복잡한 논리적 도약과 개념적 추상화를 수행할 수 있게 됐다는 것을 말합니다.
여기에 GPT-5.2와 하모닉은 '증명을 발견’하는 능력이 핵심입니다. 그러나 액시엄은 '발견된 증명을 검증’하는 데 뛰어나다는 것을 강조했습니다.
액시엄은 퍼트넘 문제를 3가지 유형으로 구분했습니다. ▲인간에게는 쉬웠지만 형식화할 때는 매우 까다로운 문제(부등식, 무게중심, 순열 계수 문제 등) ▲인간이 예상하지 못했던 AI의 해결 문제(게임 이론, 유클리드 기하학, 수열 및 정수론 문제 등) ▲AI와 사람이 서로 다른 수학적 접근 방식을 통해 해결한 문제(행렬 교환, 행렬 합계 부등식 문제 등)입니다.
액시엄은 이번 연구가 "기계에 수학 문제를 어렵게 만드는 요소는 무엇인가"에 대한 질문을 던진다고 전했습니다.
또 "인간에게 어려운 것과 기계에게 어려운 것은 다르다"라고 설명했습니다. 인간은 뛰어난 직관력을 가지고 있지만, 복잡한 분석이 필요한 문제는 지루한 작업에 애를 먹는다는 것입니다. 이에 비해 기계는 반복 작업으로 많은 데이터를 처리하지만, 진짜 능력이 무엇인지는 아직 미지의 영역으로 남아 있다는 것입니다.
이에 따라 "인간과 기계가 서로 다른 분야에서 뛰어난 점과 어려움을 겪는다는 점이 바로 협업의 핵심"이라고 강조했습니다. 기계가 인간의 아이디어를 실시간으로 검증하고, 인간은 기계의 피드백을 검토하여 유망한 방향으로 탐색을 이끌어가는 상호보완적이 구조가 이상적이라고 강조했습니다.
이는 테렌스 타오 교수의 말과 일맥상통합니다. 그는 지난 2024년 첫 추론 모델 'o1’을 테스트한 뒤 "AI를 인간의 조력자로 잘 활용하면 새로운 규모의 과학이 가능할 것"이라고 밝힌 바 있습니다.
그리고 이후 1년여 만에 AI는 빠른 속도로 성능을 끌어 올렸고, 이제는 일부 분야에서 인간을 대체하거나 보완할 수 있는 수준에 도달했습니다. 이전까지 추상적이었던 '인간-AI 협업론’은 이제부터 구체화할 것으로 보입니다.
그리고 많은 전문가가 꼽는 인공일반지능(AGI)의 증거, 즉 인간의 발견을 뛰어넘은 'AI 과학자’가 어떻게 실현될지도 점점 구체화하고 있습니다.
액시엄은 "기계는 원두를 갈고, 인간은 커피의 맛을 음미한다"라는 비유를 들었습니다. AI는 이제 직관의 영역에서 아이디어를 던지고, 검증의 영역에서 오류를 차단하며, 인간의 연구 속도를 혁신적으로 높일 것으로 기대된다는 말입니다.