AI2026. 11. 6. 오후 6:49 UTC·1 분 소요

Axiom Math, Stacks Project 형식 검증 완료 AI 슬롭 막는다

Axiom Math의 AI 에이전트가 수학 라이브러리 Stacks Project를 형식 검증했습니다. 검증된 토대로 AI 슬롭을 막겠다는 전략입니다.

Abstract illustration of mathematical formulas and lines of code representing formally verified proofs checked by AI agents. — 이미지: TechCrunch

기업가치 16억 달러의 스타트업 Axiom Math가 수요일 수학 라이브러리 Stacks Project를 AI 에이전트로 형식 검증했다고 발표했습니다. 사람이 쓴 가장 방대한 수학 자료 중 하나로 꼽히는 프로젝트입니다. 검증되지 않은 AI 증명이 쏟아지는 가운데, 검증된 토대를 세우겠다는 시도입니다.

7,654쪽을 1,600만 줄 코드로

Stacks Project는 2005년 컬럼비아대 수학자 Johan de Jong이 오픈소스 참고 자료로 시작했습니다. 대학 수준 대수학부터 대수, 기하, 수론의 최첨단 내용까지 담고 있습니다. 같은 대학의 Peter Woit은 “이에 견줄 만한 것이 정말 없다”고 평가했습니다.

Axiom의 AI 에이전트들은 약 7,654쪽 분량을 약 1,600만 줄의 컴퓨터 검증 코드로 옮겼습니다. 증명을 프로그래밍 언어 Lean으로 다시 쓰면 증명 보조기가 한 줄씩 검사하는 방식입니다. 정리와 정의가 서로 얽혀 있어 모든 연결을 유지하는 것이 관건이었다고 합니다.

팀은 에이전트에게 느슨한 위계만 부여하고, 에이전트가 스스로 작업을 찾아 병렬로 진행하게 했습니다. 수학에 특화한 자체 모델도 학습시켰습니다. 기술진 Ashvin Swaminathan은 형식화된 수학에 대수기하학이라는 거대한 “블랙홀”이 있었다며, 이번 결과로 그 공백을 메웠다고 설명했습니다.

소프트웨어로 확장

회사는 검증된 결과 하나하나가 다음 증명의 구성 요소가 된다고 주장합니다. 대상은 수학자만이 아닙니다. AI가 작성하는 코드가 늘수록 버그와 보안 결함이 없음을 보증하기 어려워지기 때문입니다. CEO Carina Hong은 미래의 소프트웨어가 검증된 토대 위에 서야 한다고 말하며, 다른 코딩 기업들에도 같은 규모의 형식화에 도전하라고 공개적으로 요구했습니다. Axiom은 지난 3월 Menlo Ventures 주도로 2억 달러 시리즈 A를 유치했습니다.