핵심 요약

  • Axiom은 수학 증명을 기계가 확인할 수 있는 코드로 바꾸는 형식 수학 추론을 개발한다. 카리나 홍 창업자는 이 기술을 AI가 코드를 생성하면서 정확성을 확인하는 데 활용하려 한다.
  • 홍은 수학 증명을 위해 만든 기술을 소프트웨어·하드웨어 검증에도 재사용할 수 있다고 본다. 과학 연구로 확장하는 구상도 제시했다.
  • 데이터부터 모델 학습, 실행 환경까지 직접 구축하되 다른 회사가 더 잘하는 부분은 받아들인다. 자체 합성 데이터를 만드는 능력은 핵심으로 지킨다.
  • 두 번째 투자 유치에서는 기술 성과와 투자자의 선제 제안이 협상 조건을 바꿨다. 첫 투자 유치가 어려웠던 경험을 모든 단계에 일반화하지 않았다.
  • 연구 조직을 키우려면 큰 목표를 세우는 사람과 실행 위험을 찾아내는 사람이 모두 필요하다. 창업자의 감정 관리와 명시적인 감사 표현도 조직 운영의 일부였다.

수학 증명에서 AI 코드 검증으로

스탠퍼드 공대 기술벤처 프로그램이 운영하는 기업가정신 강연에서 Axiom 창업자 겸 CEO 카리나 홍(Car​ina Hong)은 진행자·학생들과 수학 AI의 사업 가능성과 연구 조직을 만드는 경험을 나눴다. 대화의 중심은 수학을 푸는 AI가 어떻게 신뢰할 수 있는 코드 생성으로 이어질 수 있느냐는 문제였다.

Axiom이 개발하는 형식 수학 추론은 수학을 기계가 확인할 수 있는 코드로 바꾸는 기술이다. 홍은 AI가 만들어 내는 결과물이 늘어나는 데 비해 그 결과가 맞는지 확인하는 검증 기반은 부족하다고 봤다.

그는 강연 전날 유한 단순군 분류 증명의 형식화를 발표했다고 밝혔다. 여러 논문과 책에 흩어진 1만 5,000쪽 이상의 수학을 다루는 작업으로, 증명 언어 Lean으로 작성한 코드가 5,000만 줄 이상 나왔다고 설명했다. 한 사람이 전체를 읽기 어려운 거대한 증명을 컴퓨터가 확인할 수 있게 바꾸려는 시도였다.

이때 검증의 신뢰는 작은 핵심 프로그램에 달려 있다. 홍도 이를 어떤 전제도 필요 없는 절대적 확실성으로 설명하지는 않았다. 방대한 증명을 확인하는 문제를 신뢰해야 할 작은 검증 핵심으로 줄인다는 데 의미를 뒀다.

홍이 사업적으로 더 큰 관심을 두는 일은 기존 코드의 오류를 찾는 데서 끝나지 않는다. 새 코드를 생성하는 순간 검증 결과를 돌려받는 과정이 핵심이다. 홍은 테스트를 거친 소프트웨어에도 오류가 생기고 일부 AI 중심 조직에서는 코드 검토까지 생략한다며 생성 속도에 맞는 검증 방식이 필요하다고 말했다.

그가 꼽은 가치는 검증을 동반한 코드 생성과 기존 코드 검증, 신뢰성 문제로 AI 도입을 주저하는 중요 산업의 활용을 돕는 일이다. 자율적으로 장기 연구를 수행하는 에이전트를 재료·분자 등 과학 분야로 확장하는 구상도 제시했다. 중요 산업의 활용과 과학 분야로의 확장은 이 기술로 가능해질 수 있다고 봤다.

직접 만드는 기술과 받아들이는 기술

홍은 수학을 해결하면 모든 것을 해결한다는 초기 생각에서 출발했지만 실제로는 세부 구현이 중요했다고 돌아봤다. 현재는 수학 증명을 위해 구축한 기술 전반을 소프트웨어와 하드웨어 검증에도 재사용한다고 더 구체적으로 설명했다.

Axiom은 데이터 전략, 모델의 중간·후속 학습, 모델이 도구를 쓰고 작업을 수행하는 실행 환경, 기반 시설과 버전 관리까지 폭넓게 직접 만든다. 다만 기초 모델의 사전학습은 하지 않는다고 밝혔다.

그렇다고 모든 부분을 끝까지 자체 기술로 고수하지는 않는다. 홍은 일부 영역에서는 다른 조직이 앞설 수 있고 그때는 외부 기술을 쓸 수 있어야 한다고 말했다. 폭넓게 개발하면서도 경쟁사의 발전을 방어적으로 받아들이지 않는 태도가 필요하다고 봤다.

데이터는 강하게 지키는 영역이다. 홍은 스스로 개선하는 능력이 합성 데이터를 생성하는 능력에서 나온다고 봤다. 데이터와 성능 평가 기준이 모델을 규정한다는 생각도 밝혔다.

에이전트 구조를 보는 전망도 이와 맞닿아 있다. 사람이 고정해 둔 실행 절차가 여러 전문 모델을 호출하는 방식보다 학습된 조정 모델이 도구나 자기 자신을 호출하는 방식에 무게를 뒀다. 여러 에이전트가 함께 작업하는 방식은 Axiom의 성과에 중요했으며 앞으로는 그 비용을 줄이는 일이 과제라고 했다. 이를 위해 성능 좋은 소형 모델도 필요하다고 봤다.

목표는 멀리 잡고 실행 위험은 가까이 본다

AI가 빠르게 발전하는 환경에서 홍은 다음 분기에만 야심적인 목표를 잡으면 늦는다고 말했다. 연간 목표부터 충분히 높게 잡아야 기술 발전 속도를 따라갈 수 있다고 봤다.

사례로는 소수 사이의 간격에 관한 수학 결과를 형식화하는 작업을 들었다. 일정한 유한 간격 안에 놓인 소수 쌍이 무한히 존재한다는 결과다. Axiom이 간격 246에 관한 기존 결과를 형식화하려 했을 때 사내 다수는 작업량이 너무 커서 목표로 삼기 어렵다고 봤다. 하지만 실제로 그 작업을 다룰 무렵에는 팀이 해낼 수 있다는 인식이 자연스러워졌다고 회고했다.

큰 목표만 강조한 것은 아니다. 홍은 야심적인 목표를 세우는 사람과 실행 위험을 잘 찾아내는 사람이 좀처럼 겹치지 않는다고 말했다. 위험을 지적하는 사람은 반대만 하는 것처럼 보일 수 있지만 실제로는 조직이 들어야 할 문제를 짚고 있을 수 있다.

여러 기술을 직접 개발하는 전략에도 집중할 때가 있다. 유한 단순군 분류 증명을 다룰 때는 모두가 그 작업에 집중했다고 했다. 개발 범위를 넓게 가져가면서도 당장 완수할 과제에는 조직의 힘을 모아야 했다.

투자 유치를 바꾼 것은 성과와 협상 위치였다

진행자는 Axiom이 6개월 안에 두 차례 투자 유치로 2억 6,000만 달러를 확보했다고 소개했다. 홍은 첫 투자 유치는 아이디어를 설명하는 단계라 매우 어려웠지만 두 번째는 회사가 쌓은 기술 성과를 보여 줄 수 있었다고 말했다.

그중 하나는 수학 증명 모델이 다른 소프트웨어 검증 평가에서도 높은 성능을 보인 경험이었다. 수학을 위해 만든 기술이 다른 검증 문제로 옮겨 갈 수 있다는 신호였다.

협상 상황도 달랐다. 두 번째 투자 유치 당시에는 앞서 조달한 자금을 많이 쓰지 않았고 당장 추가 투자가 필요하지 않았다. 투자자들이 먼저 연락했고 일부는 투자 조건을 담은 텀시트를 보냈다. 이미 검토하고 싶은 제안이 있었기 때문에 다른 투자자와의 논의에도 기한을 둘 수 있었다.

홍은 중요한 기술 성과를 앞두고 먼저 들어온 관심에는 곧바로 응하지 않으려 했다고 말했다. 투자 유치는 주의를 분산시키고 성과를 낸 뒤에는 더 많은 관심을 받을 수 있다고 봤기 때문이다. 회사 구축에 집중하자 투자 유치가 쉬워졌다는 회고에는 이런 자금 여력과 성과, 선제 제안이라는 조건이 함께 있었다.

첫 투자 유치에서 얻은 교훈은 특정 투자자의 거절을 회사 전체의 실패로 받아들이지 않는 것이었다. 좋은 투자사는 여럿이라는 사실을 받아들이자 스트레스가 줄었고 회사의 가치를 더 자연스럽게 자신할 수 있었다고 말했다.

연구 조직이 성장하면서 사람을 대하는 방식도 바뀌었다

Axiom의 인원은 강연에서 언급한 1월의 15명 미만에서 10월 약 80명으로 늘었다. 홍은 연구 중심 AI 기업에서 뛰어난 인재가 얼마나 모여 있느냐가 사업을 좌우한다고 봤고 CEO의 일상도 사람과 기술 조직을 관리하는 쪽으로 바뀌었다고 말했다.

채용에서는 각 사람이 무엇에 동기를 느끼는지 이해하는 일을 강조했다. 첫 투자 유치 과정에서 합류한 CTO는 AI 생성 테스트와 대규모 학습에 관심이 있었고 이 관심이 Axiom의 기술 문제와 맞았다고 설명했다. 이후 사람을 붙잡아 두는 데는 적극적이고 솔직한 소통이 중요했다.

홍은 창업자 자신의 상태가 팀에 전달된다는 운영 원칙을 뒤늦게 배웠다고 했다. 자신이 소진되면 팀도 영향을 받았고 문제를 하나씩 해결하는 것만큼 휴식과 차분한 판단이 중요했다.

감정과 감사를 말로 표현하는 일도 배웠다. 유한 단순군 분류 증명 발표 직전에는 외부에서도 독립적으로 검증할 수 있게 준비하느라 팀원 상당수가 밤을 새웠다. 홍은 음식을 사 주는 방식으로 고마움을 표현했지만 직접 말해 주는 데는 서툴렀다고 돌아봤다. 특히 떨어져 일할 때는 구성원이 자신의 노력을 알아준다고 느끼게 하는 표현이 필요했다.

일하는 방식의 차이도 허용하게 됐다. 자신은 한 문제에 집중하는 편이라 다른 사람도 그러길 바랐지만 여러 일을 동시에 맡을 때 더 잘하는 사람도 있었다. 홍은 이를 허용하면서 조직을 위에서 지시하는 방식에서 구성원의 제안을 더 받아들이는 방향으로 바꿨다고 말했다.

수학자의 미래도 기술 발전의 조건에 달려 있다

학생들은 AI가 수학을 발전시키면 인간 수학자에게 어떤 일이 남는지도 물었다. 홍은 수학을 과학·기술에 쓰이는 고유한 가치가 있는 활동으로 보는지, 체스처럼 즐거움 자체에 의미를 두는 활동으로 보는지에 따라 답이 달라진다고 말했다. 자신은 전자에 더 가깝게 본다고 밝혔다.

그는 AI 발전이 계속된다면 기존 문제를 푸는 데 그치지 않고 추측과 이론, 분야의 방향을 바꾸는 아이디어까지 만들 수 있다고 봤다. 이 경우 인간만이 새로운 발상을 한다는 이유만으로 역할을 설명하기는 어렵다.

대신 수학을 업무의 중요한 일부로 쓰는 사람이 늘고 수학자의 작업 방식도 개발자와 비슷해질 수 있다고 전망했다. 수집한 데이터를 설명할 이론과 데이터·코드에서 무엇을 증명해야 하는지 정하는 능력도 필요해질 것이라고 말했다. 이런 전망에는 AI 발전이 지속된다는 조건이 붙는다. 자본시장이 위축돼 AI 발전이 둔화되는 동시에 인간의 수학 이해에 대한 관심도 줄어드는 상황을 그는 더 나쁜 경우로 봤다.

홍은 수학 문제를 많이 푸는 AI 자체보다 그 과정에서 쌓은 검증 기술을 코드와 연구에 다시 쓰는 데 연결 고리를 뒀다. Axiom의 조직 운영에서도 같은 긴장이 드러났다. 목표는 크게 잡되 실행 위험을 듣고 기술은 넓게 만들되 더 나은 외부 성과를 받아들이는 방식이다.