수학, AI 추론(Reasoning)의 ‘최종 시험대’일까요? 아니면 다음-토큰을 예측한다(Next-Token Prediction)는 학습 방식 자체가, 새로운 진리(Truth)나 추측(Conjecture)을 만들어내는 데 본질적인 한계를 갖고 있는 걸까요?

Axiom Math의 공동창업자이자 CEO인 카리나 홍(Carina Hong)은 “진짜 추론 능력을 만들려면, ‘말 잘하는(Chatty)’ 모델을 넘어서 형식 논리(Formal Logic)로 스스로의 작업을 검증(Verify)할 수 있는 시스템이 필요하다”고 말합니다.

Axiom은 최근 “Transformers know more than they can tell: Learning the Collatz sequence”라는 흥미로운 연구도 공개했습니다. 작은 트랜스포머(Transformer) 하나가, 단순히 패턴을 외우는 수준이 아니라 콜라츠(Collatz) 스타일의 난해한 알고리즘에 숨어 있는 제어 로직(Control Logic) 자체를 학습할 수 있다는 내용인데요. 더 재미있는 건 모델이 틀릴 때입니다. 실수가 무작위 환각(Hallucination)처럼 흩어지지 않고, 구조적으로 일관되고 설명 가능한 형태(Structured & Explainable)로 나타납니다. 그래서 콜라츠는 “트랜스포머가 알고리즘적 추론(Algorithmic Reasoning)을 어떻게 획득하는가”를 관찰하는 현미경(Microscope)이 됩니다. 산술(Arithmetic) 트릭도, 암기된 매핑(Memorized Mapping)도 아니고, 루프(Loop) 구조 자체를 내재화한다는 점에서 ‘깨끗한 증거’에 가깝죠. 심지어 오류가 “무슨 알고리즘을 배웠는지”를 드러내기도 합니다. 트랜스포머가 알고리즘을 학습하는 메커니즘(Mechanism)을 들여다볼 드문 창을 열어준 셈입니다.

이번 인터뷰에서는 아래와 같은 내용을 Carina Hong과 이야기합니다:

또, 자동 형식화(Auto-Formalization)의 ‘닭-달걀(Chicken-and-Egg)’ 문제, Axiom이 범용(General) 모델보다 특정 초지능(Specific Superintelligence)에 베팅하는 이유, 그리고 AI가 앞으로 ‘하드 사이언스(Hard Science)’의 알고리즘적인 기둥(Algorithmic Pillar)이 될 수 있다는 전망까지—병목과 해법을 함께 짚어봅니다.

Q. 안녕하세요, 카리나. 인터뷰 함께 해 주셔서 감사합니다. 정말 어려운 문제를 정면으로 다루고 계신 것 같은데요. 바로 질문 드릴께요. 좀 당황스러운 순간이 있잖아요. 다들 AGI 얘기를 하는데, 제가 모델에게 물었어요. “이 식사는 400칼로리, 이 식사는 350칼로리, 간식은 200칼로리, 저녁은 350칼로리야. 합치면 얼마야?” 그랬더니 “총 800칼로리니까 괜찮아요”라고 답하더라고요. 저는 그냥 멍해졌죠. 왜 수학은 이렇게 어려운 걸까요?

불러주셔서 감사합니다. 좋은 질문이에요. 지금의 모델들은 기본적으로 다음-토큰을 예측하는(Next-Token Prediction) 방식으로 훈련됩니다. 그런데 그 방식은 우리가 수학적 추론(Mathematical Reasoning)을 할 때의 사고 과정과는 다릅니다. 인간 수학자는 “다른 사람들이 맞다고 하니까”라는 이유만으로 답을 내놓지 않잖아요.

게다가 현재의 모델은 인간의 선호(Human Preference)에 맞춰 학습되는 면도 큽니다. 비슷한 개념이 등장해도 문제는 완전히 달라질 수 있는데, 훈련 데이터에 그 ‘개념’이 많이 들어 있다고 해서 자동으로 해결되는 건 아니죠.

모델이 수학에서 잘하는 부분도 분명 있습니다. 예컨대 수학자의 비서(Secretary)처럼, 참고문헌을 찾고 오래된 논문—심지어 어떤 독일 수학자의 노트—에서 관련 내용을 찾아주는 일은 잘합니다. 이런 검색(Retrieval & Search)은 머신이 강한 영역이에요. 하지만 완전히 새로운 수학 지식(de novo Mathematical Knowledge)을 만들어내는 건 아직 약합니다.

산술(Arithmetic)처럼 기본적인 계산에서 틀리거나, 기초 선형대수(Linear Algebra) 증명에서 삐끗하는 일도 흥미롭죠. 그리고 일반적으로 문제가 복잡해질수록—다단계 추론(Multi-step Reasoning)이고 탐색 트리(Tree)가 깊어질수록—모델은 더 크게 흔들릴 가능성이 큽니다.

Q. 그렇다면 인간이 없이도 꽤 독립적으로 사고하고 작동하는 AI 수학자(AI Mathematician)를 만들려면, 어떤 단계가 필요할까요? 가장 큰 병목은 무엇인가요? 어렵고 큰 질문인 건 알지만 한 번 말씀 부탁드려요.

저희는 AI 수학자에게 중요한 요소가 세 가지 있다고 봅니다.

첫째는 증명기(Prover) 시스템입니다. 질문을 받았을 때, 단순히 “답”만 내놓는 게 아니라 정식 증명(Proof)을 만들어낼 수 있어야 하죠. 비형식(Informal) 모델은 종종 숫자 답만 말합니다. 하지만 수학이 ‘검증 가능(Verifiable)’하다는 건, “957은 957이다”를 채점할 수 있다는 의미만이 아니에요. 중간 과정(Intermediate Steps), 즉 추론 과정(Reasoning Process) 자체가 기계적으로 검증 가능해야 합니다. 그게 첫 번째입니다.

둘째는 지식 기반(Knowledge Base)입니다. 무엇이 이미 축적되어 있고, 무엇이 비어 있는지 알아야 합니다. 증명기가 더 많은 정확한 증명(Correct Proof)을 만들어낼수록, 추측(Conjecture)이 정리(Theorem)로 바뀌고, 새로운 정의(Definition)나 개념(Concept)이 지식 기반에 추가될 수 있어야 해요. 이 지식 기반은 인용(Citation) 중심의 지식 그래프(Knowledge Graph) 같은 구조를 가질 수도 있겠죠.

셋째는 추측(Conjecture) 시스템입니다. 흥미로운 새 수학 질문을 제안하는 모델이 필요해요. 추측 모델이 과제를 던지고, 증명 모델이 풀고, 둘이 서로 피드백을 주고받으면서 자기개선(Self-improving) 루프를 만드는 겁니다. 추측 모델은 증명 모델이 무엇을 잘하고 무엇에서 막히는지 보면서, 증명 모델이 ‘언덕을 오르듯이(Hill-Climb)’ 실력을 끌어올릴 수 있는 새로운 커리큘럼(Curriculum)을 스스로 구성할 수 있어야 합니다.

그리고 이 모든 걸 엮는 핵심이 바로 자동 형식화(Auto-Formalization)예요. 자연어 수학(Natural Language Math)을 린(Lean) 같은 형식 언어로 옮기는 능력이죠. 반대로 Lean을 다시 자연어로 풀어주는 자동 비형식화(Auto-Informalization)도 필요합니다. 추측은 대개 자연어 직관에서 나오고, 증명은 형식 언어에서 이루어지고, 다시 인간이 이해 가능한 형태로 돌아와야 하니까요.

만약 어떤 명제가 자연어로 주어지고, 증명기가 형식 언어로 증명한 다음, 그 결과를 다시 자연스러운 영어(혹은 한국어)로 풀어낼 수 있다면, 인간 수학자에게도 실제로 영감을 줄 수 있을 겁니다.

마지막으로 한 가지 더 이야기하자면, AI 수학자가 엄청난 역량을 갖게 되더라도, 인간 수학자와의 협업(Collaboration)은 여전히 중요하다고 봅니다. 인간이 어렵다고 느끼는 것과 머신이 어렵다고 느끼는 것이 다를 때가 많거든요. 두 존재가 완전히 같은 강점/약점을 갖고 있다면 “초지능(Superintelligent)이 되면 인간은 왜 필요하냐”는 질문이 생기겠죠. 그런데 저희는 둘은 서로 다른 영역에서 강하다고 봅니다. 그래서 협업의 시너지가 생깁니다.

Q. 여기서 추측 모델로 다시 가볼게요. 수학은 끝이 없는데, 모델은 어떻게 “이게 의미있는 추측이다”라는 결론을 만들어내나요? 인간 수학자의 직관(Intuition)과도 연결되는 것 같은데요. 직관은 어떤 역할을 하고, 그걸 모델에 담을 수 있을까요?

제가 “와, 이건 정말로 새로운 지식을 만들 수 있는 공간이다”라고 느낀 순간은 AlphaGeometry 논문이었습니다.

AlphaGeometry에서 Google DeepMind가 유클리드 기하(Euclidean Geometry)의 도형—삼각형, 원, 직선, 교점 같은 것—을 기호 언어(Symbolic Language)로 바꿉니다. 그리고 그걸 벡터 기반(Vector-based) 표현으로 옮긴 뒤, 그 공간에서 새로운 기하 문제를 de novo로 만들어냅니다. 일종의 코드 조각(Code Snippet)을 생성한 다음, 다시 기하 표현으로 변환하는 방식이죠.

그 결과 아주 창의적인 기하 문제가 합성(Synthetic)으로 생성됩니다. 정말 강력한 아이디어예요.

비슷한 흐름으로, 제 동료 프랑수아 샤르통(François Charton)과 알베르토 비에티(Alberto Bietti)의 ‘수학적 발견(Mathematical Discovery)’ 작업도 있습니다. 두 사람은 이전에는 Meta의 FAIR(Fundamental AI Research)에 있었고, 지금은 Axiom에 있어요. 이들은 ‘추측’ 자체보다는, 흥미로운 구성(Construction)이나 예시(Example), 즉 수학적 대상(Mathematical Object)을 기계학습으로 만들어냅니다.

그리고 인간 수학자들은 그 대상들이 만들어내는 ‘패밀리(Family)’를 관찰하면서, 그 속에 숨은 패턴(Underlying Pattern)을 포착하고 새로운 추측을 세워요. 즉 머신이 ‘예시를 만들어주고’, 인간이 그걸 통해 직관을 강화해 추측을 만든다는 그림입니다.

직관(Intuition)은 정말 큰 주제죠. 한 축은 이런 예시/구성을 많이 생성하는 능력이고, 다른 축은 그걸 종합(Synthesize)해서 ‘의미 있는 질문’을 정식화(Formulate)하는 능력입니다.

또 다른 접근도 있습니다. 형식 언어(Formal Language) 공간에서, 몇 개의 시드(Seed) 명제를 받아서 새로운 문제나 명제를 합성해서 만들어내는 방식이죠. 예를 들면 스탠퍼드의 STP(Self-Taught-Theorem-Prover) 계열 연구가 그렇습니다. Lean Workbook이라는 고등학교 수준의 수학 데이터에서 시드 명제를 가져와서, 완전히 Lean 형태의 추측을 생성하고, 증명 모델이 그 추측 모델에 보상(Reward)을 주도록 만듭니다.

다만 여기엔 설계 난제가 있어요. 시스템이 앞으로 나아가지 못할 때, 원인이 증명기(Prover)가 약해서인지, 추측기(Conjecturer)가 약해서인지 분리해서 진단하기가 어렵습니다. 이런 디버깅/분해(Disentanglement)는 아직 많은 연구자들이 고민하고 있는 문제입니다.

그럼에도 불구하고, 저는 형식 언어와 비형식 언어—서로 다른 추상화 레벨(Abstraction Level)—를 결합하면 추측을 위한 공간이 더 넓어진다고 봅니다.

Q. Lean은 기호 언어(Symbolic Language)죠. 이건 기호적 AI(Symbolic AI)의 귀환이라고 볼 수 있을까요?

좋은 질문이에요. 1980년대에도 형식 검증(Formal Verification)에 대한 기대가 있었지만, 그때는 LLM이 없었죠. 지금은 상황이 다릅니다.

LLM은 비형식적 추론(Informal Reasoning), 즉 고수준 직관(High-level Intuition)을 다루는 데 강합니다. 증명 전체를 완벽히 쓰진 못하더라도, “이런 방향의 스케치(Sketch)가 가능하다”는 초안을 꽤 그럴듯하게 만들죠. 동시에 프로그래밍 언어(Programming Language) 세계에서는 코드 생성(Code Generation)이 눈에 띄게 좋아졌고요. 거기에 Lean이 있습니다.

이 세 가지가 합쳐지면서, 형식 검증(Formal Verification)과 비형식 추론(Informal Reasoner)을 결합한 하이브리드(Hybrid) 방식으로 AI 수학자를 만들기에 지금이 좋은 타이밍이라고 봅니다. 저희는 AlphaProof처럼 순수 형식(Purely Formal)만으로 가는 것도 아니고, 그렇다고 OpenAI 같은 LLM 회사처럼 “그냥 LLM 하나로” 가는 것도 아닙니다. 서로 다른 강점을 결합하는 접근입니다.

Q. Axiom이 런칭한 시기가 Periodic Labs와 거의 겹쳤죠. 두 회사 모두 “이걸 진짜 해내겠다고?” 싶은 문제를 다룹니다. 과학/수학을 위한 전문 모델(Specialist Scientific Models), 이게 대세의 흐름일까요? 아니면 거대한 멀티모달(Multi-modal) 모델이 결국 다 흡수할까요?

재미있는 질문이에요. Periodic의 공동창업자 리암(Liam)은 저도 잘 알고, 친구이기도 합니다. Periodic이 하는 일도 정말 기대하고 있어요.

Periodic과 Axiom은 비슷한 철학을 공유합니다. 기초 과학(Fundamental Science)과 기초 수학(Fundamental Math) 발견이 결국 세상을 바꾼다는 믿음이죠.

과거에는 기초 과학이 종종 “상업적 파급이 너무 느리다”는 이유로 과소평가됐습니다. 어떤 돌파구(Breakthrough)는 경제에 영향을 주기까지 100년이 걸릴 수도 있으니까요. 그런데 지금은 AI가 그 타임라인을 압축(Compress)하고 있습니다. 게다가 과거에는 아이디어가 좁은 학문 공동체에 갇혀 인접 분야로 잘 확산되지 못하기도 했죠.

예를 들어 예전의 수학자—하디(Hardy)처럼—는 케임브리지에 머물며 리틀우드(Littlewood)와만 일하고, 물리학자나 생물학자와 교류하지 않을 가능성이 큽니다. 그래서 탑티어의 수학적인 통찰이 학계의 상아탑 안에서, 심지어 수학자들 사이에서도 충분히 연결되지 못한 채로 제한됐던 거죠.

저희는 수학을 위한 AI(AI for Math)를 과학을 위한 AI(AI for Science)의 ‘알고리즘적 기둥(Algorithmic Pillar)’으로 봅니다. 이론적 돌파구를 만들고, Periodic 같은 팀이 그걸 실험 환경(Empirical Environment)에서 검증하고, 다시 현실 데이터로 피드백을 주는 사이클이 가능해지죠. 저는 그 순환이 앞으로 매우 흥미로운 방향이라고 봅니다.

Q. 그렇다면 당신이 만들려는 AI 수학자는 어떻게 평가하고 벤치마크(Benchmark)하나요? 사람들은 IMO에 열광하지만, 그건 당신의 목표와는 다르지 않나요?

저는 토마스 울프(Thomas Wolf)의 “AI Einstein”이라는 글을 모두에게 추천하고 싶어요. 정말 좋은 글이예요.

그 글의 핵심은, 연구와 발견(Discovery)은 학교 시험이나 경시대회보다 훨씬 긴 사이클을 갖고, 요구되는 능력도 다르다는 점입니다. 물론 근성(Grit)과 회복력(Resilience) 같은 성격도 필요하지만, 스킬 자체가 달라요. 여러 분야를 연결하는 능력, 넓게 생각하는 능력, 그리고 “아깝게 실패한 시도(Close Misses)”를 분석하는 능력이죠. 될 것 같았던 아이디어가 실패했을 때, 그걸 조금 비틀어(Perturb) 다른 유용한 방향으로 전환하는 능력이 중요합니다.

흥미롭게도 저는 그 글에서 묘사한 유형 중에, IMO 상위권 학생과는 다른 쪽에 더 가까워요. 저는 AMC나 AIME 정도는 했지만 IMO급은 아니었습니다. 대신 연구 수학자로서는 꽤 괜찮았다고 생각해요. 그만큼 요구 역량이 다르다는 뜻입니다.

AI ‘연구 수학자’를 만들려면, 이론 구축(Theory Building) 능력이 중요합니다. 라이브러리 학습(Library Learning)—앞으로의 보조정리(lemma)와 정리(theorem)를 세우는 데 도움이 되는 새로운 개념을 도입하는 능력—도 중요하죠.

이론 구축은 고립된 문제 하나를 푸는 게 아니라, 큰 그래프(Big Graph)에서 문제를 하나의 노드(Node)로 다루는 장기 맥락(Long-Context) 추론에 가깝습니다. 그리고 맞아요, 이런 능력을 측정할 벤치마크가 부족합니다. 정말로요.

고등학교 올림피아드 수준은 벤치마크가 많습니다. miniF2F도 있고, IMO 시험을 모델에게 치르게 할 수도 있고, 각국 문제를 스크랩할 수도 있죠.

하지만 박사과정 자격시험(PhD Qualifying Exam)급으로 가면 비용이 확 뛰어요. IMO 문제 하나의 ‘검증된 풀이(Proven Solution)’를 만드는 데 200~300달러가 든다면, 박사 자격시험급은 1,000달러 수준이 될 수 있습니다. 대략 4배죠.

또 ‘취향(Taste)’ 문제가 생깁니다. 어떤 커리큘럼으로 벤치마크를 구성할 것인가? 진지한 수학 능력을 측정하는 벤치마킹(Benchmarking)은 Axiom이 커뮤니티의 리더가 되고 싶어하는 영역입니다. 우리는 “대회에서 이긴다”를 넘어, 연구를 할 수 있는 AI 수학자를 보고 싶습니다.

Q. 독자의 입장에서, 오늘 당장 해볼 수 있는 걸 하나라도 가져가고 싶어요. Axiom Math와 연결해서 개인이 지금 할 수 있는 건 뭘까요?

크게 두 가지 방향이 있습니다. 개인 대상부터 말해볼게요.

Lean이 처음이라면, “Natural Number Game”이라는 훌륭한 입문 게임이 있어요. 듀오링고(Duolingo)처럼 Lean을 훈련 문제로 익히게 해줍니다.

Lean을 어느 정도 안다면, 좋아하는 수학 결과를 하나 골라 직접 형식화(Formalize)해보는 걸 추천합니다. Mathlib는 대수(Algebra)나 해석(Analysis)은 꽤 잘 커버하지만, 기하(Geometry), 위상수학(Topology), 편미분방정식(Partial Differential Equations) 같은 분야는 아직 비어 있는 구간이 많거든요.

예를 들어 저차원 위상수학(Low-dimensional Topology)의 결과를 형식화하다 보면, 다른 사람들이 이후에 쓰게 될 중요한 의존성(Dependency)을 쌓게 될 수도 있습니다.

기업(Enterprise) 쪽으로는, 대형언어모델(LLM)과 형식 검증(Formal Verification)의 결합—둘의 교집합(intersection)—이 앞으로 몇 년간 굉장히 유망하다고 봅니다.

규제 산업(Regulated Industries)의 대기업은 컴플라이언스(Compliance)를 위해 형식 검증이 필요한 경우가 많습니다. Amazon이나 AWS처럼 자체적인 신경-기호(Neurosymbolic) 추론에 관심을 보이는 곳들이 이 기술을 주목하는 이유죠.

또 형식 수학 증명(Formal Math Proving)과 자동 형식화(Auto-Formalization)가 예상 밖의 영역에도 적용될 수 있다는 걸 종종 봅니다. 그런 시너지가 있다고 느끼는 분들과는 언제든 이야기해보고 싶어요.

소프트웨어/하드웨어 형식 검증(Formal Verification for Software & Hardware)은 특히 전략적인 영역이 될 겁니다. 레거시 코드(Legacy Code)를 교체하거나 업그레이드할 때, 중요한 비즈니스 엣지케이스(edge case)를 놓치지 않았는지 보장하고 싶다면, 이런 방식이 큰 도움이 될 수 있어요. 하드웨어 회로(circuit) 속성 테스트나 설계 검증도 마찬가지입니다.

한편 수학적 발견(Mathematical Discovery) 쪽은 Lean이 꼭 필요하진 않습니다. 깊은 오픈 문제(Open Problems)와 연결되는 흥미로운 구성/예시/수학적 대상을 생성하는 실천(Practice)에 가깝죠. 그래프(Graph)처럼 현실 문제—물류나 라우팅(Routing)—와도 깊이 닿아 있는 주제라면 더더욱요.

이건 “새 시장을 열자”라기보다, 기존 시장에서 LLM-보조 형식 추론(LLM-assistive Formal Reasoning)의 파워를 스케일업해서 성능을 끌어올리고, 그걸로 경쟁 우위를 만드는 접근입니다. 그리고 그 다음 단계에서 새로운 유즈케이스가 열릴 겁니다.

Q. 이 모든 걸 해내는 데 가장 큰 병목은 무엇인가요? 그리고 어떻게 풀 건가요?

병목은 몇 가지가 있는데, 첫 번째는 데이터 희소성(Data Scarcity)입니다. 파이썬(Python) 코드는 1조 토큰(trillion tokens) 이상이 있는데, Lean 코드는 아마 1천만 토큰(10 million tokens) 정도일 겁니다. 데이터 격차가 10만 배(100,000x)죠.

이 격차는 자동 형식화(Auto-Formalization) 문제로 이어집니다. 자연어 수학을 Lean으로 바꾸는 작업은 단순 번역이라고 부르기 어려울 정도로 기술적으로 까다롭습니다. 그런데 모델은 Lean을 거의 보지 못했으니 당연히 어렵죠. 거의 콜드 스타트(Cold Start) 문제고, 닭이 먼저냐 달걀이 먼저냐 하는 생각을 하게 되죠.

저희는 Lean 전문가를 고용해서 전부 수작업으로 증명을 코딩하게 만들고 싶진 않습니다. 그건 확장성이 낮거든요. 그래서 이 문제를 어떻게 ‘스케일할 수 있는 방식으로’ 풀지가 핵심입니다.

Axiom은 AI, 프로그래밍 언어(Programming Languages), 수학(Math)이라는 세 축을 기반으로 움직입니다. 응용 AI(Applied AI) 인력, 컴파일러/언어(Compiler/PL) 인력, 그리고 비형식 수학자와 Mathlib 구축을 이끌어온 형식 수학자까지—이 어려운 산을 함께 오를 팀 구성이 중요하죠.

데이터 희소성 외에도, 추측과 직관(Intuition) 자체가 엄청나게 어렵습니다. 좋은 실험 설계(Experiment Design)가 필요하고요. 스타트업 환경에서는 제한된 리소스로 여러 방향을 동시에 가속해야 하니, 이건 정말 야심차고 도전적인 문제입니다.

Q. AGI 얘기로 돌아가볼게요. AGI와 초지능(Superintelligence)을 어떻게 구분하나요? 형식 추론(Formal Reasoning)은 AGI에 필수라고 보나요?

저는 AGI보다 초지능(Superintelligence)이라는 단어를 더 좋아합니다. AGI는 의미가 너무 모호하거든요.

Q. 차이를 잘 모르겠어요. 비슷해 보이는데요.

저는 초지능을 도메인-특화(Domain-Specific)로 정의할 수 있다고 봅니다. 예를 들어 초지능 AI 수학자는 가능하지만, 그 모델이 빨래를 최고의 효율로 개는 능력까지 가질 필요는 없죠. 그래서 완전히 ‘일반’이라고 보긴 어렵습니다.

AGI를 저는 이런 이미지로 상상해요. 문제의 세계를 접시(Plate)라고 하면, 중앙에는 쉬운 문제들이 있고(1+1=2, “Hello World” 출력 같은), 가장자리에는 서로 다른 목표들이 흩어져 있습니다. 암을 치료하는 것, 리만 가설을 푸는 것, 노벨문학상 급 소설을 쓰는 것, 물리적 지능(Physical Intelligence)의 궁극 문제 같은 것들이요.

AGI라는 개념은, 중앙에서부터 해결 가능한 영역을 점점 확장해 결국 접시의 가장자리까지 넓혀가는 느낌입니다. 즉 “셰익스피어급 문학도 쓰고, 리만 가설도 풀고, 암도 치료한다”는 시스템에 베팅하는 거죠.

반면 제가 말하는 초지능은, 목표점을 하나 찍고 그 지점으로 곧장 가는 겁니다. Axiom은 그 방식으로, 초지능 AI 수학자를 만들겠다고 베팅합니다. 하지만 제 모델이 시(Poetry)를 잘 쓸 거라고는 기대하지 않아요. 오히려 못 쓸 수도 있죠. 그게 차이입니다.

Q. 결국 Periodic Labs와 Axiom 모두 특정한 모델에 베팅한다는 이야기네요.

맞습니다. 저는 특정 모델(Specific Model)에 베팅합니다. 그리고 수학을 위한 AI(AI for Math)가 과학을 위한 AI(AI for Science)의 알고리즘적 기둥(Algorithmic Pillar), 즉 추론 플랫폼(Reasoning Platform)이 될 거라고 믿습니다.

Axiom과 Periodic이 하는 일은 정말 중요하고, 저는 그게 다음 프런티어라고 봅니다. AI for Math, AI for Science요.

Q. 마지막 질문입니다. 지금의 당신을 만드는데 큰 영향, 또는 최근에 영향을 준 책이 있다면요?

저는 수학책을 너무 많이 읽었을지도 몰라요 ^.^. 수학책과 나머지 책으로 나눠서 답해볼게요.

수학 쪽에서는 대수기하(Algebraic Geometry) 교과서가 떠오르네요. 하츠혼(Hartshorne)을 쓰는 사람도 있고, 라비 바킬(Ravi Vakil)의 The Rising Sea를 쓰는 사람도 있죠. 저는 하츠혼을 이해할 만큼 똑똑하지 않아서(웃음) The Rising Sea를 봤는데, 예시가 훨씬 풍부합니다.

이 책은 ‘이론 구축(Theory Building)’이 무엇인지 이해하게 해줬어요. 스킴(Scheme) 개념을 도입하면, 그로텐디크(Grothendieck)가 말한 시야 전환이 확 느껴집니다. 대수기하는 ‘문제 풀이’가 아니라 ‘이론 구축’의 좋은 사례라고 생각해요.

반면 해석적 정수론(Analytic Number Theory)의 대번포트(Davenport) 같은 책은 문제 해결에 유용한 트릭을 많이 제공합니다. 경계(Bound)를 세우는 법, 코시-슈바르츠(Cauchy-Schwarz) 같은 부등식(Inequality) 기반 논증들이요. 그 분야에서는 부등식을 보면 거의 반사적으로 떠오를 정도로요. 그런 면에서 수학을 바둑이나 체스처럼 ‘유한 탐색 공간(Finite Search Space)’이 있는 것으로 느끼게 만들기도 합니다.

어릴 때는 Proofs from THE BOOK을 정말 좋아했어요. “신에게 최고의 수학 증명이 담긴 책이 있다”는 에르되시(Erdős)의 말이 있죠. 저에게는 그게 거의 영적인(Spiritual) 경험이었습니다.

수학자는 진리를 찾는 사람이자, 어떤 면에서는 사자(Messenger) 같다고 느낍니다. 사다리를 타고 올라가 가장 달콤한 사과를 따서 사람들에게 나눠주는 존재요. 그리고 이런 이론적 진리가 결국 현실을 떠받치죠. 정수론의 돌파구가 암호학(Cryptography)으로 이어진 것처럼요.

하디(Hardy)는 A Mathematician’s Apology에서 “내 수학은 쓸모없다”고(약간 반어법을 섞어서) 말하죠. 그런데 전쟁에서 꽤 유용해졌습니다. 그게 참 흥미로워요.

비수학 쪽으로는 인문/사회과학을 좋아합니다. 저는 로스쿨을 2년 다니다가 이 길로 뛰어들었거든요.

Q. 그래서 토마스 울프를 좋아하나 봐요.

네, 저는 법과 경제(Law and Economics)를 좋아합니다. 안드레이 슐라이퍼(Andrei Shleifer)의 연구는 정말 훌륭했고, 스탠퍼드 로스쿨에서 그의 세미나를 들은 것도 좋은 경험이었어요. 특정 법과 정책이 억지(Deterrence)와 응보(Retribution)에 어떤 영향을 주는지, 그걸 수학적으로 모델링하는 건 정말 매혹적이거든요

문학으로는 Old Tales of Dayaobao라는 책이 있어요. 베이징의 한 후퉁(Hutong) 단지에서 살던 중국 작가/예술가 세대를 다루는데, 르네상스 시기의 프랑스 살롱(Salon)처럼 서로 아이디어를 주고받는 분위기가 있습니다. 건축가가 던진 말이 예술가에게 영향을 주는 식으로, 분야를 가로지르는 연결이 일어나죠.

그 대화 속에는 장인정신(Craftsmanship)이 흐르고, 문화대혁명(Cultural Revolution)의 고통도 함께 담겨 있습니다. 이 책이 저로 하여금 “예술적 표현”을 더 지향하게 만들었고, 수학과 직관이 과학보다 예술에 더 가깝다는 생각을 더 강하게 하게끔 해 주기도 했어요.

Q. 그렇다면, 인간 수학자의 관점에서, AI를 활용해서 ‘누구나 해볼 수 있는’ 수학적 발견 방법을 하나 제안해준다면요?

수학적 발견을 위한 코드베이스들이 있어요. 다만 이걸 다루는 방식은 “LLM에 프롬프트를 던지고 끝”이 아닙니다. 이런 툴킷을 만드는 사람들과 함께, 진지한 오픈 문제를 놓고 깊게 상호작용하는 방식에 가깝습니다.

제가 강조하고 싶은 두 프로젝트는 Pattern Boost와 End-to-End입니다. 둘 다 제 동료 프랑수아의 작업인데요. Pattern Boost는 흥미로운 예시를 생성하는 생성적 방법(Generative Method)이고, End-to-End는 문제를 해답으로 옮기는 번역적(Translative) 방법입니다.

예시가 대량으로 생성되면, 수학자는 그걸 보며 이전엔 몰랐던 믿음(Belief)이나 직관을 얻게 될 수 있어요. 그래서 저는 사람들이 “그 판에 들어와서” 직접 부딪혀보길 권합니다.

AI for Math 컨퍼런스도 연중 열립니다. Oberwolfach부터, 다음은 아마 JMM일 것이고, 그 다음엔 Aarhus가 있는데 Axiom이 공동 주최하기도 합니다.

프런티어 AI for Math discovery를 하는 사람들과 이야기해보면, 예전에는 도저히 손에 잡히지 않던 문제들이 갑자기 ‘가능성 있는 거리’로 다가오는 경험을 하게 될 겁니다.

Q. 오늘 말씀 감사합니다.

감사합니다.

읽어주셔서 감사합니다. 친구와 동료 분들에게도 뉴스레터 추천해 주세요!