딥마인드 '알파프루프 넥서스' 공개…56년 묵은 에르되시 난제 풀었다

반세기 동안 아무도 풀지 못한 수학 난제를 해결하려면 과거에는 세계적인 수학자가 수년간 연구에 매달려야 했습니다.

이제 그 과정은 단 몇 시간의 연산과 수백 달러의 클라우드 비용으로 압축되기 시작했습니다.

Google DeepMind는 기계 검증 기반의 수학 증명 AI 시스템인 'AlphaProof Nexus' 논문을 공개했습니다. 시스템은 353개의 미해결 수학 문제 중 조합론과 그래프 이론에 걸친 9개의 폴 에르되시(Paul Erdős) 난제를 자율적으로 해결했습니다. 이 중 2개 문제는 1970년에 처음 제기된 이후 무려 56년 동안 풀리지 않던 문제였습니다.

여기에 더해 '정수 수열 온라인 백과사전(OEIS)'에 등재된 44개의 미해결 추측까지 연달아 증명해 냈습니다.

LLM과 린(Lean)의 기계 검증 루프

AlphaProof Nexus의 핵심은 대형 언어 모델 특유의 거짓말(환각)을 원천 차단한 데 있습니다.

DeepMind는 LLM을 엄밀한 증명 보조 도구인 '린(Lean)'과 결합했습니다. LLM이 증명 아이디어를 코드로 작성하면, 린이 컴파일러처럼 논리적 엄밀성을 기계적으로 검증합니다.

검증을 통과하지 못하면 피드백을 받아 다시 증명을 생성하고, 검증을 통과할 때까지 이 과정을 끊임없이 반복합니다. 전체 버전 에이전트에는 최적의 경로를 탐색하기 위한 진화 알고리즘까지 탑재됐습니다.

연구진에 따르면 더 단순화된 에이전트 버전으로도 동일한 문제를 풀 수 있었지만 비용이 훨씬 많이 들었습니다. 최적화된 Nexus 시스템은 문제당 불과 수백 달러 수준의 추론 비용으로 증명을 끝마쳤습니다.

오픈AI 발표 직후 나온 맞불

이번 발표의 타이밍도 눈길을 끕니다.

불과 며칠 전 오픈AI는 자사 AI가 80년 된 에르되시 추측을 반증하는 데 성공했다고 발표했습니다. 몇 달 전 10개의 새로운 문제를 풀었다고 주장했다가 슬그머니 철회했던 오픈AI로서는 중요한 성과였습니다.

하지만 DeepMind는 그 바로 다음 날 기계 검증을 거친 9개의 난제 해결 소식을 내놓으며 기술적 우위를 과시했습니다.

다만 한계도 분명합니다. 논문은 완전히 새로운 수학적 구조나 개념적 도구를 발명해야 하는 문제의 경우, 현재 AI 시스템으로는 여전히 해결할 수 없다고 선을 그었습니다.

왜 중요한가

우리는 AlphaProof Nexus가 AI 벤치마크 경쟁의 룰을 근본적으로 바꿨다고 봅니다.

그동안 올림피아드 기출문제를 잘 푸는 '시험형 AI' 경쟁에 머물렀다면, 이제는 답안지가 없는 실제 수학 연구의 미개척지를 파고들기 시작했습니다.

수학 연구자들에게 이 시스템은 위협이 아니라 강력한 탐색 도구가 될 가능성이 큽니다. 인간 학자가 거시적인 가설을 세우고, 지루하고 방대한 검증 작업은 수백 달러짜리 AI 에이전트에 맡겨 병목을 뚫는 연구 방식이 가능해졌습니다.

무엇보다 생성형 모델을 린과 같은 엄격한 검증 시스템 안에 가둬둠으로써, AI의 고질병인 환각을 완벽히 통제한 점이 영리합니다.

새로운 수학 분야를 창시하는 거장의 통찰까지는 아직 갈 길이 멀지만, 기계의 속도로 수십 년 된 난제를 쳐내는 능력만으로도 학계와 산업계에 미칠 파장은 상당합니다.