액시엄, 1,600만 줄 수학 라이브러리 공개…사람 검수는 진행 중

AI 수학 기업 액시엄이 대수기하학 참고서 ‘스택스 프로젝트’를 Lean 코드로 옮긴 라이브러리를 11월 4일 공개했다. 회사가 밝힌 규모는 약 1,600만 줄이다. 연구자는 그 안의 정의와 정리를 불러와 새 증명에 사용할 수 있다. 공개 저장소는 사람이 검토한 부분과 AI가 작성해 사람의 검토를 기다리는 부분을 나눴다.

스택스 프로젝트는 대학원생과 연구자를 위한 오픈 참고서다. 대수기하학에서 필요한 개념을 쌓아 대수적 스택의 기초를 설명한다. 원문은 각 결과에 영구 식별자인 태그를 붙이고, 온라인 링크로 어떤 보조정리와 정의를 사용하는지 따라갈 수 있게 했다. 이 참고서에는 가환대수, 스킴, 다양체와 대수적 공간도 포함된다. 원문은 입문 강좌가 아닌 전문 참고 자료로 설계됐다. 이번 공개물은 이 수학적 내용을 형식 언어로 다루려는 별도 프로젝트다.

액시엄은 여러 AI 에이전트가 문장을 번역하고, 기존 수학 라이브러리를 검색하며, 증명을 병렬로 구성했다고 설명했다. 개별 정리의 증명을 만드는 것과 함께 여러 장에서 사용하는 정의와 의존 관계를 일관되게 유지하는 작업을 진행했다고 밝혔다.

코드 검사와 사람의 검토를 나눠 공개

저장소에서 StacksCore는 사람이 원문과 대조하고 기존 Lean 수학 라이브러리인 Mathlib의 작성 기준에 맞춘 부분이다. StacksFrontier는 AI가 작성한 형식화 코드로, 검토를 거쳐 Core로 옮기는 대상이다. README는 두 영역 모두 Lean 커널이 증명을 검사하며, 미완성 증명의 빈자리를 허용하는 ‘sorry’를 사용하지 않았다고 명시했다.

공개한 형식화 메타데이터는 검토 상태를 ‘자체 평가’로 표시한다. Frontier의 각 문장이 해당 원문 태그와 대조됐지만 사람의 검토는 아직 받지 않았다고 적었다. 따라서 코드의 논리 검사 결과를 읽을 때는 자연어 원문을 충실히 옮겼는지 확인하는 검토 상태도 함께 살펴야 한다.

형식화 대상도 메타데이터에 고정했다. 원문의 특정 Git 커밋에 있는 1~109장을 출처로 지정하고, 연습문제와 폐기된 장은 범위에서 뺐다. 기반 정의와 Core는 사람이 작성하고 검토했으며 Frontier 대부분은 자사 정리 증명 시스템 AxiomProver가 자율적으로 형식화했다고 기록했다. 개발은 액시엄 내부 저장소에서 이뤄졌다.

실제 배포 코드에는 후속 수정도 있다. 공개 커밋 012108f는 두 파일을 고쳐 빌드가 성공하도록 했다고 설명한다. 자동 생성된 방정식 보조정리가 중복돼 커널에서 거부된 문제를 고쳤다는 내용이다. AI Ping은 전체 라이브러리를 별도로 빌드하지 않았으며, 이 수정의 효과는 공개 커밋 설명에 근거한다.

액시엄의 탐색 사이트는 같은 태그에 대응하는 Lean 코드와 원문, 의존 관계를 연결한다. 하나의 태그를 여러 선언이 나눠 형식화하면 각각의 코드를 탭으로 보여 준다. 이용자는 특정 정리의 코드와 그 정리가 기대는 결과를 함께 찾아볼 수 있다. 사이트는 이미 Mathlib에 있는 태그를 초록색으로, Lean에 적용할 대상으로 판단하지 않은 태그를 빨간색으로 표시한다고 안내한다. 코드의 출처와 적용 대상 여부를 나눠 보여 주는 방식이다.

의존 관계 화면은 태그가 붙은 선언을 노드로 표시하고, 부·장·절을 따라 묶어 탐색하도록 구성했다. 선언이 다른 선언을 사용하는 관계와 자연어 문헌의 인용 관계를 별도로 표시한다. 기여 항목에는 새 형식화, Frontier 검토, Core로의 이동, 기존 증명 개선이 포함된다.

원문 스택스 프로젝트는 별도의 기여 방침을 유지한다. 관리자인 요한 더용은 10월 21일 자 글에서 당분간 AI가 쓴 댓글과 풀 리퀘스트를 보내지 말아 달라고 요청했다. 직접 읽고 발견한 문제를 사람이 작성해 보내는 제안은 계속 받으며, 원문 수정도 손으로 이어가겠다고 밝혔다.

라이브러리 재사용에는 빌드 자원도 필요하다. README는 약 6만3,000개 모듈을 전체 빌드하면 시간과 메모리를 많이 쓴다고 안내한다. Mathlib의 컴파일 파일은 내려받을 수 있으며, 스택스 모듈 자체의 컴파일 캐시 서비스는 계획 중이라고 표시했다.