뉴스/정보
AI, 국제수학올림피아드 문제 풀며 은메달 수준 달성
작성자
작성일
2024-07-26 00:36
조회
833
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
획기적인 모델인 AlphaProof와 AlphaGeometry 2는 수학의 고급 추론 문제를 해결합니다.
고급 수학적 추론 기능을 갖춘 인공 일반 지능(AGI)은 과학과 기술의 새로운 영역을 열어줄 수 있는 잠재력을 가지고 있습니다.
우리는 수학자들이 새로운 통찰력 , 새로운 알고리즘 및 미해결 문제 에 대한 답을 발견하도록 돕는 AI 시스템을 구축하는 데 큰 진전을 이루었습니다 . 하지만 현재의 AI 시스템은 추론 기술과 훈련 데이터의 한계로 인해 여전히 일반적인 수학 문제를 해결하는 데 어려움을 겪고 있습니다.
오늘 우리는 공식적 수학 추론을 위한 새로운 강화 학습 기반 시스템인 AlphaProof와 우리의 기하 풀이 시스템 의 개선된 버전인 AlphaGeometry 2를 소개합니다 . 이 시스템들은 함께 올해의 국제 수학 올림피아드 (IMO)에서 6개 문제 중 4개를 풀었고, 처음으로 이 대회에서 은메달리스트와 동일한 수준을 달성했습니다.
복잡한 수학 문제를 해결하는 획기적인 AI 성능
IMO는 1959년부터 매년 개최되어 온 젊은 수학자들을 위한 가장 오래되고 규모가 크고 권위 있는 대회입니다.
매년 엘리트 대학 예비 수학자들은 대수학, 조합론, 기하학 및 수론에서 6가지 매우 어려운 문제를 풀기 위해 수천 시간 동안 훈련을 받습니다. 수학자에게 가장 큰 영예 중 하나인 필즈 메달 수상자 중 다수 는 IMO에서 자국을 대표했습니다.
최근 들어 매년 열리는 IMO 대회도 머신 러닝 분야의 위대한 도전이자 AI 시스템의 고급 수학적 추론 능력을 측정하는 야심찬 벤치마크로 널리 인식되고 있습니다.
올해, 우리는 IMO 주최측에서 제공한 경쟁 문제에 통합 AI 시스템을 적용했습니다. 저희 솔루션은 IMO의 포인트 수여 규칙에 따라 IMO 금메달리스트이자 필즈 메달 수상자 티모시 고워스 교수 와 IMO 금메달 2회 수상자이자 IMO 2024 문제 선정 위원회 위원장 인 조셉 마이어스 박사가 평가 했습니다.
첫째, 문제는 우리 시스템이 이해할 수 있도록 수동으로 공식 수학 언어로 번역되었습니다. 공식 대회에서 학생들은 각각 4.5시간씩 두 세션에 걸쳐 답을 제출했습니다. 우리 시스템은 한 문제를 몇 분 안에 풀었고 다른 문제를 푸는 데 최대 3일이 걸렸습니다.
AlphaProof는 답을 결정하고 그것이 옳다는 것을 증명함으로써 두 개의 대수 문제와 한 개의 수론 문제를 풀었습니다. 여기에는 올해 IMO에서 단 5명의 참가자만이 푼 대회에서 가장 어려운 문제가 포함되었습니다. AlphaGeometry 2는 기하학 문제를 증명했지만 두 개의 조합 문제는 미해결 상태로 남았습니다.
우리 시스템의 IMO 2024 솔루션을 확인하세요
6가지 문제 각각은 7점을 얻을 수 있으며, 총 최대 42점입니다. 저희 시스템은 최종 점수 28점을 달성하여, 해결한 각 문제에서 완벽한 점수를 받았습니다. 이는 은메달 부문 의 최고 점수와 동일합니다 . 올해 금메달 기준은 29점에서 시작하며, 공식 대회에서 609명의 참가자 중 58명이 달성했습니다.
...
AlphaProof: 추론에 대한 공식적 접근 방식
AlphaProof는 공식 언어 Lean 에서 수학적 진술을 증명하도록 스스로를 훈련시키는 시스템입니다 . 사전 훈련된 언어 모델을 AlphaZero 강화 학습 알고리즘과 결합합니다. 이 알고리즘은 이전에 체스, 쇼기, 바둑 게임을 마스터하는 방법을 스스로 학습했습니다.
공식 언어는 수학적 추론을 포함하는 증명이 정확성을 위해 공식적으로 검증될 수 있다는 중요한 이점을 제공합니다. 그러나 기계 학습에서의 사용은 이전에는 인간이 작성한 데이터의 양이 매우 제한적이어서 제약을 받았습니다.
대조적으로 자연어 기반 접근법은 수십 배 더 많은 데이터에 액세스할 수 있음에도 불구하고 그럴듯하지만 잘못된 중간 추론 단계와 솔루션을 환각할 수 있습니다. 우리는 Gemini 모델을 미세 조정하여 자연어 문제 진술을 자동으로 공식 진술로 변환하고 다양한 난이도의 공식 문제 라이브러리를 생성하여 이 두 보완적인 영역 사이에 다리를 놓았습니다.
문제가 제시되면 AlphaProof는 솔루션 후보를 생성한 다음 Lean에서 가능한 증명 단계를 검색하여 이를 증명하거나 반증합니다. 발견되고 검증된 각 증명은 AlphaProof의 언어 모델을 강화하는 데 사용되어 후속의 더 어려운 문제를 해결하는 능력을 향상시킵니다.
우리는 대회에 앞서 몇 주 동안 광범위한 어려움과 수학적 주제 영역을 포괄하여 수백만 개의 문제를 증명하거나 반증함으로써 IMO를 위해 AlphaProof를 훈련했습니다. 훈련 루프는 대회 중에도 적용되어 전체 솔루션을 찾을 때까지 대회 문제의 자체 생성 변형에 대한 증명을 강화했습니다.
획기적인 모델인 AlphaProof와 AlphaGeometry 2는 수학의 고급 추론 문제를 해결합니다.
고급 수학적 추론 기능을 갖춘 인공 일반 지능(AGI)은 과학과 기술의 새로운 영역을 열어줄 수 있는 잠재력을 가지고 있습니다.
우리는 수학자들이 새로운 통찰력 , 새로운 알고리즘 및 미해결 문제 에 대한 답을 발견하도록 돕는 AI 시스템을 구축하는 데 큰 진전을 이루었습니다 . 하지만 현재의 AI 시스템은 추론 기술과 훈련 데이터의 한계로 인해 여전히 일반적인 수학 문제를 해결하는 데 어려움을 겪고 있습니다.
오늘 우리는 공식적 수학 추론을 위한 새로운 강화 학습 기반 시스템인 AlphaProof와 우리의 기하 풀이 시스템 의 개선된 버전인 AlphaGeometry 2를 소개합니다 . 이 시스템들은 함께 올해의 국제 수학 올림피아드 (IMO)에서 6개 문제 중 4개를 풀었고, 처음으로 이 대회에서 은메달리스트와 동일한 수준을 달성했습니다.
복잡한 수학 문제를 해결하는 획기적인 AI 성능
IMO는 1959년부터 매년 개최되어 온 젊은 수학자들을 위한 가장 오래되고 규모가 크고 권위 있는 대회입니다.
매년 엘리트 대학 예비 수학자들은 대수학, 조합론, 기하학 및 수론에서 6가지 매우 어려운 문제를 풀기 위해 수천 시간 동안 훈련을 받습니다. 수학자에게 가장 큰 영예 중 하나인 필즈 메달 수상자 중 다수 는 IMO에서 자국을 대표했습니다.
최근 들어 매년 열리는 IMO 대회도 머신 러닝 분야의 위대한 도전이자 AI 시스템의 고급 수학적 추론 능력을 측정하는 야심찬 벤치마크로 널리 인식되고 있습니다.
올해, 우리는 IMO 주최측에서 제공한 경쟁 문제에 통합 AI 시스템을 적용했습니다. 저희 솔루션은 IMO의 포인트 수여 규칙에 따라 IMO 금메달리스트이자 필즈 메달 수상자 티모시 고워스 교수 와 IMO 금메달 2회 수상자이자 IMO 2024 문제 선정 위원회 위원장 인 조셉 마이어스 박사가 평가 했습니다.
첫째, 문제는 우리 시스템이 이해할 수 있도록 수동으로 공식 수학 언어로 번역되었습니다. 공식 대회에서 학생들은 각각 4.5시간씩 두 세션에 걸쳐 답을 제출했습니다. 우리 시스템은 한 문제를 몇 분 안에 풀었고 다른 문제를 푸는 데 최대 3일이 걸렸습니다.
AlphaProof는 답을 결정하고 그것이 옳다는 것을 증명함으로써 두 개의 대수 문제와 한 개의 수론 문제를 풀었습니다. 여기에는 올해 IMO에서 단 5명의 참가자만이 푼 대회에서 가장 어려운 문제가 포함되었습니다. AlphaGeometry 2는 기하학 문제를 증명했지만 두 개의 조합 문제는 미해결 상태로 남았습니다.
우리 시스템의 IMO 2024 솔루션을 확인하세요
6가지 문제 각각은 7점을 얻을 수 있으며, 총 최대 42점입니다. 저희 시스템은 최종 점수 28점을 달성하여, 해결한 각 문제에서 완벽한 점수를 받았습니다. 이는 은메달 부문 의 최고 점수와 동일합니다 . 올해 금메달 기준은 29점에서 시작하며, 공식 대회에서 609명의 참가자 중 58명이 달성했습니다.
...
AlphaProof: 추론에 대한 공식적 접근 방식
AlphaProof는 공식 언어 Lean 에서 수학적 진술을 증명하도록 스스로를 훈련시키는 시스템입니다 . 사전 훈련된 언어 모델을 AlphaZero 강화 학습 알고리즘과 결합합니다. 이 알고리즘은 이전에 체스, 쇼기, 바둑 게임을 마스터하는 방법을 스스로 학습했습니다.
공식 언어는 수학적 추론을 포함하는 증명이 정확성을 위해 공식적으로 검증될 수 있다는 중요한 이점을 제공합니다. 그러나 기계 학습에서의 사용은 이전에는 인간이 작성한 데이터의 양이 매우 제한적이어서 제약을 받았습니다.
대조적으로 자연어 기반 접근법은 수십 배 더 많은 데이터에 액세스할 수 있음에도 불구하고 그럴듯하지만 잘못된 중간 추론 단계와 솔루션을 환각할 수 있습니다. 우리는 Gemini 모델을 미세 조정하여 자연어 문제 진술을 자동으로 공식 진술로 변환하고 다양한 난이도의 공식 문제 라이브러리를 생성하여 이 두 보완적인 영역 사이에 다리를 놓았습니다.
문제가 제시되면 AlphaProof는 솔루션 후보를 생성한 다음 Lean에서 가능한 증명 단계를 검색하여 이를 증명하거나 반증합니다. 발견되고 검증된 각 증명은 AlphaProof의 언어 모델을 강화하는 데 사용되어 후속의 더 어려운 문제를 해결하는 능력을 향상시킵니다.
우리는 대회에 앞서 몇 주 동안 광범위한 어려움과 수학적 주제 영역을 포괄하여 수백만 개의 문제를 증명하거나 반증함으로써 IMO를 위해 AlphaProof를 훈련했습니다. 훈련 루프는 대회 중에도 적용되어 전체 솔루션을 찾을 때까지 대회 문제의 자체 생성 변형에 대한 증명을 강화했습니다.
전체 0