소식

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

기계 심장 보고서

머신하트 편집부

Gemini 대형 모델과 AlphaZero 강화학습 알고리즘을 사용하여 기하학, 대수학, 정수론을 마스터할 수 있습니다.

AI의 경우 수학 올림피아드는 더 이상 문제가 되지 않습니다.

목요일에 Google DeepMind의 인공 지능은 AI를 사용하여 올해 국제 수학 올림피아드 IMO의 실제 문제를 해결하는 위업을 달성했으며 금메달 획득에 한 걸음 더 다가섰습니다.

지난주 막 끝난 IMO 대회에는 대수학, 조합론, 기하학, 수론 등 6개 문제가 출제됐다. 구글이 제안한 하이브리드 AI 시스템은 4문제를 맞혀 28점을 얻어 은메달 수준에 이르렀다.

이달 초 UCLA 종신 교수 테렌스 타오(Terence Tao)가 상금 100만 달러의 AI 수학 올림피아드(AIMO Progress Award)를 추진했는데, 예상외로 7월 이전에 AI 문제 해결 수준이 이 수준으로 향상됐다.

IMO, 질문을 동시에 수행하고 가장 어려운 질문을 올바르게 처리하세요.

IMO는 1959년부터 매년 개최되는 젊은 수학자들을 위한 가장 오래되고 규모가 크며 권위 있는 대회입니다. 최근 IMO 대회는 머신러닝 분야에서도 거대한 도전으로 널리 인식돼 인공지능 시스템의 고급 수학적 추론 능력을 측정하는 이상적인 벤치마크가 되고 있다.

올해 IMO 대회에서 DeepMind 팀이 공동으로 개발한 AlphaProof와 AlphaGeometry 2는 획기적인 돌파구를 달성했습니다.

그 중 AlphaProof는 정형수학적 추론을 위한 강화학습 시스템이고, AlphaGeometry 2는 DeepMind의 기하학 해결 시스템인 AlphaGeometry를 개선한 버전입니다.

이 획기적인 발전은 과학과 기술의 새로운 영역을 여는 고급 수학적 추론 능력을 갖춘 일반 인공 지능(AGI)의 잠재력을 보여줍니다.

그렇다면 DeepMind의 AI 시스템은 어떻게 IMO 대회에 참가하게 되었나요?

간단히 말해서 이러한 수학적 문제는 AI 시스템이 이해할 수 있도록 먼저 수동으로 공식적인 수학 언어로 번역됩니다. 공식 대회에서는 인간 참가자들이 두 세션(2일)에 걸쳐 답변을 제출하며, 각 세션당 시간 제한은 4.5시간입니다. AlphaProof+AlphaGeometry 2로 구성된 AI 시스템은 한 문제는 몇 분 만에 해결했지만, 다른 문제를 해결하는 데는 3일이 걸렸습니다. 규칙을 엄격하게 준수하더라도 DeepMind 시스템은 시간 초과되었습니다. 어떤 사람들은 이것이 많은 무차별 대입 크래킹을 포함할 수 있다고 추측합니다.

AlphaProof는 답을 결정하고 그 정확성을 입증함으로써 두 가지 대수학 문제와 하나의 정수론 문제를 해결했다고 구글은 말했습니다. 여기에는 올해 IMO에서 5명의 참가자만이 해결한 대회에서 가장 어려운 문제가 포함됩니다. 그리고 AlphaGeometry 2는 기하학 문제를 증명합니다.

AI가 제공하는 솔루션: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

IMO 금메달리스트이자 필즈 메달리스트인 Timothy Gowers와 IMO 2회 금메달리스트인 IMO 2024 문제 선택 위원회 의장인 Joseph Myers 박사는 IMO 채점 규칙에 따라 결합 시스템이 제공하는 솔루션의 점수를 매겼습니다.

6개 질문은 각각 7점으로 최대 총점은 42점입니다. DeepMind의 시스템은 최종 점수 28점을 받았습니다. 이는 해결한 문제 4개 모두 만점을 받았음을 의미합니다. 이는 은메달 부문에서 가장 높은 점수에 해당합니다. 올해 금메달 기준점은 29점으로, 공식 대회에 출전한 선수 609명 중 58명이 금메달을 획득했다.

이 그래프는 IMO 2024에서 인간 경쟁자와 비교하여 Google DeepMind의 인공 지능 시스템의 성능을 보여줍니다. 총점 42점 중 28점을 획득해 대회 은메달리스트와 같은 수준에 이르렀다. 게다가 올해는 29점만 있어도 금메달을 딸 수 있다.

AlphaProof: 형식적 추론 방법

Google이 사용하는 하이브리드 AI 시스템 중 AlphaProof는 공식 언어 Lean을 사용하여 수학적 진술을 증명하는 자가 훈련 시스템입니다. 사전 훈련된 언어 모델과 AlphaZero 강화 학습 알고리즘을 결합합니다.

그 중에서 형식언어는 수학적 추론 증명의 정확성을 형식적으로 검증하는 데 중요한 이점을 제공합니다. 지금까지는 사람이 작성한 데이터의 양이 매우 제한적이었기 때문에 머신러닝에서는 이 기능이 제한적으로 사용되었습니다.

이와 대조적으로 자연어 기반 방법은 더 많은 양의 데이터에 액세스할 수 있음에도 불구하고 합리적으로 보이지만 잘못된 중간 추론 단계와 솔루션을 생성합니다.

Google DeepMind는 Gemini 모델을 미세 조정하여 자연어 문제 설명을 공식적인 설명으로 자동 번역함으로써 이러한 두 보완적인 필드 사이에 다리를 구축함으로써 다양한 난이도의 형식 문제로 구성된 대규모 라이브러리를 생성합니다.

수학적 문제가 주어지면 AlphaProof는 후보 솔루션을 생성한 다음 Lean에서 가능한 증명 단계를 검색하여 이를 증명합니다. 발견되고 검증된 각 증명 솔루션은 AlphaProof의 언어 모델을 강화하고 이후의 더욱 어려운 문제를 해결하는 능력을 향상시키는 데 사용됩니다.

AlphaProof를 교육하기 위해 Google DeepMind는 IMO 대회가 열리기 몇 주 동안 다양한 어려움과 주제를 다루는 수백만 개의 수학 문제를 입증하거나 반증했습니다. 완전한 솔루션을 찾을 때까지 자체 생성 경쟁 문제 변형에 대한 증거를 강화하기 위해 경쟁 중에 훈련 루프도 적용됩니다.

AlphaProof 강화 학습 훈련 루프 프로세스 인포그래픽: 약 백만 개의 비공식 수학 문제가 공식 네트워크를 통해 공식 수학 언어로 변환됩니다. 그런 다음 솔버는 문제의 증명 또는 반증을 찾기 위해 네트워크를 검색하고 AlphaZero 알고리즘을 사용하여 더 어려운 문제를 해결하기 위해 점차적으로 스스로 훈련합니다.

더욱 경쟁력 있는 AlphaGeometry 2

AlphaGeometry 2는 올해 Nature지에 등장한 수학적 AI AlphaGeometry를 대폭 개선한 버전입니다. 이는 언어 모델이 Gemini를 기반으로 하고 이전 모델보다 훨씬 더 많은 합성 데이터를 바탕으로 처음부터 훈련되는 신경 기호 하이브리드 시스템입니다. 이는 모델이 물체의 움직임과 각도, 비율 또는 거리의 방정식을 포함하여 더욱 까다로운 기하학적 문제를 해결하는 데 도움이 됩니다.

AlphaGeometry 2는 이전 버전보다 2배 빠른 기호 엔진을 갖추고 있습니다. 새로운 문제가 발생하면 새로운 지식 공유 메커니즘을 통해 다양한 검색 트리의 고급 조합을 통해 보다 복잡한 문제를 해결할 수 있습니다.

올해 대회 이전에 AlphaGeometry 2는 지난 25년 동안 모든 역사적 IMO 기하학 문제의 83%를 해결할 수 있었는데, 이는 이전 버전의 53%에 불과했습니다. IMO 2024에서 AlphaGeometry 2는 공식화를 받은 후 19초 이내에 문제 4를 해결했습니다.

질문 4의 예에서는 ∠KIL과 ∠XPY의 합이 180°임을 증명해야 합니다. AlphaGeometry 2는 ∠AEB = 90°가 되도록 선 BI 위에 점 E를 구성하는 것을 제안합니다. 점 E는 선분 AB의 중간점 L에 의미를 부여하는 데 도움을 주어 ABE ~ YBI 및 ALE ~ IPC와 같은 유사한 삼각형 쌍을 많이 만들어 결론을 증명합니다.

Google DeepMind는 또한 IMO 작업의 일환으로 연구원들이 고급 문제 해결 능력을 달성하기 위해 Gemini와 최첨단 자연어 추론 시스템을 기반으로 한 새로운 자연어 추론 시스템을 실험하고 있다고 보고했습니다. 이 시스템은 질문을 공식 언어로 번역할 필요가 없으며 다른 AI 시스템과 결합될 수 있습니다. 올해 IMO 경쟁 문제 테스트에서는 “큰 잠재력을 보여줬다”고 한다.

Google은 수학적 추론을 발전시키기 위해 AI 방법을 계속 연구하고 있으며 곧 AlphaProof에 대한 더 많은 기술적 세부 정보를 공개할 계획입니다.

우리는 수학자들이 AI 도구를 사용하여 가설을 탐구하고, 오랜 문제를 해결하기 위해 과감하고 새로운 접근 방식을 시도하고, 시간이 많이 걸리는 증명 요소를 신속하게 완료할 미래를 기대하고 있습니다. Gemini와 같은 AI 시스템은 다음과 같은 분야에서 큰 변화를 가져올 것입니다. 수학 등 광범위한 추론 측면이 더욱 강력해집니다.

연구팀

구글은 새로운 연구가 국제 수학 올림피아드(International Mathematical Olympiad)의 지원을 받았다고 밝혔습니다.

AlphaProof 개발은 Thomas Hubert, Rishi Mehta 및 Laurent Sartran이 주도했으며 주요 기여자로는 Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser가 있습니다. Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland 및 Grace Margand.

그중 아자 황(Aja Huang), 줄리안 슈리트위저(Julian Schrittwieser), 야닉 슈뢰커(Yannick Schroecker) 등도 8년 전(2016년) 알파고 논문의 핵심 멤버였다. 8년 전, 강화학습을 기반으로 만든 알파고가 유명해졌습니다. 8년 후 강화 학습은 AlphaProof에서 다시 빛을 발합니다. 누군가 친구들 사이에서 다음과 같이 한탄했습니다. RL이 돌아왔습니다!

AlphaGeometry 2 및 자연어 추론 작업은 Thang Luong이 주도합니다. AlphaGeometry 2의 개발은 Trieu Trinh과 Yuri Chervonyi가 주도했으며 Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang 및 Marcelo Menegali의 중요한 공헌이 있었습니다.

또한 David Silver, Quoc Le, Hassabis 및 Pushmeet Kohli는 전체 프로젝트 조정 및 관리를 담당합니다.

참고 내용:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/