소식

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

새로운 지혜 보고서

편집자: 편집부

[새로운 지혜 소개] 방금 Google DeepMind의 최신 수학적 모델이 IMO 수학 올림피아드 은메달을 획득했습니다! 6개 문제 중 4개 문제를 만점으로 풀었을 뿐만 아니라 금메달과 단 1점 차이가 났을 뿐만 아니라, 4번째 문제를 해결하는 데 19초밖에 걸리지 않았으며 문제 해결의 질과 속도는 득점한 인간 심사위원들을 놀라게 했습니다. .

AI가 IMO 수학 올림피아드 은메달을 획득했습니다!

방금 구글 딥마인드는 올해 국제 수학 올림피아드의 실제 문제가 자체 AI 시스템으로 제작되었다고 발표했습니다.

이 중 AI는 6개 문제 중 4개 문제를 성공적으로 풀었을 뿐만 아니라, 각 문제에서 만점을 받아 은메달 최고 점수인 28점에 해당한다.

이번 결과는 금메달과 단 1점 차이가 납니다!

609명의 참가자 중 금메달은 58명만 획득

공식 대회에서 인간 참가자는 두 세션에 걸쳐 답변을 제출하게 되며, 시간 제한은 매번 4.5시간입니다.

흥미롭게도 질문 중 하나에 AI가 답변하는 데는 몇 분 밖에 걸리지 않았지만 나머지 질문에는 꼬박 3일이 걸렸는데, 이는 심각한 타임아웃이라고 할 수 있습니다.

이번에 큰 공헌을 한 것은 두 가지 AI 시스템인 AlphaProof와 AlphaGeometry 2였습니다.

중요한 점: 2024 IMO는 이 두 AI의 훈련 데이터에 없습니다.

AI 엔지니어 데빈(IOI 3회 금메달리스트)의 창립자 중 한 명인 스캇 우(Scott Wu)는 “어렸을 때는 올림픽이 불과 10년 뒤에 AI로 대체될 것이라고는 전혀 생각하지 못했습니다. . 해결되었습니다."

올해 IMO 대회에는 대수학, 조합론, 기하학, 정수론을 포함한 6가지 경쟁 문제가 출품됩니다. 6개의 길은 4개가 되고, AI의 레벨을 느껴보자──

AI의 수학적 추론 능력에 교수도 충격

이전 AI는 추론 능력과 훈련 데이터의 한계로 인해 수학적 문제를 해결하는 데 한계가 있었다는 사실은 모두가 알고 있습니다.

오늘 함께 등장한 두 AI 플레이어는 이러한 한계를 깨뜨렸습니다. 그들은 각각--

- 강화 학습을 기반으로 한 공식적인 수학적 추론을 위한 새로운 시스템인 AlphaProof

- 2세대 기하학 문제 해결 시스템인 AlphaGeometry 2

두 AI의 답변은 유명한 수학자 Timothy Gowers 교수(IMO 금메달리스트 및 필즈 메달리스트)와 Joseph Myers 박사(2회 IMO 금메달리스트이자 IMO 2024 질문 선택 위원회 회장)의 규칙에 따라 채점되었습니다. .

결국 AlphaProof는 두 개의 대수학 문제와 하나의 정수론 문제를 올바르게 풀었습니다. 올해 IMO에서는 단 5명의 인간 참가자만이 기하학 문제를 풀었습니다.

아직 정복되지 않은 조합 수학 문제는 두 가지뿐입니다.

Timothy Gowers 교수도 채점 과정에서 큰 충격을 받았습니다.

프로그램이 그렇게 명확하지 않은 해결책을 제시할 수 있다는 것은 정말 인상적이며 현재의 기술 수준을 고려할 때 제가 기대했던 것보다 훨씬 뛰어납니다.

알파프루프

AlphaProof는 공식 언어 Lean으로 수학적 명제를 증명할 수 있는 시스템입니다.

사전 훈련된 대규모 언어 모델과 체스, 장기, 바둑을 스스로 익히는 AlphaZero 강화 학습 알고리즘을 결합합니다.

형식 언어의 주요 장점은 수학적 추론과 관련된 증명에 대해 형식적으로 검증할 수 있다는 것입니다. 그러나 인간이 작성하는 관련 데이터의 양이 매우 제한되어 있어 기계 학습에서의 적용은 제한적이었습니다.

대조적으로, 자연어 기반 접근 방식은 대량의 데이터에 액세스할 수 있음에도 불구하고 그럴듯하지만 잘못된 중간 추론 단계와 솔루션을 생성할 수 있습니다.

이를 극복하기 위해 Google DeepMind 연구자들은 자연어 문제 진술을 자동으로 형식문으로 변환하도록 Gemini 모델을 미세 조정하고, 다양한 난이도의 형식 문제가 포함된 대규모 라이브러리를 구축하여 두 보완 분야 사이에 다리를 구축했습니다.

문제를 해결할 때 AlphaProof는 후보 솔루션을 생성하고 Lean에서 가능한 증명 단계를 검색하여 이를 증명하거나 반증합니다.

발견되고 검증된 각각의 증명은 AlphaProof의 언어 모델을 강화하여 향후 더 어려운 문제를 해결할 수 있도록 하는 데 사용됩니다.

AlphaProof를 교육하기 위해 연구원들은 대회가 시작되기 몇 주 전부터 대회가 진행되는 동안 다양한 난이도와 수학적 주제 영역을 다루는 수백만 개의 질문을 입증하거나 반증했습니다.

대회 기간 동안 그들은 완전한 해결책을 찾을 때까지 대회 문제의 자체 생성 변형에 대한 증명을 강화하여 훈련 루프를 적용했습니다.

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

알파지오메트리 2

AlphaGeometry의 업그레이드 버전인 AlphaGeometry 2는 Gemini의 언어 모델을 기반으로 처음부터 훈련된 신경 기호 하이브리드 시스템입니다.

이전 세대보다 훨씬 더 많은 합성 데이터를 기반으로 물체의 움직임, 각도, 비율, 거리 등과 관련된 방정식을 포함하여 더욱 어려운 기하학적 문제를 해결할 수 있습니다.

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

올해 IMO에 참여하기 전에 AlphaGeometry 2는 이미 많은 성공을 거두었습니다. 지난 25년 동안 IMO 기하학 문제의 83%를 해결할 수 있었던 반면, 1세대는 53%만 해결할 수 있었습니다.

이번 IMO에서는 AlphaGeometry 2의 속도가 모든 사람을 놀라게 했습니다. 공식 질문을 받은 후 19초 이내에 질문 4를 해결했습니다!

질문 4에서는 ∠KIL과 ∠XPY의 합이 180°라는 증명이 필요합니다. AlphaGeometry 2에서는 ∠AEB=90°가 되도록 BI 선에 점 E를 구성할 것을 권장합니다.점 E는 AB의 중간점 L을 결정하는 데 도움이 되며 ABE ~ YBI 및 ALE ~ IPC와 같은 유사한 삼각형 쌍을 많이 형성하여 결론을 증명합니다.

AI 문제 해결 프로세스

이러한 질문은 AI에 제출되기 전에 먼저 공식적인 수학 언어로 수동으로 번역된다는 점을 언급할 가치가 있습니다.
피1

일반적으로 각 IMO 테스트의 첫 번째 질문(P1)은 비교적 쉽습니다.

네티즌들은 "P1에는 고등학교 수학 지식만 있으면 되는데 인간 플레이어들은 보통 60분 안에 끝낸다"고 말했다.

IMO 2024의 첫 번째 질문은 주로 실수 α의 특성을 조사하며 특정 조건을 만족하는 실수 α를 찾는 것이 필요합니다.

AI가 정답을 제시했습니다. α는 짝수입니다. 그렇다면 정확히 어떻게 대답됩니까?

문제 해결의 첫 번째 단계에서 AI는 먼저 왼쪽 세트와 오른쪽 세트가 동일하다는 정리를 제시했습니다.

왼쪽의 집합은 임의의 양의 정수 n에 대해 조건을 충족하는 모든 실수 α가 ⌊i*α⌋를 1에서 n으로 나눌 수 있음을 나타냅니다. 오른쪽의 집합은 정수 k가 있음을 나타냅니다. 짝수이고 실수 α는 k와 같습니다.

다음 증명은 두 방향으로 나누어진다.

먼저 오른쪽 집합이 왼쪽 집합의 부분집합(간단한 방향)임을 증명하세요.

그런 다음 왼쪽 집합이 오른쪽 집합(어려운 방향)의 부분 집합임을 증명합니다.

코드가 끝날 때까지 AI는 α가 반드시 우수.

마지막으로 DeepMind는 문제 해결 과정에서 AI가 의존하는 세 가지 원칙인 propext, Classical.choice 및 Quot.sound를 요약했습니다.

다음은 P1의 전체 문제 해결 과정입니다: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

두 번째 질문은 최대 공약수 속성과 관련된 양의 정수 쌍(a, b) 간의 관계를 조사합니다.

AI가 해결한 답은 다음과 같습니다.

정리는 특정 조건을 만족하는 양의 정수 쌍(a, b)에 대해 그 집합은 (1,1)만 포함할 수 있다는 것입니다.

다음 문제 해결 과정에서 AI가 채택한 증명 전략은 (1,1)이 주어진 조건을 만족한다는 것을 먼저 증명한 후 이것이 유일한 해결책임을 증명하는 것입니다.

g=2, N=3을 사용하여 (1,1)이 최종 해임을 증명하십시오.

(a,b)가 해라면 ab+1은 g를 나누어야 함을 보여주세요.

이 과정에서 AI는 오일러의 정리와 모듈러 연산의 속성을 추론에 활용했습니다.

마지막으로, a=b=1이 유일한 해법임을 증명하세요.

다음은 P2의 전체 문제 해결 과정입니다: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

P4는 특정 기하학적 각도 관계를 증명해야 하는 기하학적 증명 문제입니다.

위에서 언급했듯이 이는 AlphaGeometry 2에 의해 19초 만에 완료되어 새로운 기록을 세웠습니다.

제공된 솔루션에 따라 1세대 AlphaGeometry와 마찬가지로 모든 솔루션의 보조 포인트가 언어 모델에 의해 자동으로 생성됩니다.

증명에서 모든 각도 추적은 가우스 제거를 사용하며 d(AB)−d(CD)는 AB에서 CD로의 방향 각도(모듈로 π)와 같습니다.

문제 해결 과정에서 AI는 유사한 삼각형과 합동 삼각형의 쌍(빨간색으로 표시)을 수동으로 표시합니다.

다음으로 "재모순법"을 이용하여 완성된 AlphaGeometry의 문제를 해결하는 단계가 있다.

먼저 Lean을 사용하여 증명해야 하는 명제를 공식화하고 기하학적 구성을 시각화합니다.

증명의 주요 단계는 다음과 같습니다.

전체 문제 해결 프로세스는 아래 그림을 참조하세요. https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

여섯 번째 IMO 질문은 함수의 속성을 탐구하고 유리수에 대한 구체적인 결론을 증명해야 하는 "궁극적 보스"입니다.

AI는 c=2로 해결합니다.

먼저 "수족관 함수"의 속성을 정의하고 이러한 모든 함수에 대해 f(r)+f(-r) 값 집합에는 최대 2개의 요소가 있다고 선언하는 정리문을 살펴보겠습니다.

증명 전략은 먼저 모든 Aquaesulian 함수에 대해 f(r)+f(-r) 값 세트에 최대 2개의 요소가 있음을 증명하는 것입니다. 그런 다음 f(r)+f(-r)이 정확히 2개의 서로 다른 값을 갖도록 특정 Aquaesulian 함수를 구성합니다.

f(0)=0일 때, f(x)+f(-x)는 최대 두 개의 다른 값을 취하고, 아쿠아에술리안 함수 f(0)≠0이 없음을 증명하십시오.

함수 f(x)=-x+2⌈x⌉를 구성하고 이것이 Aquaesulian 함수임을 증명하십시오.

마지막으로, 이 함수의 경우 f(-1)+f(1) =0과 f(1/2)+f(-1/2)=2가 두 개의 다른 값임을 증명하십시오.

다음은 전체 문제 해결 프로세스입니다. https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

올림피아드 수학 문제를 풀 수 있지만 9.11과 9.9 중 어느 것이 더 큰지 알 수 있나요?

스탠포드 대학과 Sequoia의 연구원인 Andrew Gao는 이 AI 혁신의 중요성을 확인했습니다.

중요한 점은 최신 IMO 시험 문제가 훈련 세트에 포함되어 있지 않다는 것입니다. 이는 AI가 보이지 않는 새로운 문제를 처리할 수 있음을 보여주기 때문에 중요합니다.

더욱이 AI가 성공적으로 해결한 기하학적 문제는 관련 공간의 특성(직관적 사고와 공간적 상상력 필요)으로 인해 항상 매우 어려운 것으로 간주되어 왔습니다.

Nvidia의 수석 과학자 Jim Fan이 대형 모델은 신비한 존재라는 장문의 글을 올렸습니다.

그들은 수학 올림피아드에서 은메달을 따기도 하고, "9.11과 9.9 중 어느 숫자가 더 크나요?"와 같은 질문에서 자주 실수를 합니다.

Gemini 뿐만 아니라 GPT-4o, Claude-3.5, Llama-3도 100% 정답을 맞힐 수는 없습니다.

AI 모델을 훈련함으로써 우리는 우리의 지능을 넘어서는 광범위한 영역을 탐색하고 있습니다.그 과정에서 우리는 매우 이상한 지역을 발견했습니다. 지구와 비슷하지만 이상한 계곡으로 가득 찬 외계 행성입니다.

이는 불합리해 보이지만 훈련 데이터 분포를 사용하여 설명할 수 있습니다.

AlphaProof 및 AlphaGeometry 2는 형식 증명 및 도메인별 기호 엔진에 대해 교육되었습니다. 범용 LLM을 기반으로 구축되었음에도 불구하고 전문적인 올림피아드 문제를 어느 정도 더 잘 해결합니다. GPT-4o의 훈련 세트에는 수학 데이터를 훨씬 초과할 수 있는 대량의 GitHub 코드 데이터가 혼합되어 있습니다. 소프트웨어 버전 중 "v9.11 > v9.9"는 데이터 분포를 심각하게 왜곡시킬 수 있습니다. 그러므로 이 오류는 어느 정도 이해가 됩니다.

Google 개발자 책임자는 어려운 수학적, 물리적 문제를 해결할 수 있는 모델이 AGI의 핵심 경로라고 말했고, 오늘 우리는 이 경로에서 한 단계 더 나아갔습니다.

다른 네티즌들은 이번 주에는 정보가 너무 많다고 말했다.

참고자료:

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

https://x.com/DrJimFan/status/1816521330298356181