Terence Tao at IMO 2024: AI and Mathematics

AIMO Prize

테렌스 타오는 인공지능과 기계가 수학 연구에 미치는 영향에 대해 강연하며, 이는 과거부터 컴퓨터를 활용한 수학의 연장선임을 강조한다.

강연에서는 수천 년 전의 주판부터 현대의 SAT 솔버, 그리고 최근의 기계 학습과 대규모 언어 모델에 이르기까지 다양한 도구를 사용하여 수학 문제를 해결하는 방법을 소개한다.

수학자들은 이러한 도구를 활용하여 새로운 연결을 발견하고, 추측을 생성하며, 복잡한 증명을 검증하는 데 도움을 받을 수 있으며, 이는 수학 연구의 미래에 큰 영향을 미칠 것이다.

테렌스 타오는 IMO에서의 경험이 인생에서 가장 즐거운 시간 중 하나였다고 회상하며, AI와 수학, 더 나아가 수학에서의 기계 보조에 대한 강연을 시작합니다. 그는 **AI가 모든 것을 변화시키고 있다는 점**을 강조하며, DeepMind의 AlphaGeometry가 IMO 기하 문제를 푸는 능력과 AI Math Olympiad에 대한 소개를 언급합니다.

타오는 기계를 이용한 수학의 역사가 수천 년 전으로 거슬러 올라간다고 설명합니다. 로마 시대의 주판과 같은 초기 기계부터 시작하여, **컴퓨터의 개념이 전자 장치 이전부터 존재**했으며, 인간 계산자들이 중요한 역할을 수행했음을 지적합니다.

1700년대에는 로그 테이블과 같은 수학 테이블을 만드는 데 컴퓨터가 활용되었으며, 이는 현대의 데이터베이스와 유사한 역할을 했습니다. **정수열 온라인 백과사전(OEIS)과 같은 데이터베이스**는 수학자들이 연구 문제를 해결하는 데 중요한 단서를 제공합니다.

과학적 계산은 1920년대부터 시작되었으며, 헨드릭 로렌츠는 네덜란드의 거대한 둑 건설 프로젝트에서 물의 흐름을 모델링하기 위해 인간 컴퓨터를 사용했습니다. 또한, **SAT 해결사(satisfiability solvers)는 논리 퍼즐을 푸는 데 사용**되며, SMT 해결사는 추가적인 법칙과 변수를 포함하여 더욱 복잡한 문제를 해결합니다.

피타고라스 삼조 문제와 같이 컴퓨터만이 해결할 수 있는 문제도 있습니다. 이 문제는 자연수를 두 가지 색으로 칠했을 때, **항상 피타고라스 삼조를 포함하는 색이 존재**하는지를 묻는 문제입니다. 컴퓨터 계산을 통해 7,824까지의 자연수에서 이 사실이 성립함이 증명되었습니다.

🧑‍🏫 현대적인 접근 방식: 머신러닝, 대규모 언어 모델, 형식 증명 보조 도구

타오는 머신러닝, 대규모 언어 모델, 형식 증명 보조 도구가 수학 연구에 어떻게 활용되는지 설명합니다. **머신러닝은 새로운 연결 고리를 발견**하고, 대규모 언어 모델은 문제에 대한 접근 방식을 제안하며, 형식 증명 보조 도구는 주장의 진위를 확인하는 데 사용됩니다.

✅ 형식 증명 보조 도구의 발전

4색 정리 증명은 컴퓨터 보조 증명의 초기 사례 중 하나였지만, 현대적인 의미의 컴퓨터 검증 가능 증명은 아니었습니다. 케플러 추측의 증명 또한 **완전한 형식화 과정을 거쳐 2014년에 완료**되었으며, 이는 컴퓨터를 이용한 증명의 신뢰성을 높이는 데 기여했습니다.

피터 숄체의 응축 수학(condensed mathematics) 이론은 형식 증명 보조 도구 Lean을 사용하여 검증되었으며, 이를 통해 수학 라이브러리가 확장되고 **미래의 형식화 프로젝트를 지원하는 소프트웨어 도구가 개발**되었습니다.

타오 자신도 팀 가워스와 함께 조합론 문제를 해결하고 Lean을 사용하여 3주 만에 형식화했습니다. 이 프로젝트에서는 **블루프린트(blueprint)라는 도구를 사용하여 증명을 작은 단계로 나누어 협업**을 촉진했습니다.

🧠 머신러닝과 뇌 이론의 접목

매듭 이론에서 머신러닝은 **서로 관련이 없어 보이는 불변량 사이의 숨겨진 연결 고리를 발견**하는 데 사용됩니다. 신경망을 훈련하여 쌍곡선 기하 불변량으로부터 시그니처를 예측할 수 있으며, 이는 인간이 놓칠 수 있는 패턴을 드러냅니다.

🗣️ 대규모 언어 모델의 가능성과 한계

GPT-4와 같은 대규모 언어 모델은 IMO 문제를 해결할 수 있지만, 이는 예외적인 경우입니다. AI는 인간이 쉽게 해결하는 문제를 어려워하는 경향이 있으며, **정확성을 높이기 위해 다양한 시도가 진행 중**입니다.

타오는 GPT에게 문제 해결 기법을 제안받아 실제로 해결에 도움을 받은 경험을 공유하며, **대규모 언어 모델이 뮤즈(muse)로서 유용**할 수 있다고 언급합니다.

🛠️ 결론: 미래의 수학 연구 방향

타오는 AI가 수학 문제를 직접 해결하는 데는 아직 갈 길이 멀지만, **유용한 보조 도구로서의 역할**은 이미 입증되었다고 말합니다. 그는 AI가 좋은 추측을 생성하고, 다양한 수학적 객체 간의 연결 고리를 찾는 데 기여할 수 있기를 희망합니다.

미래에는 AI를 사용하여 **수천 개의 유사한 문제를 동시에 탐색**하고, 다양한 기술의 효과를 평가하는 방식으로 수학 연구가 진행될 수 있습니다. 이러한 도구를 통해 전례 없는 규모로 수학을 수행할 수 있을 것입니다.

그는 강연을 마무리하며, AI 시대에도 인간의 역할이 중요하며, **AI를 안내하기 위해서는 스스로 문제를 해결하는 능력을 유지**해야 한다고 강조합니다.

테렌스 타오 교수 소개 및 IMO 참가 경험

테렌스 타오 교수는 11세에 IMO에 참가하여 동메달, 이후 은메달, 13세에 금메달을 수상함.

강연 주제는 AI와 수학에서의 기계 보조이며, 특히 연구 수학에서의 변화에 대해 이야기할 예정임.

수학에서 기계를 사용한 역사는 수천 년 전으로 거슬러 올라가며, 주판은 초기 기계 중 하나임.

컴퓨터는 1700년대부터 테이블 생성에 사용되었으며, 현대 수학 연구에서도 데이터베이스 형태로 활용됨.

수론에서 중요한 결과인 소수 정리와 Birch and Swinnerton-Dyer 추측은 테이블을 통해 발견됨.

정수열 온라인 백과사전(OEIS)은 수학 연구 문제 해결에 도움을 주는 데이터베이스임.

과학적 계산은 컴퓨터를 이용한 대규모 연산으로, 1920년대부터 사용되었으며, Hendrik Lorentz가 유체 방정식 모델링에 활용함.

과학적 계산은 선형 방정식, 편미분 방정식, 조합 계산, 대수 문제 해결에 사용될 수 있으며, 올림피아드 기하 문제도 해결 가능함.

SAT 솔버와 SMT 솔버는 논리 퍼즐과 제약 조건 문제를 해결하는 데 사용되지만, 복잡도가 높아 확장성이 제한적임.

피타고라스 쌍 문제와 같은 특정 문제는 컴퓨터를 통해서만 해결 가능함.

수학 연구에서 컴퓨터의 창의적인 활용

기계 학습, 대규모 언어 모델, 형식 증명 보조 도구는 수학 연구에 새로운 가능성을 제시함.

대규모 언어 모델은 자연어 처리를 통해 문제 접근 방식을 제시하며, 형식 증명 보조 도구는 주장의 진위 여부를 검증하는 데 사용됨.

형식 증명 보조 도구의 활용 사례

최초의 컴퓨터 보조 증명은 4색 정리였으며, 이후 케플러 추측의 증명도 컴퓨터의 도움을 받음.

4색 정리 증명 과정에서 수동 검사의 어려움과 오류 발생 가능성이 있었음.

케플러 추측은 구를 가장 효율적으로 배열하는 문제로, 토트의 전략을 기반으로 해결되었지만, 완전히 검증된 증명은 아니었음.

Voronoi 영역을 이용하여 공간을 분할하고, 폴리토프의 통계적 특성을 분석하여 밀도에 대한 상한을 구하는 방식으로 접근함.

토마스 헤일즈는 Voronoi 셀을 변형하고, 점수를 부여하여 선형 부등식을 만들고 밀도에 대한 상한을 구하는 방법을 사용함.

점수 함수를 계속 변경하면서 동료들의 비판을 받았지만, 결국 150개 변수의 선형 부등식을 찾아 해결함.

증명 과정이 복잡해 컴퓨터를 사용하게 되었고, 4년간의 심사 끝에 99%의 정확도로 인정받았지만, 컴퓨터 계산의 정확성은 보장되지 않았음.

헤일즈는 Flyspeck 프로젝트를 통해 케플러 추측을 형식화하는 데 12년이 걸렸으며, 이를 통해 결과에 대한 완전한 신뢰를 얻게 됨.

피터 숄체는 응축 수학이라는 분야를 만들어 대수적 방법을 함수 해석에 적용하고자 했으나, 중요한 소멸 정리 증명에 어려움을 겪음.

숄체는 Lean이라는 증명 보조 언어를 사용하여 소멸 정리를 형식화하려 했으며, 수학 라이브러리가 불완전하여 추가 작업이 필요했음.

18개월 만에 소멸 정리를 형식화하는 데 성공했으며, Lean의 수학 라이브러리 확장과 함께 블루프린트라는 새로운 도구를 개발함.

블루프린트는 큰 증명을 작은 단계로 나누어 형식화하는 데 도움을 주며, 팀 협업을 용이하게 함.

형식 증명에서 인간이 읽을 수 있는 증명으로 변환하는 도구가 개발되어 상호 작용적인 교과서 제작에 활용될 수 있음.

테렌스 타오 교수 자신도 최근 조합론 문제를 형식화하는 프로젝트를 진행했으며, 블루프린트 도구를 활용하여 3주 만에 완료함.

이 프로젝트는 여러 분야의 전문가들이 협업하여 진행되었으며, Lean 컴파일러를 통해 코드의 정확성을 보장함.

증명 작업을 작은 조각으로 나누어 다양한 기술을 가진 사람들이 독립적으로 작업할 수 있도록 함.

Lean 언어를 사용한 증명은 인간이 읽기 어려울 수 있지만, 증명 과정을 여러 기술로 분리하여 협업을 용이하게 함.

형식 증명은 손으로 쓰는 것보다 시간이 오래 걸리지만, 증명을 변경하는 경우에는 더 빠를 수 있음.

현재 페르마의 마지막 정리를 Lean으로 형식화하는 프로젝트가 진행 중이며, 형식 증명 보조 도구가 계속 발전하고 있음.

기계 학습은 신경망을 사용하여 다양한 질문에 대한 답을 예측하는 데 사용될 수 있음.

매듭 이론에서 기계 학습을 사용하여 매듭 불변량 간의 연결 고리를 발견함.

신경망을 훈련시켜 쌍곡선 기하 불변량으로부터 시그니처를 예측하는 데 성공했지만, 그 이유는 알 수 없었음.

민감도 분석을 통해 중요한 입력 변수를 식별하고, 인간의 직관을 사용하여 패턴을 발견하고 추측을 세움.

신경망을 통해 얻은 정보를 바탕으로 이론적 설명을 찾아내고 증명함.

대규모 언어 모델은 인간 수준의 출력을 생성할 수 있으며, IMO 문제 해결에 성공한 사례도 있음.

대규모 언어 모델은 인간이 어려워하는 것을 쉽게 해결하지만, 인간이 쉽게 하는 것을 어려워하는 경향이 있음.

정확도를 높이기 위해 다른 신뢰할 수 있는 소프트웨어와 연결하거나, 증명 보조 언어로 출력을 강제하는 방법 등이 시도되고 있음.

대규모 언어 모델은 문제 해결뿐만 아니라 영감을 주는 역할도 할 수 있으며, 증명 보조 도구에 유용한 도구로 활용될 수 있음.

GitHub Copilot과 같은 도구를 사용하여 증명 코드를 자동 완성하고, 컴파일러와 연동하여 오류를 수정하는 방법이 연구되고 있음.

AI는 아직 수학 문제를 직접 해결하는 데는 한계가 있지만, 유용한 보조 도구로 활용될 수 있음.

AI가 좋은 추측을 생성하고, 대규모 데이터 세트를 통해 수학적 객체 간의 연결 고리를 발견하는 데 기여할 수 있을 것으로 기대됨.

AI를 사용하여 개별 문제 해결 대신 유사한 문제 클래스를 탐색하고, 다양한 기술의 효율성을 평가하는 새로운 방식의 수학 연구가 가능해질 수 있음.

미래에는 AI와 함께 전통적인 방식으로 정리 증명을 진행해야 하며, AI를 효과적으로 활용하기 위해서는 인간의 지식과 능력이 필수적임.

Voevodsky의 homotopy type theory에 대한 질문에 대해, Lean은 전통적인 수학을 형식화하는 데 중점을 두고 있으며, 다양한 강점과 약점을 가진 증명 보조 언어가 필요하다고 언급함.

박사 과정 지원에 대한 조언에 대해, 대학 진학 시기는 개인의 준비 상태에 따라 다르며, 13세에 대학에 진학한 자신의 경험이 모든 사람에게 적용되는 것은 아니라고 답함.

다양한 수학 분야에 기여한 방법에 대한 질문에 대해, 초기에는 지도 교수의 제안을 받았지만, 현재는 수학 행사에서 다른 수학자들과의 대화를 통해 연구 주제를 찾는다고 답함.

AI에 대한 관심도 최근에 생겼으며, 미래에는 융통성을 가지고 새로운 분야를 탐구하는 사람들이 많아질 것이라고 전망함.