AI가 수학적 연구를 전복시킨다! 필즈상 수상자이자 중국계 미국인 수학자, Terence Tao가 좋아하는 11개 논문 발표 |

AI는 실제로 수학을 변화시키고 있습니다.

최근 이 문제에 주목하고 있는 테렌스 타오(Terence Tao)가 "미국수학회지" 최신호를 전달했습니다.

"기계가 수학을 바꿀 것인가?"라는 주제를 중심으로 많은 수학자들이 자신의 의견을 표현했습니다. 전체 과정은 열정적이고 흥미진진했습니다.

저자는 필즈상 수상자 Akshay Venkatesh, 중국 수학자 Lejun Zheng, 뉴욕대학교 컴퓨터 과학자 Ernest Davis 및 기타 업계의 유명 학자들을 포함하여 강력한 라인업을 보유하고 있습니다.

AI의 세계는 엄청난 변화를 겪었습니다. 아시다시피, 이 기사 중 상당수는 1년 전에 제출되었으며, 올해 안에 AI는 많은 중요한 변화를 겪었습니다.

그러나 그럼에도 불구하고 이러한 기사는 여전히 금빛으로 가득 차 있으며 심지어 Terence Tao는 이렇게 외치게 만들었습니다. 이 분야는 너무 빠르게 움직이고 있습니다! 게시되지 않은 기사가 중복된 것처럼 보이게 만듭니다.

AI 도구가 수학 분야를 놀라운 속도로 발전시키고 있다는 사실을 누구도 부인할 수 없습니다.

인공지능은 순수 수학을 포함한 과학 분야에서 정보를 수집하고 처리하는 방식에 혁명을 가져올까요? 수학이 이루어지는 방식이 바뀔까요?

수학자들은 의견이 분분합니다. 어떤 사람들은 연구에서 기계 학습의 광범위한 사용이 코앞에 다가왔다고 믿는 반면, 다른 사람들은 회의적이어서 지나친 낙관주의와 그에 따른 "AI 겨울"을 회상합니다.

그러나 수학 연구의 실천에는 급격한 변화가 일어날 가능성이 매우 높습니다. 이제 수학자들이 이러한 변화가 제기하는 문제를 고려해야 할 때입니다.

분명히 폭풍이 다가오고 있습니다.

그럼 기계가 수학을 바꿀까요?

수학적 자동화가 수학적 연구에 미치는 영향

이 논문에서 필즈상 수상자 Akshay Venkatesh는 자동화가 수학적 연구에 미치는 영향을 탐구합니다.

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01834-5/S0273-0979-2024-01834-5. pdf

이 논문에서 Akshay Venkatesh는 흥미로운 사고 실험을 제안했습니다.

2017년 DeepMind의 Alphazero는 체스와 바둑을 스스로 가르쳐 인간을 능가했습니다.

10년 후 "알레프제로"(작성)도 동일한 형식의 수학을 수행했다면 어떨까요?

이 기사에서 "수학"은 "순수한 수학 연구"를 의미합니다.

우리의 출발점은 "Alephzero"가 독학으로 고등학교 및 대학교 수학을 가르쳤고 SpringerVerlag 대학원 Terts in Mathematics 시리즈의 모든 연습을 완료했다고 가정하는 것입니다. 다음날 아침 수학자들이 그것을 내놓았고, 아이들은 그것을 다운로드하여 우리의 컴퓨팅 자원으로 실행했습니다.

이것은 명백히 비현실적이기 때문에 실제로 사고 실험입니다. 우리의 시야를 향후 10년 또는 20년으로 제한함으로써 우리는 그러한 기술 발전에 수반될 수 있는 사회적 변화에서 벗어날 수 있습니다. 더 극단적인 유형의 기계 지능에 대해 생각하는 것을 피하기 위해 우리는 Alephzero를 살아있는 협력자가 아닌 전동 공구로 모델링합니다.

우리는 이렇게 스스로를 위로할 수 있습니다. 사실 이 전제는 우리와 너무 거리가 멀기 때문에 고려할 필요가 없습니다. 하지만 조금이라도 기회를 준다면 20년 안에 이런 일이 일어날 수도 있습니다.

수학자와 문제 네트워크 간의 베이지안 상호 작용을 통해 가치 메커니즘의 일부를 보여주는 매우 대략적인 모델을 제공합니다. 이제 우리는 “Alephzero”가 이 네트워크에 어떤 영향을 미치고 결과를 바꿀지 고려합니다.

보시다시피 인지된 어려움은 가치를 구축하는 방법에 있어 중요한 부분입니다.

특정 상황에 관계없이 "알레프제로"는 우리의 문제 해결 능력을 변화시켜 문제의 어려움에 대한 인식을 변화시킬 것입니다.

가장 빠르게 가속화될 수 있는 수학적 과정의 부분은 인식된 난이도가 가장 크게 감소하며 위의 모델에 따르면 상태가 가장 크게 감소합니다. 많은 자동화 사례에서 유사한 패턴이 발생합니다.

마지막으로 "Alephzero"는 수학의 흥미로운 문제 전체 범위를 크게 확장할 것입니다. 이는 전문 수학자와 다른 모든 사람 사이의 공평한 경쟁의 장을 마련할 것입니다.

기계가 수학을 더욱 집약적으로 만드는 방법

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01827-8 / S0273-0979-2024-01827-8.pdf

수학자 Zheng Lejun은 기술이 우리가 수학을 공부하는 방식을 변화시켰기 때문에 이 기술을 사용하여 수학을 더욱 "집합"할 수 있다고 믿습니다. 기술 발전에 직면하여 인간 수학자들을 불필요하게 만드는 것이 아닙니다.

"수학을 한다"는 것이 무엇을 의미하는지 생각하면서 그녀는 가르치고 배우기, 질문하기, 협력, 의사소통, 연구 수행 행위 등 수학 기술의 측면을 조사했습니다.

엄밀한 분석이 아니라 수학자로서의 경험을 바탕으로 한 현명한 반성입니다.

Lejun Zheng은 일부 컴퓨터 지원 증명 검사기와 증명 생성기가 있지만 기술이 아직까지 수학 연구의 가장 심오하고 창의적이며 인간적인 측면을 진정으로 침해하지 않았다고 믿습니다.

깊고 창의적인 부분은 먼저 정의에 대한 아이디어, 증명에 대한 아이디어, 수학의 여러 부분을 연결하기 위한 아이디어, 사물을 표현하는 새로운 방법에 대한 아이디어, 기호 및 용어에 대한 아이디어, 그래픽 추론 아이디어 등 아이디어를 떠올리는 것입니다. 시각적 표현을 위한 아이디어도 포함됩니다.

기계가 수학적 연구를 하기 위해서는 기계에게 하라고 지시할 수 있는 방법을 찾아야 하는데, 우리가 스스로 방법을 모르면 기계에게 어떻게 하는지 알려주기가 어렵습니다.

기계는 특정 수준의 증명 확인을 수행할 수 있지만 비밀리에 수학자들은 우리가 완전히 엄격한 증명을 작성할 수 없다는 것을 알고 있습니다. 우리는 논리를 기반으로 주장을 하고 동료들이 그럴 것이라고 생각하는 논리적 단계를 따릅니다. 채울 수 있습니다. 지원합니다.

이 단계의 크기를 정의하지 않기 때문에 기계에 지시하기가 어렵습니다.

증명을 생성하는 것은 모든 수학 학생이 알고 있듯이 단순히 확인하는 것과는 완전히 다른 기술입니다. 스스로 새로운 증거를 생각해내는 것보다 다른 사람의 증거를 따르는 것이 훨씬 쉽습니다. 이는 컴퓨터가 수학적 연구 능력에서 결코 인간 수학자들을 능가할 수 없다는 말은 아닙니다.

그녀의 의견으로는 컴퓨터가 인간 수학자보다 더 강력한 이유는-

컴퓨터는 현재 알려진 가능한 모든 논리적 결과를 검색하여 가능한 모든 작업을 검색하는 더 뛰어난 능력을 갖고 있으며 새로운 수학을 생각해내려고 노력할 수 있다는 것입니다. .

이 작업에는 상상력, 추측, 직관의 도약이 필요합니다. 컴퓨터가 이를 수행하려면 무엇이 충분할까요? 아이디어는 매우 흥미롭습니다.

컴퓨터가 논리적 추론을 도와줄 수 있을까요

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01833-3/S0273-0979-2024-01833-3.pdf

컴퓨터는 수학적 연구를 수행하는 방식에 혁명을 일으켜 복잡한 계산을 쉽게 만들어줍니다.

그럼 다음에는 논리적 추론의 보조자가 될까요? 언젠가 그들은 독립적으로 추론할 수 있을까요?

이 기사에서는 신경망, 컴퓨터 정리 증명자 및 대규모 언어 모델 분야의 최근 중요한 발전에 대한 개요를 제공합니다.

공식 도구가 더 나은 수학적 연구를 수행하는 데 어떻게 도움이 되는지

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979- 2024-01832-1/S0273-0979-2024-01832-1.pdf

20세기 초부터 우리는 수학적 정의와 증명이 엄격한 구문과 형식 시스템을 통해 달성될 수 있다는 것을 이해했습니다. 규칙이 표현됩니다.

이를 바탕으로 컴퓨터 증명 보조 장치의 개발을 통해 수학적 지식을 디지털 형식으로 인코딩할 수 있습니다.

이 기사에서는 이러한 유형의 기술과 관련 도구가 더 나은 수학적 연구를 수행하는 데 어떻게 도움이 될 수 있는지 살펴보겠습니다.

정리 증명자를 사용하여 수학 연구의 복잡한 문제를 단순화

논문 주소: https://www.ams.org/journals/bull/2024-61-02/ S0273- 0979-2024-01831-X/S0273-0979-2024-01831-X.pdf

이 기사에서는 추상 경계를 설정하여 수학 연구의 복잡한 문제를 단순화하기 위해 대화형 정리 증명자를 어떻게 사용할 수 있는지 살펴봅니다.

이상하고 새로운 우주: LLM을 통해 수학자들은 보다 자연스러운 언어로 증명 보조원과 소통할 수 있습니다.

논문 주소: https://www.ams.org/journals/bull/2024-61 - 02/S0273-0979-2024-01830-8/S0273-0979-2024-01830-8.pdf

현재 컴퓨터 프로그램(증명 보조자라고도 함)은 수학적 증명의 정확성을 확인할 수 있으며, 그러나 그들이 사용하는 특수한 증명 언어는 많은 수학자에게 장벽이 됩니다.

대형 언어 모델(LLM)은 이러한 장벽을 무너뜨릴 수 있는 잠재력을 가지고 있어 수학자들이 보다 자연스러운 언어로 증명 보조자와 통신할 수 있도록 해줍니다. 이는 직관력을 발전시킬 뿐만 아니라 추론이 정확하다는 것을 보장해 줍니다.

딥 러닝 도구를 사용하여 순수 수학 연구 수행

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024 - 01829-1/S0273-0979-2024-01829-1.pdf

이 글은 순수 수학자가 연구에 딥러닝 도구를 사용하려고 할 때 기대할 수 있는 것에 대한 개인적인 경험과 비공식적인 공유에 관한 것입니다.

AI도 수학적 연구를 할 수 있나요

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01828-X/S0273-0979-2024-01828-X.pdf

이 글에서는 기초 수학과 상식 추론을 결합한 단어 문제 해결에 있어 현재 AI 기술의 역량과 한계를 살펴봅니다.

저자는 AI 자연어 기술을 활용하여 개발된 세 가지 방법인 직접 답변 제공, 문제를 해결하는 컴퓨터 프로그램 생성, 자동화된 정리 테스터에서 사용할 수 있는 형식적 표현 생성을 검토합니다.

저자는 순수 수학 연구를 위한 AI 기술 개발에서 이러한 한계의 중요성은 아직 결정되지 않았지만 수학 응용에서는 매우 중요하며 작성된 수학적 내용을 이해할 수 있는 프로그램 개발에도 중요하다고 믿습니다. 인간에 의해.

기계시대에 증거란 무엇인가

논문주소 : https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01826- 6 /S0273-0979-2024-01826-6.pdf

이 기사에서 저자는 전통적인 검증과 컴퓨터 검증 분석의 가치를 대조하여 증명의 본질과 기계 시대의 진화를 탐구합니다.

기사에서 최종적으로 제안된 방법을 통해 컴퓨터는 인간의 경험을 활용한 성공적인 전략을 증명할 수 있습니다.

자동화를 통해 수학자들은 자신의 가치를 되돌아볼 수 있습니다

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01825 -4/S0273-0979-2024-01825-4.pdf

이 논문에서 저자는 특히 수학의 기계화된 미래를 고려할 때 동료들의 사고 부족을 신랄하게 비판합니다. 사회의 더 넓은 수준에서 인공 지능.

p진 숫자 필드의 연속 분수

논문 주소: https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01819 - 9/S0273-0979-2024-01819-9.pdf

연분수는 정수론, 특히 디오판토스 근사 분야에서 오랜 역사를 가지고 있습니다.

이 문서는 p진 숫자 필드 Qp에 정의된 연속 분수인 p진 연속 분수 이론의 핵심 결과를 개괄적으로 설명하는 것을 목표로 합니다.

콘텐츠는 기본 개념부터 시작하여 최신 진행 상황과 현재 직면한 문제를 소개합니다.

Tao Zhexuan 게시: 기계 보조 증명

그런데 Tao Zhexuan도 이전에 쓴 논문의 "기계 보조 증명"을 활용했습니다.

문서 주소: https://terrytao.files.wordpress.com/2024/03/machine-assisted-proof-notices.pdf

이 논문에서 Tao Zhexuan은 LLM의 자연어 입력 처리 능력 덕분에 사용자 친화적인 플랫폼이 되어 특정 소프트웨어 지식이 없는 수학자도 고급 도구를 사용할 수 있게 될 것이라고 말했습니다.

이제 그와 많은 과학자들은 이러한 모델을 사용하여 기호 대수학 패키지를 비롯한 다양한 언어로 간단한 코드를 생성하거나 복잡한 다이어그램과 이미지를 만드는 데 익숙해졌습니다.

현재 형식적 증명 검증은 인간의 노력에 크게 의존하기 때문에 현재 다수의 연구 논문을 실시간으로 완전히 형식화하는 것은 비현실적입니다.

편미분 방정식 분야에서는 여러 페이지의 계산을 통해 하나 이상의 미지 함수(예: PDE의 해)가 포함된 적분식을 추정해야 하는 경우가 많습니다.

여기에는 표준 부등식(예: Hölder 부등식 및 Sobolev 부등식)과 결합된 다양한 함수 공간 표준(예: Sobolev 공간 표준)에서 이러한 함수의 경계를 사용하고 부분별 적분 또는 적분 기호 미분 방정식 .

이러한 유형의 계산은 일상적인 작업이지만 다양한 정도의 오류(예: 부호 오류)가 포함될 수 있습니다. 검토자가 이러한 계산을 자세히 확인하는 것은 지루하고 시간이 많이 걸리는 일이며 이러한 계산 자체는 최종적으로 추정이 정확하다는 사실을 넘어 더 깊은 수학적 이해나 통찰력을 제공하기는 어렵습니다.

미래에는 자동 또는 반자동 방식으로 수학적 추정치를 설정하고 현재의 길고 지루한 추정 증명을 공식 증명 인증서 링크로 대체하는 도구가 개발될 수 있습니다.

한 단계 더 나아가, 초기 가정과 방법을 기반으로 미래의 AI 도구가 먼저 종이 작업을 하지 않고도 가능한 최선의 추정치를 제시할 수 있을 것이라고 기대할 수 있습니다. 그 추정치가 무엇인지 예측하기 위한 연필 계산입니다.

현재 가능한 상태 공간은 자동으로 탐색하기에는 너무 복잡하다고 추정되지만, 기술의 발전으로 이러한 자동화된 탐색을 실현할 가능성은 멀지 않습니다.

일단 구현되면 현재 불가능해 보이는 규모의 수학적 탐색을 수행할 수 있게 됩니다.

편미분 방정식을 예로 들어 보겠습니다. 현재 연구에서는 일반적으로 한 번에 하나 또는 두 개의 방정식만 연구하지만, 미래에는 수백 개의 방정식을 동시에 연구할 수 있습니다.

예를 들어, 먼저 방정식에 대한 완전한 인수를 개발한 다음 AI 도구가 이러한 인수를 수많은 관련 방정식 계열로 조정하도록 합니다. 필요한 경우 인수 확장이 색다른 상황에 직면할 때, AI가 저자에게 질문을 할 것입니다.

이제 그래프 이론과 같은 수학의 다른 영역에서는 이러한 대규모 수학적 탐구의 첫 징후가 이미 나타나기 시작했습니다.

그러나 현재의 이러한 예비 시도는 극도로 계산 집약적이거나 전문가 수준의 인간 참여와 감독이 많이 필요한 AI 모델에 의존하기 때문에 대규모로 추진하기가 어렵습니다.

그러나 Terence Tao는 가까운 미래에 보다 혁신적인 기계 지원 수학적 방법의 탄생을 목격하게 될 것이라고 믿습니다.