GN⁺: 딥마인드의 AI, 국제 수학 올림피아드 문제 은메달 수준 해결
(deepmind.google)- 구글 딥마인드의 AlphaProof와 AlphaGeometry 2가 국제 수학 올림피아드 문제를 풀어냄
- AlphaProof: 강화 학습 기반의 수학적 추론 시스템
- AlphaGeometry 2: 개선된 기하학 문제 해결 시스템
- 두 시스템이 올해 국제 수학 올림피아드(IMO)에서 6문제 중 4문제를 해결하여 은메달 수준의 성과를 달성함
복잡한 수학 문제 해결에서의 AI 성과
-
IMO 소개
- 1959년부터 매년 개최되는 가장 오래되고 권위 있는 청소년 수학 대회
- 대회 문제는 대수학, 조합론, 기하학, 수론 등에서 출제됨
- Fields Medal 수상자 중 다수가 IMO 출신
-
AI 시스템의 IMO 도전
- AlphaProof와 AlphaGeometry 2가 올해 IMO 문제를 해결
- 문제는 공식 대회 규칙에 따라 점수화됨
- AlphaProof는 대수학 문제 2개와 수론 문제 1개를 해결
- AlphaGeometry 2는 기하학 문제 1개를 해결
- 두 조합론 문제는 해결하지 못함
- 총 42점 중 28점을 획득하여 은메달 수준의 성과를 달성
AlphaProof: 형식적 추론 접근법
-
AlphaProof의 작동 원리
- 수학적 명제를 형식 언어 Lean으로 증명
- 사전 훈련된 언어 모델과 AlphaZero 강화 학습 알고리즘 결합
- 자연어 문제를 형식 명제로 번역하여 다양한 난이도의 문제를 해결
- 문제를 제시하면 AlphaProof는 해결 후보를 생성하고 증명 또는 반증
- 증명된 결과는 AlphaProof의 언어 모델을 강화하여 더 어려운 문제 해결 능력 향상
-
훈련 과정
- 수백만 개의 문제를 증명하거나 반증하며 훈련
- 대회 기간 동안에도 훈련 루프를 적용하여 문제 변형을 증명
더 경쟁력 있는 AlphaGeometry 2
-
AlphaGeometry 2의 개선점
- Gemini 기반의 언어 모델과 신경-기호 하이브리드 시스템
- 이전 버전보다 10배 더 많은 합성 데이터로 훈련
- 기하학 문제 해결 속도와 정확도 향상
- 새로운 문제 해결 시 지식 공유 메커니즘 사용
-
IMO 2024 성과
- 과거 25년간의 IMO 기하학 문제 중 83% 해결
- 올해 대회에서 문제 4를 19초 만에 해결
수학적 추론의 새로운 프론티어
-
자연어 추론 시스템 실험
- Gemini 기반의 자연어 추론 시스템 실험
- 형식 언어로 번역하지 않고 문제 해결 가능
- 다른 AI 시스템과 결합 가능성 탐색
-
미래 전망
- 수학자들이 AI 도구와 협력하여 새로운 가설 탐구, 문제 해결 접근법 시도, 증명 과정 단축 가능
- Gemini와 같은 AI 시스템이 수학 및 일반 추론 능력 향상
GN⁺의 정리
- AlphaProof와 AlphaGeometry 2는 수학적 추론에서 AI의 가능성을 보여줌
- 국제 수학 올림피아드에서 은메달 수준의 성과를 달성하여 AI의 수학 문제 해결 능력을 입증
- 수학자들이 AI와 협력하여 새로운 문제 해결 접근법을 탐구할 수 있는 가능성을 열어줌
- 유사한 기능을 가진 프로젝트로는 OpenAI의 GPT-3와 같은 자연어 처리 모델이 있음
형식 수학 라이브러리의 개발에 이바지하는 수학자가 많아질수록 성능이 좋은 수학 AI를 만들기가 수월해질 것입니다. 자신이 직접 린(Lean) 증명 보조기의 언어로 형식화한 수학 이론을 린의 수학 라이브러리 매스리브(Mathlib)에 옮기고 있는 한국인은 제가 알기로 현재 3명 있습니다.
저는 지난해에 매스리브를 린 3에서 린 4로 옮기는 작업에 조금 참여했고, 올해에는 린 4 배터리 라이브러리의 미해결 정리 하나를 증명했습니다.
Hacker News 의견
-
첫 번째 의견
- 이 프로젝트에 대해 매우 흥분하지만, 수학 문제를 형식적 언어로 번역하는 과정에서 컴퓨터가 얼마나 기여했는지 불분명함
- 다운로드 가능한 솔루션에서 인간이 번역 과정에서 결정한 것인지 컴퓨터가 찾은 것인지 명확하지 않음
-
두 번째 의견
- IMO에서 메달은 참가자의 50%에게 수여되며, 금, 은, 동 메달의 비율은 1:2:3임
- AI가 75%의 학생들보다 더 잘 해결했다는 것은 인상적임
- 그러나 AI가 문제를 해결하는 데 걸린 시간은 학생들이 시험에서 주어진 시간과 다르므로 직접 비교는 부적절함
-
세 번째 의견
- AlphaGeometry는 제한된 문제를 해결했지만, 이번 방법은 더 광범위하게 수학에 영향을 미칠 것임
- 자연어 수학을 형식화된 수학으로 변환하는 파이프라인을 구현하고 있으며, 이는 기본 이론 구축도 학습할 수 있음
- 이는 증명 보조의 성배이며, 인간이 더 자연스럽게 수학을 형식화할 수 있게 도와줄 것임
-
네 번째 의견
- 시스템이 문제를 해결하는 데 3일이 걸렸다면, 이는 단순한 무차별 대입과 다를 바 없음
- 이는 진정한 추론이 아님
-
다섯 번째 의견
- Lean을 사용하고 있음
- 이는 수학 문제뿐만 아니라 일반적으로 무의미한 결과를 피하는 데 중요함
- 더 많은 사람들이 Lean과 같은 시스템에서 타입을 작성하기를 희망함
-
여섯 번째 의견
- 이 프로젝트에 참여하는 사람들을 부러워함
- 최첨단 기술을 발전시키는 것이 매우 재미있고 만족스러울 것임
-
일곱 번째 의견
- 최고의 논의는 LeanProver의 Zulip 채팅에서 이루어짐
-
여덟 번째 의견
- Fields 메달리스트인 Tim Gowers가 주요 주의사항을 설명하고 맥락을 제공하는 좋은 개요를 제공함
-
아홉 번째 의견
- 정리 증명은 매우 큰 탐색 공간을 가진 단일 플레이어 게임임
- AlphaProof의 가장 큰 기여자는 Lean과 Mathlib의 개발자들임
- 수학 논문에서 형식화의 부족이 자동화 시도를 방해했음
-
열 번째 의견
- 기계는 수십 년 동안 체스에서 인간보다 뛰어났음
- 그러나 사람들은 여전히 Magnus Carlsen을 보고 있음
- 인간은 다른 인간의 행동에 관심이 있음
- 기계는 인간에게 도움이 되는 한에서만 관심을 가짐