Axiom Math CEO 카리나 홍: 6,400만 달러 규모의 수학적 추론 AI 프로젝트

섹션별 상세

00:00

Axiom Math의 미션과 자가 개선 엔진

Axiom Math는 생성(Generation)과 검증(Verification)을 결합하여 스스로 성능을 개선하는 추론 엔진을 구축하는 것을 목표로 합니다. 수학은 정답이 명확하고 논리적 단계가 엄밀하기 때문에 이러한 자가 학습 루프를 테스트하기에 최적의 환경입니다. 카리나 홍은 현재 AI 지형에서 간과되고 있는 검증 구성 요소의 중요성을 강조하며, 이를 통해 신뢰할 수 있는 AI 수학자를 만들고자 합니다.

00:13

Putnam 수학 경시 대회에서의 성과

Axiom의 시스템은 대학생 대상의 고난도 수학 경시 대회인 Putnam 시험에서 놀라운 성과를 거두었습니다. 12문제 중 8문제를 해결하며 인간 참가자 중 상위권에 해당하는 점수를 기록했습니다. 이는 결정론적 도구(Deterministic Tooling)와 확률적 시스템(Probabilistic System)이 협력했을 때 발생하는 강력한 시너지를 증명하는 사례입니다. 카리나 홍은 시스템의 최종 점수가 인간 최고 득점자들과 경쟁할 수 있는 수준임을 시사했습니다.

06:33

LLM의 한계와 정형 언어 Lean의 도입

기존의 대규모 언어 모델(LLM)은 수학적 추론에서 종종 오류를 범하거나 논리적 비약을 보입니다. Axiom은 이를 해결하기 위해 수학적 증명을 정밀하게 기술할 수 있는 정형 언어인 Lean을 도입하여 자연어 추론을 보완합니다. Lean을 통해 AI가 생성한 논리를 엄격하게 검증함으로써 환각 현상을 방지하고 추론의 정확성을 보장합니다. 이러한 방식은 안전이 중요한 코드 작성이나 공학 설계 분야에도 적용될 수 있는 잠재력을 가집니다.

03:00

지식 베이스와 자동 정형화 시스템

Axiom의 시스템은 증명기(Prover), 가설 생성기(Conjecturer), 그리고 지식 베이스(Knowledge Base)의 세 가지 핵심 요소로 구성됩니다. 증명기는 정리를 증명하고, 가설 생성기는 흥미로운 가설을 제안하며, 지식 베이스는 이미 증명된 내용을 저장하여 추론에 활용합니다. 또한 자연어로 된 수학 문제를 정형 언어로 자동 변환하는 자동 정형화(Auto-formalization) 기술이 이 모든 과정을 연결하는 중요한 역할을 수행합니다.

00:52

수학의 미래와 인간 수학자의 역할 변화

AI 수학자의 등장은 인간 수학자의 역할을 없애는 것이 아니라 더 높은 수준의 추상화 작업으로 이동시킬 것입니다. 인간은 직관을 발휘하여 새로운 방향을 제시하고, AI는 대학원생처럼 세부적인 증명 과정을 엄밀하게 수행하는 파트너가 될 것입니다. 카리나 홍은 수학자들이 이제 계산이나 단순 증명보다는 문제의 본질을 정의하고 창의적인 가설을 세우는 데 더 집중하게 될 것이라고 전망합니다.

주목할 인용

“Axiom's mission is to build a reasoning engine that is self-improving and that combines generation and verification.”
Carina Hong·00:00
회사의 설립 목적과 기술적 지향점을 설명하며

“Math is a really good testing ground for this sort of self-loop.”
Carina Hong·00:05
왜 다른 분야보다 수학에서 먼저 추론 엔진을 개발하는지 이유를 밝히며

“Mathematicians will learn to work on a different abstraction than they are used to before.”
Carina Hong·00:54
AI가 수학 연구에 도입된 이후의 미래 변화를 예측하며