전설적인 수학자의 등장
국제수학올림피아드(IMO)에서 11세에 동메달, 12세에 은메달, 13세에 금메달을 받으며 최연소 금메달리스트가 된 테렌스 타오 교수. 현재 UCLA의 교수이자 우리 시대 가장 영향력 있는 수학자 중 한 명인 그가 AI와 수학 연구의 미래에 대해 흥미로운 이야기를 들려주었다.
타오 교수는 "AI가 모든 것을 바꾸고 있다는 이야기를 많이 들었을 것"이라며 강연을 시작했다. 실제로 DeepMind에서 발표한 AlphaGeometry가 IMO 기하 문제를 풀 수 있게 되었고, AI 수학 올림피아드도 개최되고 있다. 하지만 그는 경쟁 수학과 연구 수학의 차이점을 강조했다. 연구 수학에서는 3시간이 아닌 몇 달, 때로는 몇 년이 걸리고, 문제를 바꿔야 할 때도 있다는 것이다.
수천 년간 이어진 기계의 도움
흥미롭게도 타오 교수는 우리가 수학에서 기계의 도움을 받은 역사가 수천 년에 달한다고 설명했다. 로마인들이 사용한 주판부터 시작해서, 컴퓨터라는 개념 자체가 300-400년 전부터 존재했다는 것이다. 다만 그때의 '컴퓨터'는 전자기기가 아니라 기계식이었고, 그 이전에는 사람이었다.
2차 대전 중에는 탄도학 계산을 위해 '컴퓨터'라는 직업이 있었다. 주로 여성들이 이 일을 담당했는데, 남성들은 전쟁터에 나가 있었기 때문이다. 당시 컴퓨팅 파워의 기본 단위는 CPU가 아니라 '킬로걸아워(kilogirl-hour)'였다. 1000명의 여성이 1시간 동안 할 수 있는 계산량을 의미했다.
1700년대부터는 컴퓨터를 이용해 주로 표를 만들었다. 네이피어의 로그표가 대표적인 예다. 사인, 코사인 등을 계산하려면 이런 거대한 표가 필요했다. 타오 교수가 고등학교 다닐 때까지도 이런 표를 사용하는 법을 배웠다고 한다.
표에서 발견된 수학의 진리들
놀랍게도 수학의 많은 중요한 결과들이 표를 통해 처음 발견되었다. 수론의 가장 기본적인 결과 중 하나인 소수 정리(Prime Number Theorem)도 그 예다. 이 정리는 큰 수 X까지 소수가 대략 몇 개나 있는지 알려주는데, 르장드르와 가우스가 발견했다. 하지만 그들은 증명할 수 없었고, 가우스와 다른 수학자들이 컴퓨터(당시에는 사람)를 시켜서 첫 백만 개의 소수 표를 만들고 패턴을 찾아낸 것이다.
현재도 수학자들은 표를 사용한다. 지금은 데이터베이스라고 부르지만 본질적으로는 같은 것이다. 온라인 정수 수열 백과사전(OEIS)이 대표적인 예다. 1, 1, 2, 3, 5, 8, 13... 이 수열이 피보나치 수열인 것을 알 수 있듯이, OEIS는 수십만 개의 이런 수열들을 담고 있다.
연구를 하다 보면 자연스럽게 어떤 수열이 나타나는 경우가 많다. 처음 5-6개나 10개 정도의 수를 계산해서 OEIS에 검색해보면, 운이 좋을 때 완전히 다른 문제를 연구하던 다른 사람이 이미 같은 수열을 발견해 놓았을 수 있다. 이런 식으로 두 문제 사이의 연결고리를 찾아내어 많은 생산적인 연구가 이루어졌다.
과학적 계산의 발전
수학에서 컴퓨터를 사용하는 가장 유명한 방법은 수치 계산이다. 1920년대부터 이런 방식을 사용해왔다. 아마도 최초의 과학적 계산을 한 사람은 헨드릭 로렌츠일 것이다. 네덜란드에서 거대한 제방을 쌓으려고 할 때 물의 흐름이 어떻게 될지 알아내기 위해 유체 방정식을 모델링해야 했다. 그는 많은 인간 컴퓨터들을 동원해서 이 작업을 해냈고, 이 과정에서 부동소수점 연산을 발명하기도 했다.
현재는 컴퓨터를 사용해서 온갖 것들을 모델링한다. 선형방정식이나 편미분방정식을 풀고, 조합론적 계산을 하고, 대수 문제도 해결한다. 원리적으로는 올림피아드의 기하 문제 중 상당수를 과학적 계산으로 풀 수 있다. 10개의 점과 몇 개의 직선, 원이 관련된 기하 문제를 20개의 실변수와 20개의 미지수를 가진 방정식 시스템으로 바꿔서 Sage나 Maple 같은 컴퓨터 대수 패키지에 넣으면 된다.
하지만 문제가 커질수록 복잡도가 지수적으로, 심지어 이중 지수적으로 증가한다. 최근까지는 이런 문제들을 무차별 대입으로 푸는 것이 현실적이지 않았지만, AI 시스템과 함께라면 더 유망해질 수 있다.
SAT 솔버의 놀라운 성과
또 다른 강력한 과학적 계산 도구는 SAT 솔버(만족가능성 해결기)다. 이는 기본적으로 논리 퍼즐을 푸는 도구다. 10개 또는 1000개의 참/거짓 명제가 있고, 세 번째 명제가 참이고 여섯 번째 명제가 참이면 일곱 번째 명제는 거짓이어야 한다는 식의 제약 조건들이 주어졌을 때, SAT 솔버는 이 모든 정보를 종합해서 특정 명제 조합을 증명할 수 있는지 결론을 내린다.
더 발전된 형태인 SMT 솔버(만족가능성 모듈로 이론)는 변수 X, Y, Z도 다루고 덧셈이 교환법칙과 결합법칙을 만족한다는 법칙들도 포함한다. 이런 법칙들과 다른 사실들을 입력해서 유한한 가정 집합으로부터 어떤 결론을 도출할 수 있는지 무차별 대입으로 시도한다.
이런 도구들은 매우 강력하지만 확장성에 한계가 있다. 시간 복잡도가 지수적으로 증가해서 1000개 정도의 명제를 넘어가면 합리적인 시간 내에 실행하기 매우 어려워진다.
하지만 실제로 문제를 해결할 수 있다. 최근의 성공 사례로 피타고라스 삼조 문제가 있다. 이는 아마도 컴퓨터로만 풀 수 있고 인간이 도움 없이는 풀 수 없을 문제다.
문제는 이렇다: 자연수를 빨간색과 파란색 두 색으로 칠한다. 어떻게 칠하든 한 색깔에는 반드시 피타고라스 삼조(3, 4, 5처럼 직각삼각형의 변의 길이를 이루는 세 수)가 포함될까?
이 문제는 인간이 증명할 수 있는 방법이 알려져 있지 않지만, 컴퓨터 증명이 존재한다. 모든 자연수가 아니라 7824까지만 가면 된다는 것이 밝혀졌다. 7824개의 수를 어떻게 두 색으로 칠하든 한 색깔에는 피타고라스 삼조가 들어있다. 2의 7824제곱 가지 경우가 있어서 무차별 대입으로는 불가능하지만, 어느 정도 영리한 방법을 쓰면 가능하다.
이 증명은 당시 세계에서 가장 긴 증명이었다. 7 CPU년의 계산이 필요했고, 증명 인증서를 생성했다. 실제 증명은 200테라바이트였지만 86기가바이트로 압축되었다.
현대적 접근법: 세 가지 혁신
최근 몇 년간 컴퓨터를 더 창의적인 방식으로 사용하기 시작했다. 타오 교수는 세 가지 방법을 제시했는데, 이들이 서로 결합되고 전통적인 데이터베이스, 기호 계산, 과학적 계산과 함께 사용될 때 특히 흥미롭다고 했다.
첫째는 기계학습과 신경망을 사용해서 새로운 연결을 발견하고, 서로 다른 수학 분야들이 인간이 보기 어려운 방식으로 어떻게 상관관계를 가지는지 찾아내는 것이다. 특히 대형 언어 모델들이 자연어를 처리할 수 있어서 때로는 문제에 대한 가능한 증명이나 접근법을 생성할 수 있다.
둘째는 형식적 증명 보조 도구다. 이는 실행 가능한 코드를 작성하는 컴퓨터 언어와 달리, 특정 논증이 실제로 참인지, 주어진 데이터로부터 결론을 도출하는지 검증하는 언어다. 최근까지는 사용하기 매우 번거로웠지만 이제는 어느 정도 사용하기 쉬워졌다.
4색 정리: 최초의 컴퓨터 보조 증명
역사상 최초의 컴퓨터 보조 증명은 아마도 1976년의 4색 정리 증명일 것이다. 모든 평면 지도는 4가지 색으로 칠할 수 있다는 정리다. 하지만 이는 현재 기준으로는 컴퓨터 증명이라고 부르기 어렵다. 절반은 컴퓨터가, 절반은 인간이 한 거대한 계산이었다.
4색 정리를 증명하는 방법은 기본적으로 국가의 수에 대한 귀납법이다. 거대한 지도가 있으면 약 1000-2000개의 특별한 부분 그래프 목록이 있고, 모든 큰 국가 그래프는 이런 부분 그래프 중 하나를 포함해야 한다는 것을 보여야 했다. 그리고 이런 부분 그래프가 있을 때마다 더 간단한 것으로 바꿀 수 있고, 간단한 것을 4색으로 칠할 수 있으면 원래 것도 칠할 수 있다는 것을 보여야 했다.
이 과정에서 각 그래프에 대해 방전가능성과 축약가능성이라는 성질을 확인해야 했다. 한 작업은 컴퓨터로 할 수 있었지만, 각 그래프를 손으로 프로그램에 입력해야 했다. 다른 작업은 실제로 인간 컴퓨터가 했다. 저자 중 한 명의 딸이 시간을 들여서 수동으로 확인해야 했다.
이 과정은 완벽하지 않았다. 많은 작은 실수들이 있었고 표를 업데이트해야 했다. 현재 기준으로는 컴퓨터 증명이나 검증된 증명이 아니었다. 90년대에 와서야 700개 정도의 그래프만 사용하는 더 간단한 증명이 나왔고, 확인해야 할 모든 것들이 매우 정확하고 명확한 성질 목록이 되었다. 현재 컴퓨터로는 몇 백 줄의 C나 Python 코드로 몇 분 만에 확인할 수 있다.
실제로 수학의 공리까지 내려가는 완전한 증명을 작성한 것은 2005년 Coq(현재는 Rocq로 개명)라는 언어를 사용해서였다.
케플러 추측: 구 충전의 최적화
또 다른 유명한 예는 구 충전에 대한 케플러 추측이다. 17세기 케플러의 매우 오래된 추측으로, 진술하기는 매우 쉽다. 단위 구들을 가지고 3차원 공간을 가능한 한 효율적으로 채우고 싶다는 것이다.
구를 채우는 명백한 방법이 있다. 삼각형 충전이라고 하는데, 과일 가게에서 오렌지를 쌓는 방식이다. 같은 밀도를 가진 정육면체 충전도 있다. 밀도는 약 74%인데, 이것이 최선일까?
이는 놀랍도록 어려운 문제로 밝혀졌다. 2차원에서는 육각형 충전이 최선이고 증명하기 그리 어렵지 않다. 8차원과 24차원에서는 최근에 답을 알게 되었다. 하지만 3차원은 1차원(자명함)을 제외하고 우리가 아는 유일한 경우였다.
이 추측에 대한 완전히 인간이 읽을 수 있는 증명은 없다. 전략은 있었다. 50년대 토트가 제안한 전략인데, 무한히 많은 구가 있고 밀도가 점근적 개념이라서 유한한 문제로 축약할 수 없지만, 유한한 문제로 줄이려고 시도할 수 있다.
충전이 있을 때마다 공간을 보로노이 영역이라는 다면체로 나눈다. 구의 보로노이 다면체는 다른 모든 구보다 그 구의 중심에 더 가까운 모든 점들이다. 이런 다면체들은 특정 부피를 가지고, 면의 개수와 표면적 등을 셀 수 있다. 충전 밀도는 이런 영역들의 평균 부피와 밀접한 관련이 있다.
이런 다면체들의 부피가 평균적으로 어떻게 행동하는지에 대해 뭔가 말할 수 있다면, 충전이 얼마나 효율적일 수 있는지에 대한 상한을 얻을 수 있을 것이다. 한 다면체가 매우 크면 근처의 다면체들이 매우 작아지도록 강제할 수 있다. 그래서 한 보로노이 셀의 부피를 다른 것과 연결하는 부등식들을 찾으려고 시도할 수 있다.
많은 시도가 있었고 일부는 성공을 주장했지만 실제 증명으로 받아들여진 것은 없었다. 결국 토마스 헤일스와 공동저자들이 문제를 해결했다. 기본적으로 같은 전략이지만 더 많은 기술적 조정을 사용했다. 보로노이 셀을 약간 더 복잡한 셀로 바꾸고, 부피 대신 각 셀에 할당하는 점수를 발명했다. 부피에 많은 작은 임시 조정을 더하거나 뺀 것이다.
이 방법은 매우 유연했다. 너무 유연해서 시도할 수 있는 것이 너무 많았다. 헤일스와 퍼거슨이 깨달은 것은 함수를 최소화하려고 시도할 때 문제에 부딪힐 때마다 점수를 바꿔서 다시 시도할 수 있다는 것이었다. 하지만 그러면 이미 확인한 모든 것들을 다시 해야 했다. 그래서 점수 함수는 점점 더 복잡해졌다.
1998년에 그들은 마침내 150개 변수의 선형 부등식들을 만족하는 점수를 찾았다고 발표했다. 처음에는 컴퓨터 보조 증명으로 만들 계획이 없었지만, 프로젝트가 점점 복잡해지면서 불가피하게 되었다.
1998년 기준으로는 엄청난 증명이었다. 250페이지의 노트와 3기가바이트의 컴퓨터 프로그램과 데이터였다. 심사받기가 매우 어려웠다. 최고 수학 저널 중 하나인 Annals of Mathematics에 보내졌는데 심사에 4년이 걸렸다. 두 명의 심사위원이 있었는데, 마지막에 그들은 증명의 정확성을 99% 확신하지만 컴퓨터 계산의 정확성은 인증할 수 없다고 했다. 저널은 매우 이례적으로 편집자의 주의사항을 달고 논문을 출판했다.
당시에는 컴퓨터 보조 증명이 실제 증명으로 인정받을 수 있는지에 대한 논란이 훨씬 많았다. 지금은 훨씬 편안하게 받아들이지만, 출판된 후에도 정말로 증명인지에 대한 의구심이 있었다.
이는 아마도 완전히 형식적인 증명 언어로 처음부터 끝까지 형식화할 강한 동기가 있었던 첫 번째 주요 고급 문제였다. 헤일스는 실제로 기존 언어를 수정한 언어를 만들어서 FlySpec 프로젝트를 시작했다. 그는 자신의 증명을 형식화하는 데 20년이 걸릴 것이라고 추정했다. 하지만 21명의 협력자의 도움으로 실제로는 12년 만에 완료했고 2014년에 나타났다.
현대적 형식화: 숄체의 응축 수학
지난 몇 년간 형식화를 위한 더 나은 워크플로우를 알아냈다. 여전히 지루하지만 나아지고 있다. 피터 숄체는 매우 저명한 젊은 수학자로, 응축 수학이라는 놀라운 새로운 수학 분야를 만들었다. 이는 대수, 범주론의 모든 도구들을 함수해석학에 적용하는 것이다.
함수해석학은 대수적 방법에 정말로 저항적이었다. 하지만 이 수학 분야는 원리적으로 함수해석학의 특정 유형의 질문들을 대수적 방법으로 해결할 수 있게 해준다. 그는 응축 아벨 군, 응축 벡터 공간이라는 것들의 전체 범주를 설정했다.
그의 논제는 우리가 대학원 수업에서 배우는 모든 함수 공간 범주들이 틀렸거나 가장 자연스러운 것이 아니라는 것이다. 더 좋은 성질을 가진 것들이 있다는 것이다.
하지만 매우 중요한 소멸 정리가 있었는데, 이를 증명해야 했다. 이것 없이는 전체 이론이 흥미로운 결과를 가지지 못한다. 그는 이 결과에 대한 블로그 글을 썼는데, 이 정리의 증명에 1년을 보내며 거의 미쳐가면서 집착했다고 했다. 결국 논문에서 논증을 얻을 수 있었지만 아무도 세부사항을 보려고 하지 않았다. 여전히 의구심이 남아있다고 했다.
이 정리로 응축 형식이 함수해석학에 유익하게 적용될 수 있다는 희망이 서거나 무너진다. 이 정리는 가장 기초적으로 중요하고 99.9% 확신하는 것으로는 충분하지 않다. 그는 이것이 자신의 가장 중요한 결과일 수 있으니 정확한지 확실히 해야 한다고 했다.
그래서 그는 이 정리를 Lean이라는 현대적 언어로 형식화하기로 했다. Lean은 최근 몇 년간 많이 발전한 언어로, 거대한 수학 라이브러리를 개발하는 크라우드소싱 노력이 있다. 수학의 공리부터 시작하는 것은 매우 지루해지므로, 이미 많은 중간 결과들을 증명한 중앙 수학 라이브러리가 있다. 대략 학부 수학 교육 수준에서 시작할 수 있다.
이 이론을 형식화하기 위해서는 많은 것들을 추가해야 했다. 수학 라이브러리가 완전하지 않았기 때문이다. 형식 대수, 대수 이론, 위상수학 이론을 추가해야 했다. 단 18개월 만에 이 이론을 형식화할 수 있었다. 증명은 기본적으로 정확했다. 약간의 기술적 문제들이 있었지만 정말 중요한 것은 발견되지 않았다.
이 프로젝트의 가치는 더 간접적이었다. 첫째, 수학 라이브러리에 크게 기여했다. 이제 이 라이브러리는 추상 대수를 훨씬 더 큰 범위까지 다룰 수 있다. 또한 향후 형식화 프로젝트들이 사용하기 시작한 다른 지원 소프트웨어들이 설정되었다.
예를 들어, 이 프로젝트 과정에서 설정된 도구 중 하나가 블루프린트라는 것이다. 50페이지짜리 거대한 증명을 직접 형식화하려고 시도하는 것은 정말 고통스럽다. 전체 증명을 머릿속에 담고 있어야 한다. 올바른 워크플로우는 큰 증명을 가져와서 먼저 블루프린트를 작성하는 것이다. 이는 증명을 수백 개의 작은 단계들로 나누는 것이다. 각 단계를 별도로 형식화할 수 있고, 그것들을 모두 합친다.
협업적 형식화: PFR 프로젝트
타오 교수 자신도 작년에 프로젝트를 시작했다. 팀 가워스를 포함한 여러 사람들과 함께 조합론 문제를 해결했다. 33페이지 증명을 단 3주 만에 약 20명의 그룹 프로젝트로 형식화했다. 이는 실제로 가장 빠르게 형식화된 실제 연구 논문이다.
기본적으로 큰 정리를 가져와서 많은 작은 조각들로 나눈다. 의존성 그래프가 있고, 다른 색깔들이 형식화되었는지 여부에 따라 다르다. 초록색 버블은 이미 언어로 형식적으로 증명된 명제다. 파란색 버블은 아직 형식화되지 않았지만 형식화할 준비가 된 것이다. 모든 정의가 제자리에 있다. 흰색 버블은 명제조차 아직 형식화되지 않은 것이다.
이 프로젝트의 아름다운 점은 모든 사람이 이 그래프의 다른 조각들에서 독립적으로 협업할 수 있다는 것이다. 모든 작은 버블은 어떤 명제에 해당한다. 전체 증명을 이해할 필요 없이 자신의 작은 조각만 작업하면 된다.
이는 조합론 문제였지만 기여한 사람들 중에는 확률론 사람들도 있었고, 수학자가 아닌 사람들도 있었다. 컴퓨터 프로그래머들이었지만 이런 작은 미니 퍼즐 같은 것들을 매우 잘했다. 모든 사람이 자신이 할 수 있다고 생각하는 버블 하나를 골라서 했다.
수학에서는 보통 이렇게 많은 사람들과 협업하지 않는다. 보통 5명이 최대다. 큰 프로젝트에서 협업할 때는 모든 사람의 수학이 정확하다고 신뢰해야 하는데, 특정 크기를 넘어서면 이는 불가능하다. 하지만 이런 프로젝트에서는 Lean 컴파일러가 자동으로 확인한다. 컴파일되지 않는 것은 업로드할 수 없다. 그래서 전에 만난 적이 없는 사람들과도 협업할 수 있다.
형식화하는 것은 여전히 고통스럽다. 도구들이 더 사용자 친화적이 되고 있지만 여전히 프로그래밍에 대한 전문 지식이 필요하다. 손으로 쓰는 것보다 아마 10배 정도 더 오래 걸린다. 하지만 증명을 바꾸고 싶다면, 예를 들어 정리에서 12를 11로 개선했을 때, 보통은 전체 증명을 다시 써야 한다. 하지만 형식화했을 때는 며칠 만에 12를 11로 바꿀 수 있었다. 12를 11로 바꾸면 컴파일러가 5개 다른 곳에서 불평했고, 증명의 어떤 특정 부분이 작동하지 않는지 정확히 알 수 있었다. 그래서 표적화된 수정만 하면 되었다.
특정 유형의 수학을 하는 데는 이미 형식적 접근법이 실제로 더 빠르다. 현재 꽤 많은 큰 증명 형식화 프로젝트들이 진행 중이다. 가장 큰 것은 케빈 버자드의 프로젝트로, 페르마의 마지막 정리를 Lean으로 형식화하는 큰 보조금을 받았다. 그는 이 증명의 가장 중요한 부분들을 5년 안에 할 것이라고 말한다.
기계학습의 놀라운 발견: 매듭 이론
기계학습에 대해서도 이야기해보자. 매듭 이론은 수학의 재미있는 분야다. 많은 다른 수학 분야들을 하나로 모으는데, 이들은 서로 대화하지 않는다. 매듭은 그냥 공간에서 닫힌 끈이나 곡선의 고리다. 두 매듭이 동등한지는 끈이 자기 자신을 가로지르지 않는 방식으로 하나를 다른 것으로 연속적으로 변형할 수 있는지에 달려있다.
기본 질문은 두 매듭이 언제 동등한지다. 이 질문에 접근하는 방법은 보통 매듭 불변량이라는 것들을 개발하는 것이다. 이는 매듭에 붙일 수 있는 다양한 수들이고, 때로는 다항식들이다. 이 수들은 매듭을 어떻게 연속적으로 변형하든 바뀌지 않는다.
많은 유형의 매듭 불변량들이 있다. 시그니처라는 것이 있는데, 매듭을 평평하게 해서 교차점들을 세고, 교차점이 위로 가는지 아래로 가는지 보고, 특정 행렬을 만들어서 시그니처라는 정수를 얻는다. 존스 다항식과 호믈플라이 다항식 같은 유명한 다항식들도 있다. 그리고 쌍곡 불변량이라는 시스템이 있는데, 이는 기하학에서 온다. 매듭의 여집합을 취하면 실제로 쌍곡 공간이라는 것이 된다.
모든 매듭은 시그니처 같은 조합론적 불변량과 쌍곡 부피 같은 기하학적 불변량을 가진다. 하지만 이 둘 사이의 연결은 아무도 몰랐다.
최근에 사람들이 기계학습을 사용해서 이 문제를 공격하기 시작했다. 수백만 개의 매듭 데이터베이스를 만들었고, 이에 대해 신경망을 훈련시켰다. 훈련 후에는 모든 쌍곡 기하학 불변량들을 주면 90%의 확률로 올바른 시그니처를 추측할 수 있었다.
이는 시그니처가 어떻게든 이런 기하학적 불변량들 어딘가에 숨어있다는 것을 보여주는 블랙박스를 만들었다. 하지만 어떻게인지는 말해주지 않았다. 그래도 이 블랙박스가 있으면 가지고 놀 수 있다.
다음에 한 것은 매우 간단한 분석이었다. 현저성 분석이라고 한다. 이 블랙박스는 약 20개의 다른 입력(각 쌍곡 불변량마다 하나)을 받아서 하나의 출력(시그니처)을 낸다. 블랙박스가 있으면 각 입력을 조정해볼 수 있다. 하나의 입력을 바꾸면 출력이 바뀔 가능성이 얼마나 되는지 볼 수 있다.
20개 입력 중에서 실제로 출력에 중요한 역할을 하는 것은 3개뿐이라는 것을 발견했다. 나머지 17개는 거의 관련이 없었다. 그들이 예상한 3개가 아니었다. 예를 들어 부피가 매우 중요할 것이라고 예상했는데 부피는 거의 관련이 없었다. 가장 중요한 것은 경도 변환과 메리디안 변환의 실수부와 복소수부였다.
가장 중요한 것들을 식별한 후에는 시그니처를 그 3개 특정 입력에 대해 직접 플롯할 수 있었다. 그러면 신경망 대신 인간 네트워크를 사용해서 명백한 패턴들을 볼 수 있었다. 이런 그래프들을 보면서 실제로 무슨 일이 일어나고 있는지에 대한 추측을 만들 수 있었다.
그들은 이에 기반해서 추측을 만들었는데, 실제로는 틀렸다. 하지만 신경망을 다시 사용해서 그것이 틀렸다는 것을 보여줄 수 있었다. 그것이 실패한 방식을 통해 추측을 수정할 수 있었다. 그래서 실제로 이 현상을 설명하는 수정된 버전의 추측을 찾았다. 올바른 명제를 찾은 후에는 그것을 증명할 수 있었다.
이것이 기계학습이 수학에서 점점 더 사용되는 방식이라고 생각한다. 직접 문제를 풀어주지는 않지만, 연결이 무엇인지, 어디서 찾아야 하는지에 대한 매우 유용한 힌트들을 준다. 하지만 실제로 연결을 만드는 것은 여전히 인간이 필요하다.
대형 언어 모델의 가능성과 한계
마지막으로 대형 언어 모델이 있다. 이는 가장 화려하고 가장 많은 뉴스를 만들었다. GPT-4가 나왔을 때 그 능력을 설명하는 논문이 있었다. 그들은 기본적으로 2020년 IMO의 질문을 입력했다. 약간 단순화된 버전이었지만, 이 특정 질문에 대해 실제로 완전하고 정확한 해답을 주었다. 실제로 IMO 문제를 풀었다.
하지만 이는 극도로 선별된 예시다. 수백 개의 IMO 수준 질문들을 테스트했는데 성공률은 약 1%였다. 이 특정 문제는 풀 수 있었지만 올바른 방식으로 문제를 형식화해야 했다.
한편으로는 이런 도구들의 재미있는 점은 인간이 어렵다고 생각하는 것을 AI가 매우 쉽게 할 수 있을 때가 있지만, 인간이 쉽다고 생각하는 것을 AI가 종종 어려워한다는 것이다. 매우 직교적인 문제 해결 방식이다.
관련 논문에서 같은 모델에게 기본적인 산술 계산을 하라고 했다. 7×4 + 8×8. 모델은 입력에 기반해서 가장 가능성 높은 출력을 추측하는 것이므로 기본적으로 이 답을 120이라고 추측했다. 그리고 잠시 멈춰서 왜 120인지 설명해야겠다고 했다. 단계별로 했는데, 단계별로 했을 때는 실제로 정답인 92에 도달했다. 처음에 말한 답과 다른 답이었다.
그래서 "잠깐, 120이라고 했잖아"라고 물으면 "아, 그건 오타였어요. 죄송합니다. 정답은 92입니다"라고 한다. 그들은 첫 번째 원리로 문제를 푸는 것이 아니라 각 단계에서 다음에 말할 가장 자연스러운 것이 무엇인지 추측하고 있다. 놀라운 것은 때로는 이것이 작동한다는 것이다. 하지만 종종 그렇지 않다.
사람들은 온갖 것들을 시도하고 있다. 이런 모델들을 다른 더 신뢰할 수 있는 소프트웨어에 연결할 수 있다. 계산을 직접 하지 않고 Python에 아웃소싱하는 것이다. 또 다른 방법은 언어 모델이 이런 증명 보조 언어 중 하나로만 출력하도록 강제하는 것이다. 컴파일되지 않으면 AI에게 다시 보내서 다시 시도하게 한다.
IMO 문제를 푸는 데 사용하는 것과 같은 문제 해결 기법들을 직접 가르칠 수도 있다. 간단한 예시를 시도하고, 모순으로 증명하고, 실제로 단계별로 증명하는 것 등이다.
현재로서는 수학 올림피아드 문제의 대다수를 풀 수 있는 수준에는 전혀 가깝지 않고, 수학 연구 문제는 말할 것도 없다. 하지만 진전을 보이고 있다.
실제로 문제를 직접 풀 수 있는 것 외에도, 뮤즈로서도 유용하다. 타오 교수 자신도 이런 모델들을 실험해봤다. 조합론 문제가 있었는데 몇 가지를 시도해봤지만 작동하지 않았다. 실험으로 GPT에게 이 질문에 어떤 다른 기법들을 제안하겠냐고 물어봤다. 10가지 기법 목록을 줬는데, 그 중 5가지는 이미 시도해봤거나 명백히 도움이 되지 않는 것들이었다. 하지만 시도해보지 않은 기법이 하나 있었는데, 이 특정 질문에 생성함수를 사용하는 것이었다. 그들이 제안하자 그것이 올바른 접근법이라는 것을 깨달았지만 놓쳤던 것이다.
미래를 향한 전망
현재 우리는 어디에 있을까? 몇 년 안에 컴퓨터를 사용해서 수학 문제를 직접 풀 수 있기를 바라는 사람들이 있다. 아직 그것과는 거리가 멀다고 생각한다. 매우 좁게 집중된 문제들에 대해서는 매우 좁은 범위의 문제들만 다루는 특화된 AI를 설정할 수 있다. 하지만 그것들도 완전히 신뢰할 수 있지는 않다.
앞으로 몇 년간은 기본적으로 정말 유용한 보조 도구가 될 것이다. 이미 익숙한 무차별 대입 계산 보조를 넘어서서 말이다. 사람들은 온갖 창의적인 것들을 시도하고 있다.
특히 흥미롭다고 생각하는 한 방향은 아직 정말 성공적이지는 않지만, AI가 좋은 추측을 생성하는 데 매우 좋아지기를 바라는 것이다. 매듭에서 본 작은 예시처럼, 거대한 데이터셋을 만들어서 AI에 입력하면 자동으로 서로 다른 수학적 객체들 사이의 좋은 연결들을 많이 생성할 것이다. 이는 아직 어떻게 해야 할지 모르는 것이다. 부분적으로는 이런 거대한 데이터셋이 없기 때문이다.
또 다른 흥미로운 것은 아직 존재하지 않는 방법의 유형이다. 현재는 정리를 증명하는 것이 매우 고통스럽고 세심한 과정이기 때문에 한 번에 하나씩, 또는 효율적이면 두세 개씩 증명한다. 하지만 AI와 함께라면 미래에는 하나의 문제를 증명하려고 시도하는 대신 1000개의 비슷한 문제 클래스를 가져와서 AI에게 이 1000개 문제를 이 기법으로 풀어보라고 할 수 있을 것이다. 그러면 이 기법으로 이런 문제들의 35%를 풀 수 있다고 돌아올 것이다. 이 기법은 어떨까? 이 비율의 문제들을 풀 수 있다. 이것들을 결합하면 이만큼 할 수 있다.
각 문제를 별도로 하는 대신 문제들의 공간을 탐색하기 시작할 수 있다. 이는 현재 할 수 없는 것이거나, 수십 년에 걸쳐 수십 편의 논문으로 다양한 기법들로 무엇을 할 수 있고 없는지 천천히 알아내는 과정이다. 하지만 이런 도구들과 함께라면 정말로 전례 없는 규모로 수학을 할 수 있을 것이다.
미래는 정말 흥미로울 것이다. 여전히 옛날 방식으로도 정리를 증명할 것이다. 이런 AI들을 안내하고 또한 스스로 이런 것들을 하는 방법을 알아야 하기 때문이다. 하지만 현재 할 수 없는 많은 것들을 할 수 있게 될 것이다.
마무리: 연속성 속의 혁신
타오 교수의 강연은 AI와 수학의 만남이 혁명적이면서도 연속성을 가지고 있다는 통찰로 마무리되었다. 우리는 수천 년간 도구를 사용해서 수학을 해왔고, 지금은 그 도구들이 더 정교해지고 있을 뿐이다.
형식적 증명 보조 도구는 수학자들이 더 큰 규모로 협업할 수 있게 해주고, 기계학습은 인간이 놓칠 수 있는 패턴과 연결을 발견하게 해주며, 대형 언어 모델은 새로운 아이디어의 원천이 되고 있다.
하지만 가장 중요한 것은 이 모든 도구들이 인간의 창의성과 직관을 대체하는 것이 아니라 증폭시킨다는 점이다. 미래의 수학은 인간과 기계가 협력하여 지금까지 불가능했던 규모와 깊이로 탐구할 수 있는 새로운 영역이 될 것이다.