인공지능 스타트업 '액시엄 매스(Axiom Math)'는 자사의 독립형 에이전트 시스템이 수학자들이 역사상 집필한 가장 방대한 오픈 수학 참고 문헌 중 하나인 '스택스 프로젝트(Stacks Project)'의 전체 내용을 공식적으로 프로그래밍 검증(Formal Verification)하는 데 성공했다고 발표했습니다.
수학적 지식을 검증 가능한 코드로 변환
2005년 컬럼비아 대학교 수학 교수 요한 드 용(Johan de Jong)이 시작한 Stacks 프로젝트는 대수학 및 대수기하학 원리부터 정수론의 고급 이론에 이르기까지 약 7,654페이지에 달하는 내용을 담고 있습니다. Axiom Math의 에이전트 군단은 이 복잡하고 상호 연결된 텍스트를 약 1,600만 줄의 '린(Lean)' 언어 코드로 번역하는 데 성공했습니다. 린은 검증 소프트웨어가 모든 수학적 증명을 한 줄씩 검토하여 엄격한 논리적 무결성을 확인할 수 있도록 설계된 전문 프로그래밍 언어입니다.
멘로 벤처스(Menlo Ventures)가 주도한 첫 번째 투자 라운드에서 2억 달러를 유치하며 기업 가치 16억 달러를 기록한 이 회사는, 향후 인공지능 시스템이 소프트웨어 개발 및 과학 연구에 의존할 수 있는 신뢰할 수 있고 프로그래밍적으로 증명된 지식 기반을 구축하는 것을 목표로 합니다. 이를 통해 'AI 슬롭(AI slop)'이라 불리는 오해의 소지가 있거나 부정확한 결론을 도출하는 문제를 방지하고자 합니다.
에이전트의 프로그래밍 작동 방식과 구조적 연결성 과제
2025년 3월 스탠퍼드 대학교 수학 박사 과정을 중퇴하고 Axiom을 설립한 25세의 창업자이자 CEO 카리나 홍(Carina Hong)은 가장 큰 과제가 수천 개의 이론 간의 연결성을 유지하고 개념적 모순을 피하는 것이었다고 설명했습니다. 기술 팀원인 아슈빈 스와미나탄(Ashvin Swaminathan)은 인공지능 에이전트가 모든 단계에서 직접적인 지시를 받은 것이 아니라, 유연한 계층적 구조를 통해 작업을 병렬로 분배했다고 지적했습니다. 또한 일반적인 코드 생성 모델에 의존하는 대신 건전한 수학적 사고를 하도록 훈련된 맞춤형 모델을 활용했다고 덧붙였습니다.
이 성과가 기술 분야에 의미하는 바
이번 발전은 특히 대수기하학 분야와 같이 컴퓨터를 통한 수학 증명의 큰 격차를 해소하는 실질적인 단계를 의미합니다. 형식 검증의 이점은 학계에만 국한되지 않습니다. 컴퓨터 코드를 통한 증명 문서화는 재사용 가능한 기초 환경을 제공합니다. Axiom Math는 칩 설계나 중요 시스템 계산과 같이 소프트웨어 개발자들이 보안 취약점과 소프트웨어 작성 시 에이전트 의존도가 높아짐에 따라 발생하는 숨겨진 오류를 방지하기 위해 이러한 검증된 규칙이 필요할 것이라고 확신하고 있습니다.