인터뷰/예측
크리스티안 세게디 "우리는 제가 몇 년 전에 제안했던 지점에 매우 가까이 와 있습니다."
작성자
하이룽룽
작성일
2026-05-06 19:35
조회
2
22. 초인간 AI 수학자 타임라인
진행자:
당신은 예전에 초인간 AI 수학자 예측을 2029년에서 2026년으로 앞당긴 적이 있습니다. 올해 달성될까요? 어떤 능력을 보여야 그 milestone이 달성됐다고 보나요?
크리스티안:
정확히 말하면 저는 원래 2029년에서 2027년으로 앞당겼습니다. 그 후 François Chollet와 이야기하면서 2026년 6월에 베팅하게 됐습니다. 우리가 10년 전에 함께 냈던 DeepMath 논문의 10주년이기 때문입니다.
제가 제안한 기준은 꽤 명확했습니다. AI가 10개 또는 100개의 교과서를 완전히 자율적으로 형식화하는 것. 그리고 적어도 10개의 서로 다른 수학 분야에서, 인간이 10년 이상 공격해온 conjecture에 대해 AI가 완전히 자율적으로 proof를 만드는 것입니다.
제가 올해나 내년에 millennium prize problem이 풀릴 것이라고 말한 것은 아닙니다. P vs NP 같은 문제는 AI에게도 100년이 걸릴 수도 있습니다. 그런 문제들은 singular하고 얼마나 어려운지 알 수 없습니다.
하지만 형식화 능력은 지수적으로 올라가고 있습니다. 저는 올여름까지 10권의 책은 쉽게 형식화될 수 있고, 수백 권도 가능할 수 있다고 봅니다. 이미 그렇게 어렵지는 않지만 몇 년 동안 열려 있던 frontier statement들이 AI에 의해 풀리는 사례가 나오고 있습니다.
우리는 제가 몇 년 전에 제안했던 지점에 매우 가까이 와 있습니다.
23. 올해 AI가 Fields Medalist급이 될까
진행자:
아직 부족한 것은 무엇인가요?
크리스티안:
올해 여름이나 9월까지 Fields Medalist만큼 좋은 AI가 나올 것이라고는 생각하지 않습니다. 하지만 매우 강한 working mathematician, 상위 10% 수학자 수준은 될 수 있다고 봅니다.
가장 필요한 것은 검증입니다. 더 나은 verification이 필요합니다. 어려운 문제를 풀어도 그 solution이 맞는지 검증할 수 없다면 의미가 없습니다.
또 하나 필요한 것은 훨씬 더 큰 formalized mathematics repository입니다. 필요한 재료가 형식화되어 있지 않으면, 더 높은 수준의 정리를 형식화할 수 없습니다.
크리스티안 세게디 인터뷰 정리
직접 발언 형식
1. xAI 초창기와 프런티어 AI 조직을 만드는 방식
진행자:오늘은 xAI 이야기부터 해보겠습니다. 당신은 xAI 공동창업자로 알려져 있는데요. 프런티어 AI 조직은 실제로 어떻게 만들어지는 건가요? 어떤 사람을 뽑고, 어떤 방향을 잡아야 훌륭한 모델을 만들 수 있나요?
크리스티안 세게디:
저는 저 자신을 엄밀한 의미의 공동창업자라기보다는 founding scientist, founding engineer에 더 가깝다고 봅니다. xAI에서는 Elon이 조직을 대부분 만들었고, CEO로서 회사 전체를 끌고 갔습니다.
그리고 Elon은 xAI를 lab이라고 부르는 걸 별로 좋아하지 않았을 겁니다. 그는 xAI를 연구소라기보다는 세계 최고의 AI를 만들고, 여러 엔지니어링 목표를 달성하기 위한 조직으로 봤습니다.
모든 프런티어 AI 조직은 서로 다릅니다. OpenAI가 시작한 방식, Anthropic이 시작한 방식, Yann LeCun 쪽이 해온 방식, xAI가 만들어진 방식은 모두 달랐습니다. 그래서 하나의 정해진 패턴이 있다고 보지는 않습니다.
xAI 초기에 가장 중요했던 것은 이미 검증된 사람들을 모으는 일이었습니다. 언어모델, 대규모 트레이닝, GPU 활용, 인프라, 데이터센터 같은 영역에서 실제 경험이 있는 사람들이 필요했습니다.
초기 기술팀은 매우 작았습니다. 1년 정도는 기술 멤버가 12명 정도였고, 처음에는 약 5,000개 정도의 GPU를 쓰다가 나중에는 10만 개 이상, 제가 떠날 때쯤에는 20만 개에 가까운 GPU를 쓰는 상황이었습니다.
그 정도의 거대한 컴퓨트를 아주 적은 사람들이 다뤄야 했기 때문에, 무슨 일을 할지 매우 신중해야 했습니다. 그 자원을 낭비하면 안 됐습니다. 그래서 우리는 그 컴퓨트를 제대로 활용할 수 있다는 실적이 이미 있는 사람들을 뽑았습니다.
2. xAI 초기에 어떤 인재가 필요했는가
진행자:처음에 칠판에 적듯이, 우리는 프리트레이닝 전문가가 필요하고, 데이터 전문가가 필요하고, 인프라 전문가가 필요하다고 정리했나요? 아니면 그냥 똑똑한 사람들을 모으면 알아서 할 거라고 봤나요?
크리스티안:
대부분의 사람은 특정한 이유로 뽑혔습니다. 예를 들어 DeepMind에서 온 엔지니어들 중에는 프리트레이닝을 많이 해본 사람들이 있었습니다. 그들은 모델 트레이닝의 세부적인 부분을 잘 알고 있었습니다.
초기 회사에서는 서로 다른 능력이 필요합니다. 모델의 기반을 만들어야 하니까요. 데이터를 모으고, 초기 모델을 학습시키고, 인프라를 구축해야 합니다. 데이터센터를 잘 아는 사람도 필요했고, 인프라 작업을 매우 잘하는 사람도 필요했습니다.
프런티어 모델을 만들려는 스타트업은 처음부터 아주 신중하게 스킬셋을 조합해야 합니다. 나중에 엄청난 규모로 확장할 조직이라면 더욱 그렇습니다.
3. 일론 머스크의 AI 비전과 xAI의 목적
진행자:초기에는 아무것도 없는 상태인데, 목표는 매우 먼 곳에 있잖아요. 당장 다음 모델도 만들어야 하고, 1년 뒤에는 세계 최고 수준의 모델도 만들어야 합니다. 이 균형을 어떻게 잡았나요?
크리스티안:
Elon은 지능 폭발이 무엇을 의미하는지에 대해 매우 분명한 비전을 가지고 있었습니다. 그는 다른 많은 곳보다 훨씬 더 미래지향적으로 생각했습니다.
다른 큰 회사들은 AI가 중요하니까 몇십억 달러를 투자하자고 말합니다. 하지만 Elon은 이 목표를 이루려면 이것과 이것이 필요하고, 그 이유는 이것 때문이라고 생각합니다. 머릿속에 의존성 그래프가 있는 것처럼 봅니다.
AI가 커질 것이고, 우리가 직접 만들지 않으면 경쟁사에게 엄청난 돈을 지불해야 한다고 본 겁니다. 그래서 직접 만들어야 한다고 생각했습니다.
그는 AI가 다른 많은 기술의 기반이 될 것이라고 이해했습니다. 그래서 xAI를 만든 것입니다. 다만 동시에 투자를 받아야 했기 때문에, 사용자 수, 기능, 모델 성능 같은 것들을 보여줘야 했습니다. 그래야 자금을 조달할 수 있으니까요.
4. Math Inc와 자동 형식화로 넘어가다
진행자:이제 Math Inc와 자동 형식화 이야기를 해보죠. Goss 시스템이 강한 소수정리 형식화를 3주 만에 완료했다고 들었습니다. 인간 전문가들은 18개월 동안 진행하던 일이었는데요. 인간은 어디에서 막혔고, Goss는 무엇을 다르게 했나요?
크리스티안:
정확한 이야기는 이렇습니다. Alex Kontorovich와 Terence Tao가 소수정리의 어떤 버전을 증명하려는 장기 프로젝트를 하고 있었습니다. 가장 강한 형태의 소수정리는 리만 가설인데, 그것은 아직 증명하지 못했습니다.
여기서 다룬 증명 자체는 이미 오래전부터 알려진 것이었습니다. 문제는 그것을 Lean으로 형식화하는 일이었습니다. 그들은 학생들과 함께 1년 정도 작업했고, 남은 부분도 반년에서 1년 정도 더 걸릴 것으로 예상했습니다. 막힌 것은 아니었지만, 시간이 아주 많이 걸릴 것으로 본 겁니다.
우리는 이것을 좋은 테스트베드로 봤습니다. 우리가 더 빠르게 할 수 있는지 보자는 것이었습니다. Stanford의 Jared Lifschitz가 청사진을 만들었고, 우리는 그 청사진을 Goss 시스템에 입력하면서 작업했습니다. 결국 약 2주 만에 끝냈습니다.
물론 완전히 자동으로 된 것은 아니었습니다. 여전히 상당한 인간 노력이 들어갔습니다. Jared는 교과서 증명 안에 있는 미묘한 오류들을 찾아냈고, 그것들을 고쳐야 했습니다. 실제 정리는 보기보다 훨씬 더 기술적이었습니다.
단순히 기존 정리를 그대로 Lean으로 옮기는 작업이 아니었습니다. 어떤 부분에서는 수학 자체를 다시 정리해야 했습니다. 예를 들어 하나의 epsilon-delta만 필요한 게 아니라, 서로 의존하는 여러 개의 반지름 같은 보조 구조를 도입해야 했습니다.
5. Math Inc 이전의 시작점
진행자:그 시스템은 처음부터 Math Inc에서 시작된 건가요?
크리스티안:
처음에는 Math Inc가 아니라 Morph Labs에서 시작되었습니다. Morph Labs는 Jesse가 만든 회사였고, 원래는 인프라 회사에 가까웠습니다.
제가 xAI를 떠날 때 Jesse에게 말했습니다. 내가 xAI를 떠난다면, 이 형식화 프로젝트를 같이 해야 한다고요. Jesse는 좋다고 했고, 회사의 많은 자원과 관심을 이 프로젝트로 돌렸습니다.
우리의 첫 형식화 시도는 약 2,000줄의 Lean 코드를 만들어냈습니다. de Bruijn의 1960년대 결과를 기반으로 한, 단순화된 형태의 정리였습니다. 논문으로 정식 출판된 것도 아니고 일종의 folklore처럼 남아 있던 결과였습니다.
그것은 한 페이지에서 한 페이지 반 정도 되는 인간용 증명이었지만, Lean으로 형식화하니 약 2,000줄이 되었습니다. 인간이 했다면 훨씬 오래 걸렸을 작업을 반자동으로 훨씬 빠르게 한 것입니다.
6. 형식화란 무엇인가
진행자:한 걸음 물러나서 묻겠습니다. 왜 형식화가 중요한가요? 형식화란 정확히 무엇인가요?
크리스티안:
형식화라는 말은 여러 의미로 쓰입니다. 많은 사람들은 교과서에 나오는 수학을 보면 공식도 많고 복잡하니까 그것을 formal mathematics라고 생각합니다. 하지만 우리가 말하는 formal mathematics는 그런 뜻이 아닙니다.
우리가 말하는 형식 수학은 수학을 컴퓨터 코드로 바꾸는 것입니다. Lean 같은 언어로 수학을 작성하는 겁니다. Lean은 최근에 사람들이 좋아하는 언어인데, 문법이 비교적 우아하고 추상화 수준도 높습니다.
하지만 본질적으로는 코드를 쓰는 것과 비슷합니다. 다만 훨씬 더 어렵습니다. Lean으로 100줄짜리 형식화를 쓰는 것은 일반적인 C 코드 100줄을 쓰는 것보다 훨씬 오래 걸릴 수 있습니다. 깊은 수학적 이해가 필요하기 때문입니다.
형식화된 수학은 일반 논문보다 훨씬 장황합니다. 앞서 말한 정리도 인간용 논문으로는 한두 페이지였지만, Lean으로는 2,000줄이 되었습니다.
하지만 장점은 큽니다. 일단 Lean으로 작성하면 Lean 컴파일러에게 이 증명을 검증해 달라고 할 수 있습니다. 그 과정에는 AI가 필요 없습니다. 완전히 기계적인 검증입니다. Lean이 버그가 없다면, 증명이 맞는지 100% 확실하게 알 수 있습니다.
남는 오류는 보통 정리의 statement 자체가 인간이 의도한 것과 정확히 일치하는지의 문제입니다. 하지만 그 statement에 대한 proof 자체는 검증됩니다.
7. 왜 형식화가 AI 강화학습에 중요한가
진행자:그게 AI와는 어떻게 연결되나요?
크리스티안:
AI 강화학습에서 가장 부족한 자원 중 하나가 검증 가능한 문제입니다.
프런티어 수학 벤치마크를 생각해보세요. AI가 어떤 수학 문제의 해답을 텍스트로 내놓습니다. 그러면 수학자가 읽어야 합니다. 한 수학자가 이해하지 못하면 다른 수학자가 봅니다. 그리고 몇 주 동안 토론합니다. 이게 맞는지, 대충 맞는지, 구멍이 있는지, 미묘한 버그가 있는지 논쟁합니다.
하지만 Lean으로 되어 있으면 논쟁이 끝납니다. proof checker가 통과하면 그 증명은 맞습니다. 당신이 그 증명을 이해하지 못할 수는 있습니다. 너무 추상적일 수 있습니다. 하지만 맞는 것은 맞습니다.
이 점이 매우 중요합니다. AI가 점점 더 많은 수학을 만들어낼 때, 인간이 일일이 확인할 수 없기 때문입니다.
8. ProofBridge와 자연어-형식증명 연결
진행자:ProofBridge 논문에서는 자연어와 Lean proof pair를 joint embedding으로 정렬하는 접근이 나옵니다. 이런 방식은 수학 분야가 바뀌어도 잘 일반화되나요?
크리스티안:
제가 그 논문의 저자는 아니라서 세부사항을 정확히 알지는 않습니다. 다만 그런 아이디어 자체는 좋다고 봅니다. 사실 저는 2019년에 자동 형식화를 AGI로 가는 프런티어로 본 글에서 비슷한 생각을 스케치한 적이 있습니다.
자원이 적고 거대한 언어모델을 직접 학습시킬 수 없다면, 자연어와 형식증명을 연결하는 embedding 방식은 유용할 수 있습니다. 계산 효율을 높이고 연구를 가속할 수 있습니다.
하지만 오늘날 많은 자동 형식화는 그냥 agent AI 방식으로도 됩니다. 프런티어 언어모델을 사용해서 처리하는 겁니다. 꼭 그런 bridge가 없어도 됩니다. 장기적으로는 좋은 아이디어일 수 있지만, out-of-domain 일반화가 얼마나 잘 되는지는 저는 모릅니다.
9. Lean을 잘하는 모델이 코딩에도 도움이 되는가
진행자:수학 형식화를 잘하는 모델을 만들면 다른 분야에도 도움이 될까요? 예를 들어 코딩에도 전이될 수 있나요?
크리스티안:
확정적으로 말하기는 어렵습니다. 측정 결과도 들쭉날쭉합니다. 하지만 초기 reasoning model에서 이미 알려진 것은 있습니다. 비형식 수학, 즉 Lean이 아닌 일반 수학 문제를 푸는 능력은 코딩 능력에 도움이 됩니다.
그래서 매우 정교한 Lean 시스템이 있다면 프로그래밍에도 도움이 될 가능성이 높다고 생각합니다. 다만 누가 그 실험을 제대로 했는지는 모르겠습니다.
하지만 저는 Lean을 최종 목표로 보지는 않습니다. 형식화에는 두 가지 주요 목적이 있습니다.
첫째, 인간 피드백 없이 점점 더 복잡한 수학 문제를 다룰 수 있는 발판을 만드는 것입니다. Lean을 잘하면, 인간이 아직 풀지 못한 프런티어 수학 문제로 가서도 증명을 검증할 수 있습니다. 인간이 몇 년 동안 검증하기를 기다릴 필요가 없습니다.
둘째, Lean 같은 형식 언어는 모든 추론의 어셈블리 언어처럼 될 수 있습니다. 우리가 일반적으로 어셈블리 코드를 직접 보지 않지만, 프로그램 뒤에서 기계어가 작동하는 것처럼, 미래에는 자연어로 상호작용하더라도 배경에서는 형식 검증이 계속 돌아갈 수 있습니다.
10. 수학은 수학만이 아니다
진행자:수학 형식화가 수학 바깥에도 적용될 수 있다는 뜻인가요?
크리스티안:
수학은 단순히 수학만이 아닙니다. 앞으로 수학을 만드는 것이 싸고 쉬워지면, AI는 생물학, 물리학, 컴퓨터과학의 아직 수학화되지 않은 영역을 수학화할 수 있습니다.
인간은 너무 느립니다. 그래서 많은 분야가 충분히 수학화되지 못했습니다. 하지만 AI는 훨씬 빠르게 새로운 수학 분야를 만들 수 있습니다.
예를 들어 AI 자체도 아직 제대로 수학화되지 않았습니다. 우리는 AI에 대해 훨씬 더 나은 기초를 만들 수 있습니다. 그 올바른 수학은 인간이 아니라 AI가 개발할 수도 있습니다.
11. 모든 분야를 수학으로 설명할 수 있는가
진행자:그럼 모든 분야를 수학으로 설명할 수 있다고 보나요?
크리스티안:
모든 것을 수학으로 설명할 필요는 없습니다. 예를 들어 자율주행에서 표지판을 인식하는 문제 자체는 꼭 수학적으로 흥미로운 문제가 아닙니다.
하지만 더 robust한 자율주행 시스템을 만들기 위한 규칙, 더 좋은 알고리즘, 더 빠른 탐색, 더 효율적인 데이터 구조 같은 것은 수학적으로 다룰 수 있습니다.
특히 알고리즘에서는 아주 많은 영역이 수학적 통찰에 의존합니다. 어떤 알고리즘이 실제로 작동하는지, 충분히 빠른지, 메모리를 얼마나 쓰는지, 이런 것은 검증할 수 있습니다.
현재 AI가 생성하는 코드는 신뢰하기 어렵습니다. vibe coding으로 만든 프로그램은 어느 정도 작동하지만, 단점도 많습니다. 그래서 검증이 필요합니다.
12. 소프트웨어 검증과 AI 리팩터링의 위험
진행자:웹사이트나 앱 같은 것은 사용성이 사용자에게 달린 것 아닌가요? 그런 것을 어떻게 형식화할 수 있나요?
크리스티안:
모든 것을 형식화할 수는 없어도 많은 속성은 형식화할 수 있습니다.
칩 검증을 생각하면 됩니다. 칩은 최적화 과정을 거치면서 원래 인간이 지정한 동작과 달라질 수 있습니다. 그래서 검증합니다.
소프트웨어도 마찬가지입니다. 메모리 오류가 나면 안 된다, segmentation fault가 나면 안 된다, injection attack이 일어나면 안 된다, 특정 사용자의 transaction이 데이터베이스의 특정 부분을 바꾸면 안 된다, 이런 속성들은 형식화할 수 있습니다.
AI가 코드를 리팩터링해서 1만 줄을 바꿨다고 해봅시다. 무엇이 깨졌는지 누가 압니까? 현재 AI 코딩 도구는 chip design tool보다 훨씬 brittle합니다. 오류를 도입할 가능성이 매우 높습니다. 거의 보장된다고 봅니다.
그래서 우리는 코드의 중요한 invariant를 추출하고, 그것을 수학적으로 표현하고, 개발 과정 전체에서 유지되도록 해야 합니다.
13. Mathlib 150만 줄은 작다
진행자:Mathlib에는 이미 150만 줄 이상의 코드가 있습니다. 그런데 당신은 형식 수학 코드를 100배, 1000배 늘리고 싶다고 했습니다. 1년 안에 1억 5천만 줄 이상의 검증된 Lean을 만들겠다는 뜻인가요?
크리스티안:
150만 줄은 작습니다. 일반 코드와 비교하면 정말 작습니다. 간단한 프로젝트와 비교해도 큰 규모가 아닙니다.
현재 병목은 몇 가지입니다. 첫째, 인간이 아직 병목입니다. 특히 새로운 정의와 이론을 처음부터 형식화할 때, 인간이 definition이 맞는지 확인해야 하는 경우가 많습니다.
둘째, 계산 비용입니다. 형식화 노력에는 돈이 많이 듭니다. 100배 많은 검증 수학을 만들려면 비용이 내려가야 합니다.
셋째, 협업입니다. 지금은 여러 고립된 노력이 있습니다. 서로 위에 쌓이지 않고 각자 탑을 세우는 식입니다. 우리는 에이전트와 회사들이 협업하면서 전체 수학 건축물을 만들어가는 환경이 필요합니다.
14. AI가 만든 수학을 어떻게 믿을 것인가
진행자:결국 AI가 많은 증명을 만들고 그것을 검증하는 작업인가요?
크리스티안:
그것도 한 측면입니다. AI가 ABC conjecture 같은 것을 증명했다고 주장할 수도 있습니다. Mochizuki가 증명했다고 주장하지만 많은 사람이 믿지 않는 것처럼, AI도 그런 논쟁을 만들 수 있습니다.
하지만 우리 시스템이 충분히 좋아지면 그런 proof를 확인할 수 있습니다. 어디까지는 형식화되고, 어디에서 막히는지 정확히 말할 수 있습니다. 그러면 논쟁을 줄일 수 있습니다.
하지만 진짜 목표는 단지 몇몇 논쟁적인 명제를 정리하는 것이 아닙니다. 앞으로 AI 에이전트들은 매우 강력해질 겁니다. 1년, 아니 반년 안에도 인간보다 더 강력해질 수 있습니다. 그러면 인간이 가능하다고 보지 못했던 수많은 문제의 해답을 만들어낼 겁니다.
문제는 우리가 그것을 검증할 수 없다는 것입니다. AI가 영어로 된 수학을 엄청나게 많이 만들어낸다고 해봅시다. 또 다른 AI에게 확인하라고 할 수 있습니다. 하지만 그 AI를 믿을 수 있나요? 저는 믿지 않습니다.
그래서 AI 없이도 확인 가능한 형식 증명이 필요합니다. proof checker가 확인하는 증명이 있어야 합니다.
15. 형식 증명은 인간이 읽기 위한 것이 아닐 수 있다
진행자:AI가 만든 Lean proof가 너무 지저분하면 인간이 사용할 수 없지 않나요?
크리스티안:
이 부분에서 두 진영이 있습니다.
하나는 오래된 formalizer들의 관점입니다. 그들은 아름답고 인간이 읽을 수 있는 proof를 좋아합니다. 일종의 장인정신입니다. Lean proof를 잘 가꿔진 정원처럼 봅니다.
저는 다른 진영입니다. 저는 그런 proof의 아름다움에 별로 관심이 없습니다. 그 proof를 인간이 읽지 않아도 괜찮습니다. 목적은 검증입니다.
이것은 C 코드를 컴파일해서 어셈블리로 만든 뒤, 그 어셈블리를 인간 프로그래머에게 넘겨서 계속 개발하라고 하는 것과 비슷합니다. 당연히 싫어할 겁니다. 하지만 어셈블리는 인간이 읽으라고 있는 것이 아닙니다.
형식 증명도 마찬가지입니다. 배경에서 기계적으로 검증되면 됩니다. 인간은 자연어로 상호작용하고, 뒤에서는 Lean이나 다른 형식 시스템이 계속 체크하는 형태가 될 수 있습니다.
16. 생물학·화학·물리학도 검증 가능한가
진행자:수학에서는 중간 단계와 최종 해답을 검증할 수 있습니다. 생물학이나 화학에서도 그런 방식이 가능할까요?
크리스티안:
저는 수학화하기 어려워 보이는 많은 분야를 수학화할 수 있다고 매우 낙관합니다. AI가 우리의 수학 능력을 너무 강하게 만들어줄 것이기 때문입니다.
화학이나 생물학은 흐릿하고 규칙을 잘 모른다고 말할 수 있습니다. 맞습니다. 하지만 그것은 우리가 느리기 때문입니다. 인간은 새로운 이론을 만드는 데 너무 오래 걸립니다.
예를 들어 단백질 folding을 생각해봅시다. 어떤 구조가 절대 최소 에너지인지 100% 확신하기는 어렵습니다. 하지만 수학적으로 lower bound를 증명할 수는 있습니다. 최적점에서 얼마나 떨어져 있는지, 비슷한 에너지의 다른 구조가 있는지 같은 것을 정량화할 수 있습니다.
100% 논리적 검증은 아니더라도, 매우 강한 통계적 bound나 확률적 보장을 만들 수 있습니다. AI는 인간에게 거의 불가능한 이런 정교한 수학을 만들 수 있을 겁니다.
17. AI 이론과 실제 모델 사이의 간극
진행자:AI 이론을 만들 때는 항상 엄밀성과 실제 모델 사이에 trade-off가 있습니다. 실제 수십억 파라미터 모델에 딱 맞는 이론을 만들기는 어렵지 않나요?
크리스티안:
큰 파라미터 수는 오히려 수학화에 도움이 될 수도 있습니다. 큰 구조에서는 limit를 볼 수 있고, 큰 구조가 작은 구조보다 더 단순한 statement를 주는 경우가 많습니다.
우리는 이미 수학을 이용해 직관을 만들고, 그 직관을 대략적으로 적용합니다. 많은 optimizer도 수학적 아이디어에서 나왔습니다. 다만 그 수학이 실제 optimizer가 항상 더 낫다는 것을 증명하지는 않습니다.
새 attention mechanism도 마찬가지입니다. redundancy가 있고, correlation이 있고, 그것을 제거하면 더 효율적일 것이라는 수학적 직관이 있습니다. 그것을 구현해보고 잘 되면 논문을 씁니다. 증명하지는 않습니다.
AI도 이런 일을 할 것입니다. 하지만 차이는 AI가 훨씬 더 철저하게 분석할 수 있다는 점입니다. 인간은 한 달 안에 논문을 내야 하고, 누가 먼저 발표할까 봐 서두릅니다. 그래서 깊은 분석을 많이 못 합니다.
AI는 네트워크의 numerical analysis, floating point error, 연산 순서, cancellation 같은 미묘한 세부사항을 훨씬 더 많이 분석할 수 있습니다. floating point addition은 결합법칙도 성립하지 않습니다. 어떻게 더하느냐가 모델을 망칠 수도 있고 살릴 수도 있습니다.
AI는 인간보다 수천 배 더 많은 이런 세부사항을 분석할 수 있을 겁니다.
18. Math Inc는 사실 프로그램 검증 회사인가
진행자:Goss가 field medal급 proof를 형식화할 수 있다면, 결국 소프트웨어 correctness proof도 형식화할 수 있지 않나요? 그러면 Math Inc는 사실상 프로그램 검증 회사인가요?
크리스티안:
비밀이라기보다는, 그것은 처음부터 charter에 있었습니다. 우리의 목표 중 하나는 verified superintelligence를 만드는 것입니다. 그것은 프로그래밍에도 적용되고, 그 다음에는 과학에도 적용됩니다.
AI를 위한 수학은 AI 자체에 매우 유용합니다. AI는 직접 수학을 많이 사용하기 때문입니다. 그래서 mathematical AI를 AI에 적용하는 것은 자연스럽습니다.
하지만 다른 소프트웨어에도 당연히 적용됩니다. 중요한 소프트웨어는 대부분 어떤 수학적 trick이나 복잡한 logic을 포함합니다. 프로토콜을 보면 안전성을 검증해야 합니다. 어떤 adversarial player가 무엇을 하든 특정 나쁜 상황이 생기지 않는다는 것을 증명해야 합니다.
메모리 behavior, numerical behavior, algorithmic behavior, protocol safety, asymptotic memory use 같은 것은 모두 수학입니다. 코드를 제대로 분석하려면 알고리즘, limit, asymptotic similarity, domination 같은 개념이 필요합니다.
결국 코드 분석을 위해서는 매우 단단한 수학적 기반이 필요합니다. 인간이 이 모든 것을 손으로 만들려고 하면 실패할 것입니다. 하지만 AI는 할 수 있습니다.
19. Batch Normalization에 대한 회고
진행자:당신은 2015년에 batch normalization을 만든 사람 중 한 명입니다. 원래 설명은 internal covariate shift를 줄인다는 것이었는데, 이후에는 loss landscape를 smooth하게 만든다는 등 다른 설명도 나왔습니다. 그런 후속 설명을 받아들이나요?
크리스티안:
솔직히 말하면, batch normalization 아이디어는 논문보다 2년 전부터 생각하고 있었습니다. Sergey를 만났을 때 그는 독립적으로 자기 버전을 구현하고 있었고, covariate shift 아이디어를 제안했습니다. 그가 논문에 그것을 썼고, 저는 좋다고 했습니다.
하지만 저는 그 설명을 완전히 이해했다고 말하기는 어렵습니다. 저는 어떤 이론적 결과가 궁극적 진리처럼 제시되는 것에 항상 매우 회의적입니다.
제가 batch normalization을 생각한 원래 동기는 훨씬 단순했습니다. 입력을 normalize하면 네트워크가 잘 작동한다는 것은 당시에는 거의 당연한 일이었습니다. 그렇다면 왜 입력만 normalize하나요? 모든 layer의 출력은 다음 네트워크의 입력입니다. 그러면 모든 곳에서 normalize하면 되지 않나 생각했습니다.
또 다른 이유는 activation이 함수의 민감한 구간에 있어야 한다는 것입니다. activation이 너무 멀리 가면 하나가 다른 하나를 지배하고, 다른 activation은 아무 역할을 못 할 수 있습니다.
그래서 normalization이 좋은 이유는 여러 가지가 있습니다. 저에게는 normalization이 도움이 된다는 것이 거의 no-brainer였습니다.
20. Batch Normalization은 필수인가
진행자:그럼 batch normalization은 필수인가요?
크리스티안:
아니요. batch normalization은 편의 도구입니다. 올바른 hyperparameter를 모를 때, 특히 convolutional network에서는 잘 작동하는 hyperparameter 범위를 넓혀줍니다.
하지만 정확한 hyperparameter를 알고 있다면 보통 batch normalization이 꼭 필요하지는 않습니다.
21. 현재 AI 모델에서 정말 필수적인 것은 무엇인가
진행자:현재 AI 모델에서 근본적으로 필요한 것은 무엇이라고 보나요? transformer를 다른 architecture로 바꾸거나, 데이터나 학습 알고리즘을 바꿔도 되나요?
크리스티안:
좋은 AI 모델은 좋은 데이터, 좋은 optimizer, 좋은 network 없이는 보통 작동하지 않습니다. 그중 데이터는 절대적으로 중요합니다.
Normalization, infrastructure, architecture는 어느 정도 secondary입니다. 물론 너무 엉뚱한 architecture를 쓰면 안 됩니다. 하지만 꽤 다양한 architecture가 잘 작동할 수 있습니다.
우리가 LLM을 쓰는 이유는 지난 3~4년 동안 transformer 기반 LLM을 중심으로 엄청난 튜닝과 인프라가 쌓였기 때문입니다. attention mechanism, mixture of experts, KV cache, inference 최적화 등 많은 것이 이미 구축되었습니다.
이것은 hardware lottery와 비슷합니다. 저는 이것을 infrastructure lottery라고 봅니다. 새로운 인프라를 처음부터 만들어 기존 transformer 생태계와 경쟁하는 것은 매우 어렵습니다.
하지만 transformer가 5년 뒤에도 주된 workhorse일 것이라고는 생각하지 않습니다. 저는 100% 확신합니다. AI가 새롭게 설계하거나 발명한 architecture가 transformer보다 훨씬 나을 것입니다.
22. 초인간 AI 수학자 타임라인
진행자:당신은 예전에 초인간 AI 수학자 예측을 2029년에서 2026년으로 앞당긴 적이 있습니다. 올해 달성될까요? 어떤 능력을 보여야 그 milestone이 달성됐다고 보나요?
크리스티안:
정확히 말하면 저는 원래 2029년에서 2027년으로 앞당겼습니다. 그 후 François Chollet와 이야기하면서 2026년 6월에 베팅하게 됐습니다. 우리가 10년 전에 함께 냈던 DeepMath 논문의 10주년이기 때문입니다.
제가 제안한 기준은 꽤 명확했습니다. AI가 10개 또는 100개의 교과서를 완전히 자율적으로 형식화하는 것. 그리고 적어도 10개의 서로 다른 수학 분야에서, 인간이 10년 이상 공격해온 conjecture에 대해 AI가 완전히 자율적으로 proof를 만드는 것입니다.
제가 올해나 내년에 millennium prize problem이 풀릴 것이라고 말한 것은 아닙니다. P vs NP 같은 문제는 AI에게도 100년이 걸릴 수도 있습니다. 그런 문제들은 singular하고 얼마나 어려운지 알 수 없습니다.
하지만 형식화 능력은 지수적으로 올라가고 있습니다. 저는 올여름까지 10권의 책은 쉽게 형식화될 수 있고, 수백 권도 가능할 수 있다고 봅니다. 이미 그렇게 어렵지는 않지만 몇 년 동안 열려 있던 frontier statement들이 AI에 의해 풀리는 사례가 나오고 있습니다.
우리는 제가 몇 년 전에 제안했던 지점에 매우 가까이 와 있습니다.
23. 올해 AI가 Fields Medalist급이 될까
진행자:아직 부족한 것은 무엇인가요?
크리스티안:
올해 여름이나 9월까지 Fields Medalist만큼 좋은 AI가 나올 것이라고는 생각하지 않습니다. 하지만 매우 강한 working mathematician, 상위 10% 수학자 수준은 될 수 있다고 봅니다.
가장 필요한 것은 검증입니다. 더 나은 verification이 필요합니다. 어려운 문제를 풀어도 그 solution이 맞는지 검증할 수 없다면 의미가 없습니다.
또 하나 필요한 것은 훨씬 더 큰 formalized mathematics repository입니다. 필요한 재료가 형식화되어 있지 않으면, 더 높은 수준의 정리를 형식화할 수 없습니다.
24. Lean이 유일한 답인가
진행자:Lean 말고 Coq, HOL Light 같은 다른 proof assistant는 어떻게 보나요?
크리스티안:
AI에게는 Lean의 인간 친화성이 꼭 필요한 것은 아닙니다. Lean은 인간에게 좋습니다. 문법이 좋고 추상화도 좋습니다. 하지만 AI 입장에서는 Coq도 충분히 강하고, HOL Light도 충분히 강합니다. 심지어 first-order logic도 충분할 수 있습니다.
중요한 것은 하나의 충분히 강한 시스템이 있으면 된다는 점입니다. 같은 목적을 위해 10개의 서로 다른 repository를 만들 필요는 없습니다.
지금 Lean을 쓰는 이유는 데이터 때문입니다. 현재 가장 많은 형식화 데이터가 Lean에 있습니다. 그러니 자연스럽게 Lean으로 갑니다.
하지만 reinforcement learning loop를 돌려서 스스로 proof를 대량 생성하기 시작하면, 어떤 형식 언어를 쓰는지는 덜 중요해질 수 있습니다. 아주 지저분한 formalization이어도 proof checker가 검증해주면 됩니다.
25. AI 시대에 수학자의 역할
진행자:AI가 거의 모든 것을 형식화하고, 수많은 theorem을 증명하고, 자동으로 검증할 수 있게 되면 수학자의 역할은 무엇인가요?
크리스티안:
앞으로 5~10년 동안 수학자의 역할은 방향을 제시하는 쪽으로 이동할 가능성이 큽니다. 어떤 영역을 탐험할지, 어떤 이론을 개발할지 AI에게 말하고, AI와 반복적으로 상호작용하는 역할입니다.
그 역할이 영원히 지속될지는 모르겠습니다. 하지만 적어도 다음 5년 정도는 그럴 것 같습니다.
수학자는 교육에서도 역할이 있습니다. 저는 AI가 교육에 매우 도움이 될 수 있다고 생각하지만, 제 아이들이 오직 AI에게만 교육받기를 바라지는 않습니다.
저는 헝가리에 AI augmented education 회사를 시작했습니다. 목표는 교사를 AI로 대체하는 것이 아니라, 교사를 AI로 증강하는 것입니다. 채점, 문제 생성, 커리큘럼 구성 같은 지루한 일은 AI가 도울 수 있습니다. 하지만 영감, 인간적 접촉, 롤모델로서의 교사는 여전히 중요합니다.
인간은 인간과 함께하고 싶어합니다. 체스도 AI가 인간보다 훨씬 강하지만, 사람들은 여전히 인간 체스를 봅니다. 사람들은 skillful한 인간을 좋아합니다. 그 인간이 AI보다 훨씬 약하더라도 말입니다.
26. 수학은 망원경을 얻은 천문학과 비슷하다
진행자:AI 이후에도 인간 수학자의 경쟁이나 업적이 의미 있을까요?
크리스티안:
수학 역사에는 인간적 요소가 많았습니다. Cardano와 Tartaglia, Newton과 Leibniz처럼 서로 도전하고 경쟁하는 역사가 있었습니다. 사람들은 수학을 너무 비인간적인 활동으로 보지만, 실제로는 인간적 요소가 많습니다.
다만 앞으로 수학은 이상해질 것입니다. 비유하자면 망원경 이전의 천문학과 비슷합니다. 망원경 이전에는 좋은 눈을 가진 사람이 천문학자가 되기 유리했습니다. 하지만 망원경이 나오자 더 이상 자연 시력의 한계가 중요하지 않게 되었습니다.
수학도 마찬가지입니다. 우리는 수학적 우주를 인간 정신보다 훨씬 더 깊이 들여다볼 수 있는 망원경을 갖게 되는 것입니다.
수학자들은 적응해야 합니다. 많은 수학자는 아직 부정하고 있습니다. 하지만 동시에 많은 사람은 흥분할 겁니다. 마치 죽어서 천국에 갔더니 모든 것을 배울 수 있고, 신이 설명해주는 것 같은 느낌일 수 있습니다.
27. AI가 인간의 일을 빼앗는 문제보다 더 큰 문제
진행자:AI가 사람들의 일을 대체하는 문제는 어떻게 보나요?
크리스티안:
저는 인간에게 artificial work가 필요하다고 생각하지 않습니다. 그래서 그 점 자체는 크게 걱정하지 않습니다.
제가 걱정하는 것은 AI의 이익이 모두에게 공평하게 분배될지입니다. 아무도 뒤처지지 않도록 할 수 있느냐가 중요한 문제입니다.
물론 AI가 완전히 재앙이 될 가능성도 있습니다. 터미네이터처럼 모두를 죽이는 것도 매우 현실적인 outcome이라고 생각합니다. 그보다 더 이상한 시나리오들도 어느 정도 현실적이라고 봅니다.
저는 그렇게 낙관적이지 않습니다. 그래서 이런 문제를 계속 생각합니다. verification은 AI가 우리를 속이지 못하게 하고, 더 겸손하게 만드는 데 어느 정도 역할을 할 수 있다고 봅니다.
28. AI 이후의 사회 예측은 어렵다
진행자:체스에서는 Deep Blue 이후 5~10년이 지나자 인간+AI centaur도 AI 단독보다 약해졌습니다. 하지만 체스 인기는 오히려 커졌습니다. AI 시대에 일자리 종말이 올까요, 아니면 모두가 더 바빠질까요?
크리스티안:
모르겠습니다. 정말 흥미로운 질문이고 많이 생각합니다.
저는 수학 예측이나 ARC-AGI 벤치마크 예측에서 나름 좋은 기록이 있었습니다. ARC-AGI 예측은 한 달 차이로 틀렸습니다.
하지만 이제는 솔직히 말해야 합니다. 제게는 앞으로 2년 뒤는 event horizon입니다. 1년 정도는 예측할 수 있을지도 모릅니다. 하지만 2년 이상은 어렵습니다.
AI가 그 수준에 도달하면, 사회에 미치는 비선형 효과 때문에 어떤 projection도 의미를 잃을 수 있습니다.
저는 AI보다 인간을 더 불신합니다. 인류는 모두를 잘 돌본 기록이 좋지 않습니다. 인간 사회는 엉망입니다. 지금 우리는 역사적으로 더 나아져야 하는 시점에 있지만, 더 나아지고 있는 것처럼 보이지 않습니다.
AI를 이용해 인류를 노예화할 수도 있고, 독재와 초감시 사회를 만들 수도 있고, 거대한 로봇 군대를 만들 수도 있습니다. 안타깝게도 그런 일이 실제로 일어나고 있는 것처럼 보입니다.
인류는 엄청나게 밝은 미래를 가질 수도 있습니다. 하지만 우리가 그것을 파괴할 수도 있습니다.
29. 학생들은 무엇을 해야 하나
진행자:이 분야의 학생들은 무엇에 집중해야 할까요? Math Inc 같은 회사들이 대규모 자동 형식화를 할 수 있다면, 학생들은 무엇을 해야 하나요?
크리스티안:
수작업 형식화를 한다면, 재미로 하는 것은 좋습니다. 하지만 좋은 커리어라고 생각해서 하는 것은 권하지 않습니다.
수학 학생이라면 자신의 커리어와 인생 선택을 다시 생각해봐야 합니다. AI를 받아들이고, AI와 함께 즐겁게 일하고, AI를 가장 잘 활용하는 방법을 찾아야 합니다.
전통적인 커리어 경로는 곧 끝날 가능성이 큽니다. 앞으로 가장 중요한 skill set은 다른 인간과 얼마나 잘 일하는가, 그리고 AI와 얼마나 잘 일하는가가 될 것입니다.
30. AI alignment를 형식 검증할 수 있는가
진행자:모델의 alignment property를 형식 검증할 수 있을까요? 아니면 너무 비형식적이라 formal system으로는 불가능할까요?
크리스티안:
alignment를 100% 검증할 수는 없습니다. 저는 alignment보다 validation이라는 단어를 더 좋아합니다.
예를 들어 수학에서 informal statement를 formal statement로 바꿀 때, 그 둘이 실제로 같은 의미인지 확인해야 합니다. formal statement를 증명했을 때 informal statement의 증명으로 인정할 수 있는지가 문제입니다.
알고리즘도 마찬가지입니다. informal specification을 formal algorithm으로 바꿨을 때, 그 알고리즘이 정말 인간이 의도한 것을 하는지 확인해야 합니다.
이 validation은 많이 개선할 수 있습니다. 하지만 100% 확실하게 만들 수는 없습니다. informal이라는 것은 본질적으로 완전히 지정되지 않았다는 뜻이기 때문입니다. 인간이 무엇을 의도했는지 100% 확정할 방법은 없습니다.
또 더 어려운 문제도 있습니다. AI가 우리가 시킨 문제를 해결했지만, 그 과정에서 인류를 죽인다거나, 강의 물을 다 끓여버린다거나, 다른 큰 해를 끼치면 어떻게 하나요?
우리는 AI가 할 수 있는 모든 해악을 미리 지정할 수 없습니다. 그래서 AI가 모든 나쁜 일을 하지 않는다는 것을 형식적으로 검증하는 것은 매우 어렵습니다.
전체 핵심 요약
크리스티안 세게디의 관점은 이렇게 정리할 수 있습니다.xAI는 연구소라기보다 세계 최고의 AI를 만들기 위한 엔지니어링 조직이었다.
프런티어 AI 조직은 적은 수의 검증된 인재가 거대한 컴퓨트를 극도로 신중하게 쓰는 방식으로 만들어진다.
AI 시대의 핵심 병목은 “답을 만드는 능력”이 아니라 “그 답이 맞는지 검증하는 능력”이 될 수 있다.
Lean 같은 형식 수학은 미래 AI 추론의 어셈블리 언어가 될 수 있다.
AI는 수학뿐 아니라 소프트웨어, 물리학, 생물학, AI 자체까지 수학화하고 검증하는 방향으로 갈 수 있다.
인간 수학자는 점점 문제를 직접 푸는 사람에서 AI에게 방향을 제시하는 사람으로 바뀔 가능성이 크다.
하지만 AI의 미래는 밝기만 한 것이 아니며, 인간 사회가 AI를 어떻게 사용할지에 따라 감시, 독재, 전쟁, 불평등, 심지어 실존적 재앙으로 이어질 수도 있다.
전체 0