AlphaProof·AlphaGeometry 2, 국제수학올림피아드 은메달 수준 달성

국제수학올림피아드(IMO)는 오랫동안 인공지능에게 넘기 힘든 벽이었습니다. 전 세계에서 가장 뛰어난 학생들이 수천 시간을 훈련해 출전하는 이 무대에서, 기존 거대언어모델(LLM)들은 그럴듯해 보이지만 논리적으로 구멍투성이인 환각 답변을 내놓기 일쑤였습니다.

Google DeepMind가 이 한계를 크게 넘어섰습니다. 정식 수학 추론 시스템인 'AlphaProof'와 개선된 기하학 모델 'AlphaGeometry 2'를 결합해, 2024년 IMO 6개 문제 중 4개를 완벽하게 풀어냈습니다. 총 42점 만점에 28점을 기록하며 은메달 커트라인 최상단에 도달했습니다. 올해 금메달 기준선인 29점에는 단 1점 모자란 성적입니다.

AlphaZero의 방식을 형식 수학에 접목하다

이번 채점은 필즈상 수상자인 Timothy Gowers 교수와 2024년 IMO 문제선정위원회 위원장인 Joseph Myers 박사가 맡았습니다. 두 전문가는 실제 대회 규정을 그대로 적용해 채점했고, AI가 제출한 4개 문제 풀이에 모두 만점인 7점을 부여했습니다.

가장 돋보인 것은 이번에 처음 공개된 AlphaProof였습니다. 사전 훈련된 언어 모델에 체스와 바둑을 독학했던 AlphaZero의 강화학습 알고리즘을 결합한 시스템입니다. AlphaProof는 대수 2문제와 정수론 1문제를 풀어냈는데, 여기에는 이번 대회 참가자 609명 중 단 5명만 풀어낸 최고 난도 6번 문제도 포함되었습니다.

기하학 전용 모델인 AlphaGeometry 2 역시 문제 4번을 단 19초 만에 증명해 내며 위력을 보였습니다. 다만 두 개의 조합론 문제는 두 시스템 모두 해결하지 못했습니다. 또한 인간 참가자가 4.5시간씩 두 번의 세션을 거치는 반면, AI는 쉬운 문제는 몇 분 만에 풀었지만 어려운 문제는 최대 3일 동안 연산을 돌려야 했습니다.

수학적 환각을 없앤 Lean 언어

자연어 기반 모델은 데이터가 많지만 그럴싸한 오류를 지어내는 치명적인 약점이 있습니다. DeepMind는 이를 극복하기 위해 컴퓨터로 검증 가능한 형식 수학 언어인 'Lean'을 다리에 놓았습니다.

Gemini 모델을 미세조정해 자연어 문제를 Lean 코드로 번역한 뒤, AlphaProof가 올바른 증명 단계를 찾아 헤매도록 만들었습니다. Lean 환경에서는 단계마다 논리적 참·거짓이 즉각 기계적으로 검증되기 때문에 엉터리 논리가 끼어들 틈이 없습니다. AlphaProof는 대회 전 수백만 개의 문제를 풀며 학습했고, 대회 기간 중에도 문제의 변형을 만들어 스스로 증명하며 성능을 끌어올렸습니다.

왜 중요한가

이번 성과는 바둑이나 체스처럼 닫힌 규칙을 가진 게임을 넘어, 고도의 추상적 사고가 필요한 순수 수학에서도 강화학습과 자기 탐색 방식이 통한다는 것을 증명했습니다.

연구자들에게는 든든한 수학 연구 파트너의 등장을 예고합니다. 언어 모델의 치명적 단점인 환각을 기계 검증으로 차단했기 때문에, 수학자들은 복잡하고 지루한 보조정리 증명이나 가설 검증을 AI에게 안심하고 맡길 수 있게 됩니다.

물론 한계도 명확합니다. 자연어 문제를 Lean 언어로 바꾸는 초기 작업은 여전히 인간 전문가의 손을 거쳐야 했습니다. 또한 조합론 문제에 전혀 손을 대지 못했고 한 문제에 사흘간의 연산이 소요되었다는 점은, 아직 AI가 인간 특유의 수학적 직관이나 광범위한 탐색 효율성 면에서 갈 길이 멀다는 것을 보여줍니다. 그럼에도 엄밀한 논리 추론 분야에서 거둔 의미 있는 도약입니다.