딥마인드의 AI, 국제 수학 올림피아드 문제 은메달 수준 해결

(deepmind.google)

3P by GN⁺ 2024-07-26 | ★ favorite | 댓글 3개

고난도 수학 추론의 대표 시험대인 IMO 2024에서 Google DeepMind의 AlphaProof와 AlphaGeometry 2가 6문제 중 4문제를 해결해 AI 최초로 은메달권 성적에 도달함
총점 42점 중 28점을 얻었고, 해결한 문제는 모두 만점 처리됐으며 2024년 금메달 기준인 29점에 1점 모자란 수준임
평가는 IMO 채점 규칙에 따라 수학자들이 진행했으며, 대수·수론은 AlphaProof가, 기하는 AlphaGeometry 2가 맡아 서로 다른 추론 방식을 결합함
문제는 먼저 형식 수학 언어로 수동 번역됐고, 학생 대회 시간이 4.5시간씩 2회인 반면 시스템은 한 문제는 몇 분, 다른 문제들은 최대 3일이 걸림
이번 결과는 수학 AI가 단순 계산을 넘어 증명 탐색과 검증에 접근했음을 보여주지만, 형식화 입력과 긴 풀이 시간은 아직 중요한 제약으로 남아 있음

IMO 2024에서 거둔 은메달권 성적

Google DeepMind는 수학 추론 시스템 AlphaProof와 기하 문제 풀이 시스템의 개선판 AlphaGeometry 2를 공개함
두 시스템은 2024년 International Mathematical Olympiad의 6개 문제 중 4개를 해결함
- AlphaProof: 대수 2문제, 수론 1문제 해결
- AlphaGeometry 2: 기하 1문제 증명
- 조합론 2문제는 풀지 못함
각 문제는 7점 만점이며 총점은 42점임
- 시스템은 해결한 4문제에서 모두 만점을 받아 28점을 획득함
- 이는 2024년 IMO 은메달권 상단에 해당함
- 2024년 금메달 기준은 29점이며, 공식 대회에서는 609명 중 58명이 금메달권에 도달함
AI 시스템이 IMO에서 은메달리스트 수준에 해당하는 성적을 낸 첫 사례임

평가 방식과 풀이 조건

문제는 IMO 주최 측이 제공한 대회 문제를 사용함
답안은 IMO의 점수 부여 규칙에 따라 평가됨
- 평가자는 IMO 금메달리스트이자 Fields Medal 수상자인 Prof Sir Timothy Gowers와 IMO 금메달 2회 수상자이자 IMO 2024 Problem Selection Committee 의장인 Dr Joseph Myers임
시스템이 문제를 이해할 수 있도록 모든 문제는 먼저 형식 수학 언어로 수동 번역됨
공식 대회에서 학생들은 4.5시간씩 두 세션 동안 답안을 제출함
- AI 시스템은 한 문제를 몇 분 안에 풀었고, 다른 문제들은 최대 3일이 걸림
AlphaProof가 푼 문제에는 2024년 IMO에서 참가자 5명만 해결한 가장 어려운 문제가 포함됨

AlphaProof: Lean 기반 형식 추론

AlphaProof는 수학 명제를 Lean 형식 언어로 증명하도록 학습하는 시스템임
사전학습 언어 모델과 AlphaZero 강화학습 알고리듬을 결합함
- AlphaZero는 체스, 쇼기, Go를 스스로 익히는 데 사용된 알고리듬임
형식 언어를 쓰면 수학 추론이 포함된 증명의 정확성 검증이 가능함
기존에는 사람이 작성한 형식 증명 데이터가 매우 적어, 머신러닝에서 형식 언어 활용이 제한적이었음
자연어 기반 접근은 훨씬 많은 데이터를 사용할 수 있지만, 그럴듯해 보이면서도 잘못된 중간 추론 단계나 해답을 만들어낼 수 있음
DeepMind는 Gemini 모델을 파인튜닝해 자연어 문제를 형식 명제로 자동 번역하도록 하고, 다양한 난도의 형식 문제 라이브러리를 만듦
AlphaProof는 문제가 주어지면 해답 후보를 생성한 뒤, Lean에서 가능한 증명 단계를 탐색해 이를 증명하거나 반증함
- 발견되고 검증된 증명은 AlphaProof의 언어 모델을 강화하는 데 사용됨
- 이 반복 과정이 더 어려운 문제를 푸는 능력을 높이는 데 쓰임
IMO 준비 과정에서는 수 주 동안 수백만 개 문제를 증명하거나 반증하며 학습함
- 대회 중에도 문제의 자체 생성 변형에 대한 증명을 강화하면서 완전한 풀이를 찾는 학습 루프가 적용됨

AlphaGeometry 2: 더 어려운 기하 문제로 확장

AlphaGeometry 2는 기존 AlphaGeometry의 크게 개선된 버전임
이 시스템은 신경망과 기호 추론을 결합한 뉴로-심볼릭 하이브리드 구조임
- 언어 모델은 Gemini를 기반으로 함
- 이전 버전보다 한 차수 더 많은 합성 데이터로 처음부터 학습됨
더 많은 데이터와 개선된 모델 덕분에 물체의 움직임, 각도·비율·거리 방정식이 포함된 더 어려운 기하 문제를 다룰 수 있게 됨
AlphaGeometry 2의 기호 엔진은 이전 버전보다 두 자릿수 배 빠름
새 문제를 받을 때는 새로운 지식 공유 메커니즘으로 서로 다른 탐색 트리의 고급 조합을 활용해 더 복잡한 문제를 처리함
최근 25년 IMO 기하 문제 해결률: {b:83,53}
- 2024년 대회 전 기준으로 AlphaGeometry 2는 최근 25년간 IMO 기하 문제의 83%를 풀 수 있었음
- 이전 AlphaGeometry의 해결률은 53%였음
IMO 2024에서는 Problem 4를 형식화 입력 후 19초 안에 해결함

자연어 추론과 향후 활용

IMO 작업의 일부로, DeepMind는 Gemini와 최신 연구를 기반으로 한 자연어 추론 시스템도 실험함
이 시스템은 문제를 형식 언어로 번역할 필요가 없으며, 다른 AI 시스템과 결합될 수 있음
2024년 IMO 문제에도 이 접근을 테스트했고 결과는 유망한 수준으로 평가됨
AlphaProof의 더 기술적인 방법론은 Nature 논문으로 공개됨
DeepMind는 수학자가 AI 도구와 함께 가설을 탐색하고, 오래된 문제에 새로운 접근을 시도하며, 증명의 시간이 많이 드는 요소를 빠르게 완료하는 미래를 목표로 함

chabulhwi 2024-07-26 [-]

형식 수학 라이브러리의 개발에 이바지하는 수학자가 많아질수록 성능이 좋은 수학 AI를 만들기가 수월해질 것입니다. 자신이 직접 린(Lean) 증명 보조기의 언어로 형식화한 수학 이론을 린의 수학 라이브러리 매스리브(Mathlib)에 옮기고 있는 한국인은 제가 알기로 현재 3명 있습니다.

저는 지난해에 매스리브를 린 3에서 린 4로 옮기는 작업에 조금 참여했고, 올해에는 린 4 배터리 라이브러리의 미해결 정리 하나를 증명했습니다.

답변달기

GN⁺ 2024-07-26 [-]

Hacker News 의견들

이 발표에 정말 기대가 크지만, “먼저 문제를 시스템이 이해할 수 있도록 형식적 수학 언어로 사람이 직접 번역했다”는 문장이 얼마나 많은 일을 떠안고 있는지 불분명함
기하가 아닌 문제들은 모두 “...인 모든 X를 구하라” 형태였고, 정리 문장은 “모든 X의 집합이 {foo}임을 보인다” 형태였음
https://storage.googleapis.com/deepmind-media/DeepMind.com/B...의 내려받을 수 있는 풀이만 봐서는 번역 단계에서 사람이 {foo}를 정했는지, 컴퓨터가 찾았는지 알기 어려움. 컴퓨터가 찾았다고 믿고 싶지만 확인할 근거를 못 찾겠음
- 컴퓨터가 답을 직접 찾았음. 즉 P1에서는 짝수 정수, P2에서는 {1,1}, P6에서는 2를 찾았고, 각 경우에 Lean 증명도 함께 제시했음
- 일반적으로 말하면 그 번역 단계는 증명 단계보다 훨씬 쉬움. 자동 번역의 문제는 번역 결과가 틀릴 수 있다는 것임
  사람도 형식 기법을 직접 다룰 때 이런 일이 자주 생기니, 연구자들은 LLM이든 다른 도구든 결국 모든 번역을 감사해야 한다고 판단했을 듯함
- 링크된 페이지에는 “문제 문장은 사람이 Lean으로 형식화했지만, 문제 문장 안의 답은 에이전트가 생성하고 형식화했다”고 되어 있음
  다만 에이전트에 어떤 초기 형식이 주어졌기에 이 단계가 가능했는지는 불명확함
- 훈련 데이터를 만드는 데 쓰인 형식화 도구가 있는데 여기서는 쓰지 않은 점이 흥미로움. 아직 충분히 신뢰할 수 없었나 봄
- “문제가 주어지면 AlphaProof는 해 후보를 생성한 다음 Lean에서 가능한 증명 단계를 탐색해 그것을 증명하거나 반증한다”는 설명으로 들림
  즉 AlphaProof가 어떤 형태의 “문제”를 받고, “...인 모든 X를 구하라”를 어떻게 형식화했든 간에, 후보 정리들을 아마 Lean으로 생성하는 듯함. 예컨대 집합이 어떤 공식 P에 대해 {n: P(n)} 꼴이라는 식일 수 있음. 그다음 증명을 탐색함
  만약 AlphaProof가 {foo}를 찾은 게 아니라 주어진 것이라면, 문제를 풀었다고 주장하는 건 꽤 터무니없을 것 같음. 그래도 이 결과에는 매우 기대가 큼
확실히 인상적이지만 IMO가 언급될 때는 주의점이 필요함. 메달은 참가자, 즉 고등학생의 50%에게 주어지고 금·은·동 비율은 1:2:3이라서 금·은 수상자는 전체 참가자의 상위 25%에 들어감
따라서 “AI가 IMO 문제를 학생 75%보다 잘 풀었다”는 표현이 되며, 사실 이것도 더 인상적일 수 있음
하지만 “한 문제는 몇 분, 나머지 각 문제는 최대 3일”이라는 조건은 학생들이 받는 9시간과 다르기 때문에 진정한 비교라고 보기 어려움. 학생들에게도 9시간 대신 최대 15일이 주어졌다면 이 점수를 맞추거나 넘는 사람이 더 많았을 것임
실제로는 AI가 학생들에게 주어진 9시간 안에 한 문제만 푼 셈이라 메달권과는 거리가 멀었을 가능성이 큼. 이렇게 인상적인 결과를 굳이 사과와 오렌지 비교로 흐릴 필요가 있나 싶음
더 객관적으로, 시간이 더 걸렸지만 전체 문제의 X%를 풀었다거나 N점 만점에 X점을 받았다고 보고하면 됨
- IMO 참가자들을 만나본 적이 있는데, 정말 말도 안 되게 똑똑함. 그런 집단을 접하기 전에는 사람이 그 정도로 똑똑할 수 있다고 상상하지 못했음. 그러니 고등학생 전체의 0.01% 중 상위 25%에 가깝다고 봐야 함
  여기서 시간은 그다지 흥미로운 축이 아님. 인간은 거대한 GPU 클러스터와 같은 CPU를 쓰지 않기 때문임. “충분한 자원이 주어졌을 때 해에 도달할 수 있는가”라는 이분법이 더 흥미롭고, GPT/Claude의 답은 명확히 아니었음
- “참가자 고등학생의 50%에게 메달이 주어진다”는 말이 헷갈릴 수 있는데, 여기서 말하는 고등학생은 일반 고등학생 표본이 아님. 아는 바로는 각 나라에서 경시 문제 풀이 최강자 약 6명으로 구성된 대표팀임
- 개인적으로는, Google의 입장은 아니지만, 올해 금메달을 못 받은 유일한 이유는 문제 선택 운이 나빴던 것과 P3/P5에서 부분 점수를 노리지 않았기 때문이라고 봄
  컷오프에 매우 가까웠고, 보통 약간의 진전만 있어도 1점은 받을 수 있음. 다만 기술적인 이유로 금메달을 땄다는 식의 보도는 좋지 않았을 테니, 논란 없는 은메달에 만족한 것 같음
- 인간에게 시간을 더 주는 것과 컴퓨터 프로그램에 시간을 더 주는 것의 핵심 차이는, 역사적으로 후자를 더 빠르게 실행하게 만드는 데 훨씬 성공해 왔다는 점임
- DeepMind 연구 대부분은 회사 입장에서는 비용 센터임. 이런 보도자료는 투자자와 대중에게 지속 투자를 정당화하는 데 도움이 됨
이건 진짜임. AlphaGeometry는 많은 무차별 탐색으로 매우 제한된 문제 집합을 푼 것이었음
이번 방법은 훨씬 넓고, 수학을 하는 방식에 큰 영향을 줄 것이라고 봄. 자연어 수학에서 형식화된 수학으로 이어지고, 거기서 형식화와 증명을 모두 훈련할 수 있는 자기 공급 파이프라인을 실제로 구현하고 있음
원칙적으로 이 파이프라인은 보조 정의와 보조정리 생성 같은 기초적인 이론 구축도 배울 수 있음. 증명 보조의 성배에 가깝고, 우리가 자연스럽게 만드는 수학 대부분을 형식화하게 해줄 것이라 생각함. 인간은 사후 엄밀화 방식으로 일하고, 세부를 채우는 일은 기계가 보조하게 될 것임
- 동의함. 큰 진전임. 기하 문제는 다항식 방정식계로 번역한 뒤 잘 알려진 컴퓨터 대수 알고리즘으로 풀 수 있어서 다른 범주에 속함
  반대로 이런 개방형 형식화는 진전이 매우 느리고 점진적이던 영역임. 5년 전 인접 분야에서 일했는데, 이 결과는 전통적인 자동 추론 기법으로는 도달 불가능한 수준이라고 봐도 됨
  진짜 자동 정리 증명은 순수수학보다 훨씬 넓게 유용함. 예를 들어 작은 프로그래밍 언어의 공리적 의미론을 Lean으로 적고 “이 명세를 만족하는 프로그램이 존재함을 보여라” 같은 질문을 던질 수 있음
  이 접근이 확장된다면 지난 몇 년간 나온 어떤 기계학습 응용보다 중요해질 것임
- 탐색을 낮춰 보면 안 됨. 무차별처럼 보일 수 있지만, 탐색은 바둑에서 인간 수준을 넘었고 IMO 은메달 수준까지 갔음
  우리를 만든 진화도 엄청난 무차별 시도로 작동한 탐색이고, 과학적 방법의 연구도 본질적으로 탐색임
- 이미 이 분야를 하는 사람들이 있음
  https://leandojo.org/
  https://machine-learning-for-theorem-proving.github.io/
  https://www.youtube.com/watch?v=P5ew0BrRm_I
  https://paperswithcode.com/task/automated-theorem-proving
  https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
  https://github.com/RiccardoBiosas/LeanGPT
- 이런 시스템은 수학 연구 바깥에서 훨씬 더 유용할 것 같음
  유용한 일을 하려면 아주 어려운 문제를 증명할 필요가 없음. 간단한 것만 증명해도 충분한 경우가 많음. 언어 모델에게 작업 완료, 항목 정리, 일정 조율, X를 수행하는 코드 작성 등을 시키면 결과를 바로 신뢰하기 어렵지만, 시스템이 문제 일부를 논리로 번역하고 해를 찾을 수 있다면 훨씬 더 신뢰할 수 있게 됨
- 아님. 해법을 찾기 위해 검색 엔진을 쓸 수 있게 해준 것과 비슷할 뿐, 그 이상은 아님
핵심이 좀 묻혀 있는데, 이들은 Lean을 쓰고 있음
이건 수학 문제를 넘어서 중요함. 기계학습 모델이 증명 시스템과 씨름하게 만드는 건 일반적인 헛소리를 피하는 좋은 방법임
앞으로 더 많은 사람이 Lean이나 비슷한 시스템에서 타입을 작성해, 프롬프트를 쓰는 훨씬 나은 방식으로 활용하길 바람
- AlphaProof가 분명 대단하긴 하지만, IMO에서 인간에게는 없는 이점도 컴퓨터에 줌. 머릿속으로 Gröbner 기저를 만들 사람은 없지만, polyrith는 여덟 글자만 치면 됨. AlphaProof가 nlinarith를 쓰는 것도 봤음
- 놀라움. 막 Lean에 연결하면 끝내주겠다고 댓글을 달려던 참이었음. 고등 수학은 앞으로 이렇게 가야 할 것 같음. 주요 증명이 너무 복잡해져서 거의 아무도 전체 조각을 다 이해하지 못하기 때문임
  1. https://lean-lang.org/
- 이걸로 리만 가설도 노리겠네, hehe
Tim Gowers가 주요 주의점을 설명하고 맥락화한 좋은 짧은 개요가 있음. 그는 Fields 메달리스트이고 이번 작업에도 참여했음: https://x.com/wtgowers/status/1816509803407040909
맞는 말이지만, 각 나라 대표팀에 들어가는 것 자체가 매우 험난한 과정임. 지역 수학 올림피아드, 전국 수학 올림피아드 등 매 단계에서 잔혹하게 걸러짐
그 뒤에는 이 엘리트 집단을 위한 추가 훈련이 이어지고, 경우에 따라 추가 선발도 있을 수 있음
요컨대 한 나라의 IMO 대표팀에 뽑히는 것 자체가 큰일이고, 그 안에서 금·은메달을 따는 건 그냥 엄청난 성취임
- 어떤 나라들은 이 아이들을 1년 내내 학교에서 빼내 IMO 훈련에 집중하게 하고, 자국 최고 대학 입학을 보장해 주기도 함
  출처는 IMO 은메달을 딴 친구임
이 일을 하면서 돈 받는 사람들이 정말 부러움. 엄청 재미있어 보이고, 이런 식으로 최첨단 수준을 밀어 올리는 건 굉장히 만족스러울 듯함
- 꼭 그렇진 않을 수 있음. 아주 만족스러워야 할 일들이 지독하게 지루하거나 심지어 유해하게 흘러간 적도 많고, 반대로 겉보기엔 평범한 일이 정말 흥미로웠던 적도 있음
  업무 만족도에서는 주제보다 업무 환경이 더 중요하다고 봄. 세상을 바꾸는 주제를 다루더라도 팀이 엉망이면 힘든 시간을 보내게 됨. 어떤 사람들은 모든 재미를 빨아들이는 재주가 있고, 사내 정치는 어디에나 있으며, 특히 세상을 바꾸는 주제일수록 더 그럼
  반대로 고객 데이터를 데이터베이스에 넣는 것처럼 가장 지루해 보이는 주제라도, 친절한 팀, 잘 설계된 아키텍처, 실험과 지식 공유 시간이 있으면 최고의 시간을 보낼 수 있음. 그냥 잘 작동하는 단순한 것의 아름다움을 점점 더 높이 평가하게 됐음. 그런 건 과학적 돌파구보다도 더 드물 수 있음
  물론 훌륭한 업무 환경과 훌륭한 주제가 함께 올 수도 있고, 그건 잭팟에 가까워서 부러워할 만함
- 이 분야, 구체적으로 LLM 사전학습 쪽에서 일함. 겉보기보다 그렇게 화려하지 않음. 거대한 YAML을 다루고 대규모로 정규식을 쓰는 일이 포함됨. 물론 조금 단순화한 말이긴 함
  이런 일을 할 수 있다는 점에 신나고 감사해야겠지만, 조악한 도구들이 일의 즐거움을 많이 빼앗아 감
- 아마 jealous가 아니라 envious라고 해야 할 듯함
- 우리가 할 수 있는 최선은 계속 최신 정보를 따라가고 지지하는 것임
- 지금은 K8s용 3,292,329줄짜리 YML을 다시 설정해야 하는 시간 아닌가
  (/s)
기계가 인간보다 체스를 잘 둔 지는 수십 년이 됐음
그래도 아무도 신경 쓰지 않음. 모두 Magnus Carlsen을 보느라 바쁨
우리는 인간이기 때문에 다른 인간이 하는 일에 관심을 가짐. 기계에는 그것이 우리에게 도움이 되는 한에서만 관심을 둠
이 원리는 일과 예술에도 넓게 확장됨. 인간이 존재하는 한, 이런 영역에서 인간의 자리는 항상 남아 있을 것임
- AI가 아무리 체스와 예술을 더 잘해도 인간은 계속 즐길 것임. 마찬가지로 수학을 취미로 공부하는 사람들도 아마 계속 있을 것임
  하지만 가까운 미래에 AI가 대부분 또는 전부 발견하지 않은 새로운 수학 진전을 발표하는 수학자가 남아 있을지는 매우 의심스러움. 인간이 최초 질문을 던졌다는 이유로 증명 공로를 받을 수는 있겠지만, 컴퓨터가 의미 있는 수학 문제를 쉽게 풀 수 있는데도 인간이 더 느리고 비싸게 풀도록 고집할 세상은 거의 없음
- 맞지만, 예를 들어 AI가 골드바흐 추측을 증명한다면 그건 엄청난 일임
- 소비자 입장에서는 육가공 공장이나 Amazon 물류창고가 5000명을 고용하든 5명을 고용하든 차이가 없음
  예술에는 이 원리가 확실히 적용되지만, 일에는 일부 또는 대부분에만 적용됨
- 수학이 체스나 예술과 달리 실제로 유용하다고 믿는 사람들이 있음. 대부분의 수학자들은 그렇게 생각하지 않겠지만, 잠시 이 미친 생각을 받아들여 보자면, 증명은 “이 수학 조각을 올바르게 적용했다”고 알려주는 도구일 뿐임
  그러면 증명을 이해할 필요가 없고, 어딘가의 수학자가 그 증명을 완전히 이해하는지 아무도 신경 쓰지 않음. 기계가 증명을 찾고 확인하는 데 우리보다 더 나은 것은 괜찮고, 오히려 예상 가능한 일이 됨
- 이 원리는 수학 증명에는 잘 확장되지 않는다고 봄. 증명은 만드는 것보다 검증하는 것이 훨씬 훨씬 쉬우며, 두 번째 증명은 각주에 불과해짐
  많은 수학자가 그런 일에 매달리고 싶어 하진 않을 것임. 다만 IMO와 연구 수학의 최전선 사이에는 아직 큰 거리가 있음
정리 증명은 말도 안 되게 큰 탐색 공간을 가진 1인용 게임이라서, AGI보다 훨씬 전에 풀릴 것이라고 늘 생각했음
개인적으로 AlphaProof의 가장 큰 기여자는 Lean과 Mathlib 뒤에 있는 사람들이라고 봄. 수학 전체를 형식화한다는 벅찬 일을 떠맡았기 때문임
수학 논문의 형식화 부족이 자동화 시도를 계속 죽였음. AI 연구자들이 저자 고유의 표기, 암묵적 지식, 생략된 증명 단계 같은 인간적 요소와 씨름해야 했기 때문임
- “정리 증명은 엄청나게 큰 탐색 공간을 가진 1인용 게임이라 AGI보다 훨씬 전에 풀릴 것”이라는 말은 이상하게 들림
  AGI라는 용어 자체가 정의되지 않았다고 보지만, 왜 “일반적으로 지능적인 무언가”, 즉 인간 중앙값 수준 지능을 만드는 일이 “Terrence Tao보다 수학을 잘하는 것”보다 훨씬 어렵다고 예상하는지 모르겠음
- 그들이 수학 전체를 형식화한 건 아님. IMO에는 전체 수학이 필요 없으니 다행이긴 함. 하지만 IMO에 충분한 만큼도 형식화하지 못했음. 아마 그래서 조합론 문제를 못 풀었을 것임
가장 좋은 논의는 여기 있음: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...