AI가 코드를 작성하는 시대가 왔다. 하지만 그 코드를 믿을 수 있는가 — 이 질문에 답하려는 스타트업이 있다.

액시엄 매스(Axiom Math)는 AI가 생성한 코드의 정확성과 안전성을 수학적으로 검증하는 회사다. 2025년 7월 조용히 문을 연 이 회사가 창업 7개월 만에 멘로 벤처스(Menlo Ventures) 주도로 2억 달러 시리즈A를 유치했다. 기존 투자사인 마드로나(Madrona), 그레이크로프트(Greycroft), 비캐피탈(B Capital), 토요타 벤처스(Toyota Ventures)도 모두 추가 투자에 참여했다. 투자 후 기업가치는 16억 달러다.

오늘날 AI 코딩 도구들은 인상적인 속도로 코드를 쏟아낸다. 하지만 구조적 한계가 있다. AI는 확률적으로 그럴싸한 코드를 만들 뿐, 그 코드가 실제로 올바르다는 것을 보장하지 않는다. 버퍼 오버플로우, 엣지 케이스 오류, 숨겨진 보안 취약점은 테스트를 통과하고도 살아남는다. 금융 시스템이나 항공 소프트웨어처럼 오류 허용치가 0에 수렴하는 분야에서는 ‘그럴싸한 코드’가 재앙의 씨앗이 될 수 있다.

액시엄은 이 문제를 근본부터 다르게 접근한다. 수학적 증명 전용 프로그래밍 언어 린(Lean)으로 출력을 생성하도록 AI를 훈련하는 방식이다. 린으로 작성된 출력은 기계적으로 검증 가능하고, 추론의 각 단계가 논리적으로 보장된다. AI가 잘못된 증명을 만들면 결정론적으로 오류가 잡힌다 — AI가 스스로 틀렸다는 걸 알 수 있는 구조다. 이것이 액시엄이 내세우는 ‘검증된 AI(Verified AI)’다. 환각이 없고, 출력의 안전성을 수학적으로 증명한다.

98년 만에 여섯 번째 퍼트넘 만점

액시엄의 성과 자체가 이 기술의 가능성을 증명한다. 지난 2025년 12월, 액시엄의 AI 추론 엔진 ‘액시엄프루버(AxiomProver)’는 퍼트넘 수학대회(Putnam Competition)에서 12문제를 전부 완벽하게 풀어냈다. 퍼트넘은 북미 대학생 수학 최고 권위 대회로, 15만 번 이상의 도전 중 98년 역사에서 완벽한 만점을 받은 인간은 단 다섯 명이다. 중간값은 0점이다. 2025년에 만점을 달성한 AI는 액시엄뿐이었다.

여기서 끝이 아니었다. 같은 AI 시스템이 수정 없이, 케 오노(Ken Ono) 교수조차 풀지 못했던 20년 된 미해결 정수론 추측을 자동으로 증명해냈다. 그 케 오노 교수는 지금 액시엄의 창립 수학자(Founding Mathematician)로 합류해 있다.

경쟁자들이 재현하기 어려운 구조적 강점도 있다. 액시엄은 인류가 쌓아온 모든 공식 검증 데이터보다 수십 배 많은 검증 데이터를 스스로 생성하고 있다. 결정론적 증명 검증기가 확인한 이 데이터는 바로 훈련에 다시 투입된다. 일반 LLM이 AI 생성 데이터를 훈련에 쓰면 모델이 붕괴하는 것과 정반대 구조다. 컴퓨팅 자원만 있으면 계속 자기개선이 가능한 루프가 만들어지는 셈이다.

스탠퍼드 박사과정 1년 만에 자퇴한 25세 창업자

회사를 이끄는 카리나 홍(Carina Hong) CEO는 올해 25세다. MIT에서 수학·물리학을 이중 전공하고 옥스퍼드에서 신경과학 석사(로즈 장학생)를 마쳤다. 스탠퍼드 법학-수학 박사 통합과정(나이트-헤네시 장학생)에 입학했다가 1년 만에 창업을 위해 자퇴했다. 9편의 동료 심사 논문을 발표했고 북미 학부생 수학 최고 영예상인 모건 프라이즈를 받았다. 멘로 벤처스의 매트 크래닝(Matt Kraning) 파트너는 20년 실리콘밸리 투자 이력에서 만난 가장 인상적인 창업자 중 하나라고 했다.

팀도 눈에 띈다. CTO 슈보 센굽타(Shubho Sengupta)는 전 페이스북 AI 리서치(FAIR) 디렉터로, 메타에서 수십억 달러 규모의 AI 슈퍼클러스터를 이끌고 엔비디아에서 GPU 라이브러리의 기반을 닦은 인물이다. 프랑수아 샤르통(François Charton)은 2019년 트랜스포머를 수학에 처음 적용해 AI-수학 분야 자체를 개척한 연구자로, 메타 AI에서 130년 된 수학 문제를 풀고 30년 된 추측을 반증한 뒤 합류했다. 케 오노는 구겐하임·슬론 펠로이자 세계 최고 수론학자 중 한 명으로, 버지니아대학교 부총장직과 종신교수직을 내려놓고 액시엄에 합류했다. 창립 7개월 만에 30명을 넘어선 팀이다.

목표 시장은 ‘AI가 쓰는 모든 코드’

멘로 벤처스는 이번 투자의 기준점을 기존 형식 검증 시장에 두지 않았다고 분명히 선을 그었다. 나사(NASA), AWS처럼 일부 미션 크리티컬 시스템에만 적용되던 전통적 형식 검증 시장은 규모가 작다. 박사급 전문가가 필요하고 코드 한 줄당 증명 20줄이 따라붙는 구조였기 때문이다. 액시엄이 이 과정을 자동화하면 방정식이 달라진다. 결과가 중요한 AI 생성 코드 한 줄 한 줄이 모두 잠재적 시장이 된다는 게 멘로의 시각이다.

이번 투자금은 검증 데이터 코퍼스 확장을 위한 훈련 인프라 스케일링, 기술 인력 채용, 초기 제품 출시에 쓰인다. 액시엄은 자사 린 엔진 ‘AXLE’의 공개 API를 2026년 3월 출시하기도 했다.

경쟁 구도: 수학적 검증 AI, 시장이 달아오른다

액시엄이 개척 중인 ‘AI 코드 검증’ 공간에는 이미 여러 플레이어가 각자의 각도로 진입하고 있다.

가장 직접적인 경쟁자는 하모닉(Harmonic)이다. 로빈후드(Robinhood) CEO 블라드 테네브(Vlad Tenev)가 공동 창업한 이 회사도 린4(Lean4)를 활용해 수학적 추론의 환각 문제를 해결한다. 지난 2025년 11월 리빗 캐피탈(Ribbit Capital) 주도로 시리즈C 1억 2천만 달러를 유치하며 기업가치 14억 5천만 달러를 기록했고, 누적 투자금은 2억 9천500만 달러다. 하모닉의 AI 모델 ‘아리스토텔레스(Aristotle)’는 2025년 국제수학올림피아드(IMO)에서 금메달 수준의 성적을 냈다.

방산 분야의 코드 검증이라는 각도에서 접근하는 회사도 있다. 와우테일이 지난 2월에 보도한 코드 메탈(Code Metal)이다. F-35 전투기 AI 시스템을 개발한 피터 모랄레스(Peter Morales)가 창업한 이 회사는 레거시 방산·반도체 코드를 다른 언어나 하드웨어 아키텍처로 변환할 때 수학적으로 동일한 동작을 보장하는 ‘뉴로-심볼릭’ 기술로 미 공군, L3해리스 등을 고객으로 확보했다. 지난 2월 세일즈포스 벤처스(Salesforce Ventures) 주도로 시리즈B 1억 2500만 달러를 조달하며 유니콘에 올랐다.

두 회사가 기술적으로 맞닿는 부분이 있지만 방향은 다르다. 코드 메탈이 기존 레거시 코드를 현대 언어로 ‘안전하게 옮기는’ 데 집중한다면, 액시엄은 AI가 처음부터 ‘틀림없는 코드’를 생성하도록 만드는 데 초점을 맞춘다. 미래의 소프트웨어 개발 전 과정에 검증 레이어를 심겠다는 더 넓은 그림이다.

액시엄은 시드 라운드 때 이미 하모닉 당시 기업가치를 넘어서는 3억 달러 평가를 받았고, 이번 시리즈A에서는 16억 달러로 치솟았다. 비캐피탈 주도로 6천400만 달러 시드를 조달한 지 5개월 만에 기업가치가 5배 이상 뛴 것이다. 퍼트넘 만점, 미해결 수론 증명이라는 기술적 성과가 시장에 강한 신호를 보낸 결과다.