세계 최고의 수학자들은 이번 메이데이 연휴를 어떻게 보냈을까?
필즈 메달 수상자 테렌스 타오는 자신의 오픈 소스 프로젝트를 발표하는 데 바쁜 듯합니다. "저는 임의의 양의 매개변수를 포함하는 주어진 추정치가 유효한지(상수 요인의 범위 내에서) 검증하기 위해 대규모 모델의 도움을 받아 개념 증명 소프트웨어 도구를 작성했습니다."
프로젝트 주소: https://github.com/teorth/estimates
이 프로젝트에서 Tao는 분석에서 추정치를 자동으로(또는 반자동으로) 정당화하기 위한 프레임 개발했습니다. 추정치는 X≲Y 형태의 부등식(점근 표기법으로는 X=O(Y)) 또는 X≪Y 형태의 부등식(점근 표기법으로는 X=o(Y))입니다.
왜 이런 도구를 만들었을까? 이는 테렌스 타오와 비욘 브링만(타오의 전 박사과정 학생이자 현재 프린스턴 대학교 조교수) 간의 최근 논의에서 시작해야 합니다.
기호 수학 패키지는 대수학, 미적분학, 수치 해석 등의 분야에서 많은 수학 과제를 위해 이미 매우 잘 개발되었습니다. 하지만 현재로선 손실을 일정하게 유지하면서 임의로 큰 매개변수에 적용되어야 하는 불평등인 점근적 추정치를 검증하기 위한 비슷하게 정교한 도구는 없습니다. 특히 중요한 것은 함수 추정인데, 여기서 매개변수는 알려지지 않은 함수나 시퀀스(적절한 함수 공간(예: 공간)에 존재)를 포함합니다.
타오는 이에 대한 논의에 관해 블로그 게시물을 작성했는데, 덧셈, 곱셈, 나눗셈, 지수, 최소값, 최대값(뺄셈은 제외)과 같은 산술 연산을 사용하여 유한한 개수의 양의 실수를 결합하는 점근적 추정의 더 간단한 경우에 초점을 맞췄습니다.
"저는 그러한 추정이 성립하는지 자동으로 판단할 수 있는 도구(그리고 성립한다면 증명을 제공하고, 성립하지 않는다면 점근적 반례를 제시하는 도구)를 원했습니다."
이제 그 소원이 이루어졌습니다.
테렌스 타오가 수학 문제를 해결하는 데 큰 모델을 사용하는 것을 매우 좋아한다는 것은 우리 모두 알고 있습니다. 과거에는 비교적 간단한 코딩 작업을 주로 했습니다. 예를 들어, 약간 복잡한 수학 함수를 계산한 다음 그래프로 표시하거나, 일부 데이터 세트에 대한 기본적인 데이터 분석을 하는 것이었습니다.
이번에 그는 좀 더 어려운 과제를 맡기로 결심했습니다. 즉, 위와 같은 형태의 부등식을 처리할 수 있는 검증기를 작성하는 것입니다.
예를 들어, 전형적인 부등식은 약한 산술 평균-기하 평균 부등식일 수 있습니다.
여기서 abc는 양의 실수입니다.
추정치에서 지정되지 않은 (곱셈) 상수를 잃을 수 있음을 나타냅니다.
원칙적으로 이 형태의 간단한 부등식은 무차별 대입법적 분할을 통해 자동으로 풀 수 있습니다. 이런 유형의 단일 부등식은 손으로 풀기 어렵지 않지만, 일부 응용 프로그램에서는 이런 부등식을 대량 테스트하거나 대량 의 사례로 나누어야 합니다. 이 작업은 자동화에 적합해 보이며, 특히 현대 기술의 도움을 받으면 더욱 그렇습니다.
이번에 테렌스 타오가 사용한 AI 도구는 여전히 ChatGPT입니다. 그는 대형 모델의 빈번한 도움을 받아 약 4시간 동안 프로그래밍을 한 끝에 개념 증명 도구를 완성했습니다.
동시에 타오는 ChatGPT를 통한 대화 과정도 공개했습니다. 대화 과정이 매우 길다는 것을 알아내는 것은 어렵지 않습니다.
링크: https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8
처음에 Tao는 ChatGPT에 대한 자신의 요구 사항을 제시했습니다. "기호 표현식을 처리하는 Python 클래스를 작성하고 싶습니다. 그리고 x, y, z와 같은 변수를 표현하는 클래스도 있으면 좋겠습니다. 이 함수를 사용하여 기본 클래스를 작성하는 데 도움을 주시면 감사하겠습니다."
ChatGPT는 6초간 생각한 후 답을 내놓았습니다.
이 단계가 완료된 후 다음 대화 라운드가 시작되었습니다. 그러자 도저쉬안이 물었다. "+ 연산을 구현하기 위해 add를 사용하신 걸 봤습니다. 훌륭하네요. 그럼 *와 /를 구현하는 데 해당하는 메서드는 무엇인가요?"
ChatGPT도 다음과 같은 답변을 제공했습니다.
이 과정 전반에 걸쳐 Tao는 계속해서 질문을 던졌고, ChatGPT는 간단한 질문이든 복잡한 질문이든 모든 질문에 답했습니다.
「현재 파이썬 파일과 같은 디렉토리에 있는 파이썬 파일을 가져오는 방법은 무엇입니까?」
마지막으로, Tao는 ChatGPT의 큰 도움으로 이 개념 증명 소프트웨어 도구를 완성했습니다.
사실, 많은 유명 수학자 중에서 테렌스 타오는 ChatGPT와 같은 대규모 AI 모델의 수학적 가치를 처음으로 받아들이고 발견한 사람 중 한 명입니다. 그는 "적절하게 사용된다면 2026년까지 AI는 수학 연구 및 기타 여러 분야에서 신뢰할 수 있는 공동 저자가 될 것"이라고 예측한 바 있다.
테렌스 타오는 여러 차례 대규모 모델을 연구에 활용했습니다. 그는 GPT-4의 도움으로 수학 증명 문제를 성공적으로 풀었고(GPT4는 8가지 방법을 제안했는데, 그 중 하나가 문제를 성공적으로 풀었습니다), AI의 도움으로 논문에서 숨겨진 버그를 발견했습니다.
타오는 또한 이런 종류의 소프트웨어를 개발하고 싶다면 수학자와 전문 프로그래머가 협력하여 서로의 장점을 보완하는 것이 가장 좋다고 제안했습니다.
"물론 이것은 매우 우아하지 못한 증명입니다. 그러나 우아함이 중요한 것이 아닙니다. 중요한 것은 그것이 자동적으로 이루어진다는 것입니다."
전체 과정을 돌이켜보면, 테렌스 타오의 경험에서 영감을 얻을 수 있습니다. 대형 모델의 개발과 활용은 빙산의 일각에 불과할 수 있으며, 앞으로 더 많은 기능이 모든 사람에게 공개될 예정입니다.
참조 링크:
https://terrytao.wordpress.com/2025/05/01/추정치를 검증하는 개념 증명 도구/
본 기사는 단강과 천천이 편집하고 36Kr이 허가를 받아 게시한 위챗 공개 계정 "머신하트" 에서 발췌한 것입니다.

