인공지능(AI)이 매주 새로운 수학 난제를 푸는 듯 보이지만, 동시에 검증되지 않은 증명들이 쏟아져 나오면서 수학계에 'AI발 쓰레기(AI slop)'가 넘쳐날 수 있다는 우려가 커지고 있습니다. 이러한 문제를 해결하기 위해 Axiom Math는 AI 에이전트를 활용한 '형식적 검증(formal verification)'이라는 해법을 제시하며, 최근 수학 분야에서 가장 방대한 라이브러리 중 하나인 스택스 프로젝트(Stacks Project)를 성공적으로 검증했다고 발표했습니다.
Axiom Math는 25세의 CEO 카리나 홍(Carina Hong)이 설립한 스타트업으로, 2억 달러(약 2,700억 원) 규모의 시리즈 A 투자를 유치하며 주목받았습니다. 이들은 스택스 프로젝트의 약 7,654페이지에 달하는 내용을 약 1,600만 줄의 '린(Lean)' 코드(수학적 증명을 컴퓨터로 검증할 수 있도록 작성된 프로그래밍 언어)로 번역하고, 증명 보조 프로그램(proof assistant)을 통해 한 줄 한 줄 논리적 오류를 검사했습니다. 스택스 프로젝트는 컬럼비아 대학교(Columbia University)의 요한 드 용(Johan de Jong) 교수가 2005년에 시작한 오픈소스 프로젝트로, 대수학, 기하학, 정수론 등 광범위한 수학 분야의 고급 이론들을 담고 있으며, 수학자들 사이에서는 20세기 수학의 기초를 재건한 '부르바키(Bourbaki) 총서'에 비견될 정도로 중요한 자료로 평가받습니다. Axiom Math의 AI 에이전트들은 병렬적으로 작업을 수행하며 스스로 과제를 찾아 해결하는 방식으로 이 복잡한 상호 연결된 라이브러리를 성공적으로 검증해냈습니다.
이번 스택스 프로젝트의 형식적 검증은 수학계에 큰 의미를 가집니다. 특히 대수 기하학(algebraic geometry) 분야는 그동안 형식화된 수학에서 '거대한 블랙홀'로 불릴 만큼 검증된 기반이 부족했는데, 이제 연구자들은 Axiom Math가 구축한 검증된 결과들을 바탕으로 새로운 증명을 더욱 쉽게 검증할 수 있게 되었습니다. 이는 UCLA의 필즈상 수상자 테렌스 타오(Terence Tao) 교수가 언급했듯이, '더 많은 형식화된 증명이 있을수록 더 많은 형식화된 증명을 만들 수 있다'는 원리를 현실화하는 것입니다. 나아가 Axiom Math는 이러한 수학적 검증 기술이 단순히 수학에만 국한되지 않고, AI 에이전트가 작성하는 미래 소프트웨어의 버그와 보안 취약점을 줄이는 데도 핵심적인 역할을 할 것으로 기대하고 있습니다. 검증된 수학적 기반 위에서 AI가 코드를 작성하고 새로운 인프라를 구축함으로써, 'AI발 쓰레기'를 방지하고 신뢰할 수 있는 기술 발전을 이끌 수 있다는 비전입니다.