1600만줄 수학 코드 공개…AI 작성분은 사람 검토 남아

Axiom Math가 대수기하학 참고서 Stacks Project에서 형식화할 수 있는 수학 항목을 약 1600만 줄의 Lean 코드로 공개했다. AI 에이전트가 작성한 증명도 컴퓨터로 검사하도록 구성했지만, AI 작성분을 원문과 대조하는 작업은 남아 있다.

Axiom Math는 4일 발표문에서 약 7500쪽 분량의 Stacks Project를 재사용 가능한 하나의 형식 수학 라이브러리로 만들었다고 밝혔다. 공개 저장소는 원문 항목과 이에 대응하는 형식 명제를 연결해 제공한다.

공개 저장소 README에 따르면 코드는 Lean 4와 수학 라이브러리 Mathlib을 기반으로 하며 Apache 2.0 라이선스를 적용했다. 누구나 저장소를 내려받아 코드를 살펴볼 수 있는 오픈소스 프로젝트다.

Stacks Project는 대수기하학의 정의와 정리, 증명을 담은 오픈소스 참고서로 2005년 시작됐다. 원문 각 항목에는 고유 태그가 붙어 정의와 정리 사이의 의존 관계를 추적할 수 있다.

Axiom Math는 이 태그를 Lean 코드에도 연결했다. 연구자는 원문의 항목과 그에 대응하는 형식 명제를 나란히 살펴볼 수 있다.

형식화는 사람이 읽는 수학 명제와 증명을 컴퓨터가 처리할 수 있는 언어로 옮기는 작업이다. Lean 커널은 입력된 형식 명제에 대해 증명이 논리적으로 성립하는지 검사한다.

이 검사는 형식 명제가 원문의 뜻을 정확히 담았는지까지 보증하지 않는다. 원문과 코드가 같은 의미인지 확인하려면 별도의 대조가 필요하다.

공개 저장소가 다루는 범위는 형식화할 수 있는 Stacks Project의 태그다. 예제와 연습문제, 일부 설명은 남은 작업으로 분류돼 있어 약 7500쪽의 모든 문장이 코드로 옮겨졌다는 뜻은 아니다.

코드 검토 상태는 두 갈래로 나뉜다. ‘StacksCore’는 사람이 원문과 대조해 검토한 부분이고, ‘StacksFrontier’는 AI 에이전트가 작성해 아직 사람 검토를 거치지 않은 부분이다.

Axiom Math의 형식화 메타데이터는 전체 검토 상태를 자체 평가로 표시한다. 따라서 AI 작성 코드의 기계 검사 여부와 사람이 원문에 비춰 검토했는지는 구분해 봐야 한다.

Axiom Math는 형식화 과정에서 원문 명제 수십 건에 추가 가정이 필요하거나 특정 조건에서 성립하지 않을 가능성이 있는 사례를 찾았다고 밝혔다. 이는 회사의 설명이며 원 프로젝트가 확인한 오류 목록과는 구별된다.

원 프로젝트 관리자는 10월 21일 AI가 작성한 댓글이나 풀 리퀘스트를 당분간 제출하지 말아 달라고 공지했다. Axiom Math는 형식화 결과를 원 프로젝트와 분리된 자체 저장소에서 관리한다.

11월 5일 공개 저장소에는 두 파일을 수정해 빌드 오류를 고치려는 커밋이 올라왔다. 커밋이 추가됐다는 사실만으로 수정본의 빌드가 완료됐다고 볼 수는 없다.

AI가 수학 문제의 답을 제시하는 데서 나아가 풀이를 형식적으로 검증하는 연구 흐름은 구글 딥마인드의 수학 협력과 형식 증명 시스템을 다룬 본지 보도에서도 소개됐다. 이번 작업은 AI가 작성한 수학 코드의 규모와 사람 검토의 필요성을 함께 보여준다.

Axiom Math는 대수기하학의 응용 사례로 타원곡선과 디지털 암호학을 언급했지만, 이번 형식화 결과를 특정 블록체인이나 가상자산에 적용했다고 발표하지 않았다. 수학 문헌인 Stacks Project는 비트코인 기반 네트워크 스택스(STX)와 별개 프로젝트다.

공개 저장소는 예제·연습문제의 형식화와 AI 작성분의 사람 검토를 남은 기여 작업으로 제시했다.