Automatic Textbook Formalization

3줄 요약

1. Meta FAIR·ENPC·KIAS 공동 연구진이 500쪽이 넘는 대학원 수준 대수적 조합론 교과서 전체를 자동 AI 시스템으로 Lean에 형식화했다. 결과물은 13만 줄 코드와 5,900개 Lean 선언이다.
2. 3만 개(정확히는 30,046개)의 Claude 4.5 Opus 에이전트가 git 버전 관리로 공유 코드베이스에서 병렬 협업해 1주 만에 끝냈다. 사람의 협업 소프트웨어 공학에서 검증된 관행(트렁크 기반 개발, PR 리뷰, 머지 큐, 파일 기반 이슈 트래커)을 그대로 가져와 조정 문제를 풀었다.
3. 추론 비용은 약 10만 달러로, 같은 작업을 할 인간 전문가 팀의 인건비와 대등하거나 그 이하였다. 연구진은 더 나은 모델 없이도 3~10배 비용 절감이 가능하다고 본다. 코드와 Lean 코드베이스, 대조용 blueprint 웹사이트를 오픈소스로 공개했다.

무엇을 풀려는 문제인가

논문은 수학의 “재현 위기"를 심사(refereeing) 위기로 규정하며 문을 연다. 현재의 인센티브 구조와 시간 제약 아래에서 저널 심사자는 논문의 모든 증명을 세세히 검증하지 못한다. 심사자의 일은 모든 논증의 타당성을 확인하는 것이 아니라 “논문이 쓴 방법이 주요 결과를 증명할 만큼 강력하다고 스스로 납득하는” 수준에 머문다. 이 방식은 실무에서 놀랄 만큼 잘 작동하지만, 저명한 저자의 중요한 결과에도 간과된 오류가 남을 수 있다. 필즈상 수상자 블라디미르 보예보드스키의 말을 인용한다.

신뢰받는 저자의 기술적 논증이 검증하기 어렵고 이미 옳다고 알려진 논증과 비슷해 보이면, 그것이 세세히 확인되는 일은 거의 없다.

증명 보조 소프트웨어(proof assistant)를 이용한 수학의 형식화(formalization)는 이 문제의 야심 찬 장기 해법이다. 신뢰 계층을 작고 엄밀하게 검증된 증명 체커 커널과, 논문당 수십 줄의 수작업 검토 정의·정리문으로 줄인다. 다만 요구되는 노력과 전문성이 커서 지금까지 형식 검증은 소수의 이정표급 연구에 그쳤다.

연구진은 일상적 형식화에 아직 무엇이 빠졌는지를 두 가지로 짚는다. 첫째, 교과서 문헌의 방대한 기초 내용이 증명 보조기에 들어와야 한다. 둘째, 형식화 비용(시간·노력·전문성)이 시도할 만한 수준으로 낮아져야 한다. Lean의 수학 라이브러리 mathlib는 약 220만 줄로 형식 수학의 최대 통합 라이브러리지만, 초기의 급성장 이후 확장 속도가 대략 선형으로 안정되어 순수 인간 주도 접근의 확장성에 의문을 남긴다.

자동 형식화의 세 세대

논문은 자동 형식화 시스템을 세 세대로 구분한다.

3세대는 조정 문제(coordination problem)를 풀어야 한다. 큰 에이전트 군집을 어떻게 조직해야 공유 프로젝트에서 일관된 진전을 낼 수 있는가. 소프트웨어 공학 쪽의 초기 탐색은 놀랄 만큼 큰 코드베이스를 만들어냈지만, 에이전트를 충분히 오케스트레이션하지 않을 때 생기는 일관성(coherence) 문제도 드러냈다.

방법: 사람의 협업 공학을 그대로 가져오다

이 연구의 핵심 설계는 인간 협업 소프트웨어 공학에서 검증된 표준 관행에 의존해 멀티에이전트 스캐폴드를 단순하게 짠 것이다. 다섯 가지다.

1. 잘 정의된 작업을 배정한 서브에이전트를 통한 대규모 병렬화.
2. 짧게 유지되는 기능 브랜치 위에서의 트렁크 기반 개발(git).
3. 명확한 코드 품질 지침을 가진 독립 리뷰어의 풀 리퀘스트 리뷰.
4. 머지 전 스테이징 브랜치에서 테스트하는 머지 큐 — 그래서 main은 항상 빌드된다.
5. 파일 시스템 기반 이슈 트래커를 통한 에스컬레이션·소통 메커니즘.

공유 파일이 에이전트 사이의 직접적이고 단순하며 보편적인 소통 프로토콜을 제공한다. 별도의 메시지 전달 장치가 필요 없다. 소스 관리는 버전 이력과 충돌 추적을 주고, 에이전트는 이 인터페이스를 자연스럽게 다룬다. 연구진은 이 시스템이 조정 문제를 대체로 해소하고 “겁 없는 동시성(fearless concurrency)“을 허용한다고 밝혔다.

에이전트 역할 분담

기능 개발과 조정을 위해 여러 역할을 두었다.

• Sketcher(스케처): 원본 자료의 한 덩어리(예: 한 장)를 받아 그 안의 모든 정의·정리문을 형식화하되, 증명은 sorry 키워드로 비워 둔다.
• Prover(증명자): 증명이 빠진 정리를 받아 가능하면 증명을 채운다. 정리문·순서·헬퍼 문제를 이슈 트래커에 올리거나 직접 고칠 수 있다.
• Reviewer(리뷰어): PR을 받아 품질 기준 충족 여부를 판단한다. 리뷰는 둘로 나뉜다. 명제가 원본을 정확히 반영하는지 보는 수학 리뷰와, 관례·명명·문서·API 설계 등 코드 품질을 보는 공학 리뷰다.
• Maintainer(관리자): 열린 이슈를 받아 “진전을 낸다”. 완전히 해결하거나, 나중의 해결을 쉽게 만들 코드를 커밋한다.
• Triage·Scan·Progress: 각각 이미 해결된 이슈 표시, 코드베이스 전역 문제(중복·리팩터링 여지 등) 스캔, 목표 정리 진척 추적을 맡는다.

리뷰어의 판정은 세 가지다. 머지 가능한 코드는 승인, 사소한 문제가 있으면 변경 요청, 회생 불가(잘못된 증명 전략, 머지 충돌로 유실된 코드, 기존 결과 중복)면 거부다. 리뷰어 하나라도 거부하면 PR은 폐기된다. Lean 코드를 건드리는 PR과 이슈 트래커 폴더를 건드리는 PR 사이에 본질적 차이는 없고, 모든 PR이 두 리뷰어 유형의 검토를 거친다.

사례 연구: 대수적 조합론 교과서

연구진은 Darij Grinberg의 500쪽 넘는 대학원 대수적 조합론 교과서를 대상으로 삼았다. 이 책을 고른 이유가 방법론의 핵심을 드러낸다.

• 오염(contamination) 회피: mathlib의 기존 내용과 대체로 겹치지 않는 교과서를 골라, 에이전트가 라이브러리 코드를 베껴 “커닝"하는 것을 막았다. 에이전트는 인터넷 접근이 없어 부정행위 가능성이 더 줄었다.
• 기초 정비가 먼저라는 관점: 최신 연구 결과 형식화보다, 인간 mathlib 기여자가 낼 수 있는 속도보다 빠르게 기초 문헌을 일상적으로 형식화하는 것이 먼저다. mathlib에서 곧바로 접근 가능한 잘 고른 자료로 작업하는 것은 단순화가 아니라 문헌 자동 형식화 시스템의 기본 운영 방식이라는 주장이다.

연구진은 활동을 성취로 착각하지 않으려고 LaTeX 원본에서 340개의 정의·정리를 형식화 목표(target)로 지정했다. 대상 교과서가 다루는 내용은 형식 멱급수, 순열, 행렬식(코시~비네 공식 등), 교대합과 부호 셈, 분할과 q-급수, q-이항계수, 대칭 함수(슈어 다항식, 리틀우드~리처드슨 규칙 등), 격자 경로, 도미노 타일링 응용에 이른다.

결과

형식화는 1주의 실행 끝에 성공적으로 마무리됐고, 340개 목표 정의·정리를 모두 형식화했다. 초기 목표 4개는 원본에서 연습문제로 올바르게 재분류되어 시도하지 않았다. 이 연구는 문제 풀이가 아니라 형식화에만 집중했다. 전체 줄 수와 선언 수 모두 거의 일정한 속도로 늘어 최종적으로 13만 줄, 5,900개 선언에 이르렀다.

작업을 쉽게 리뷰할 수 있는 작은 조각으로 쪼갠 전략이 잘 통했다. 에이전트가 제출한 가장 큰 PR도 수백 줄을 넘지 않았다.

실험은 Lean에 능한 에이전틱 코딩 모델 Claude 4.5 Opus를 썼고, 연구진은 현행 프런티어 모델 대부분이 이 작업에서 대체로 비슷하게 동작하리라 본다. 리뷰 에이전트가 높은 명제 형식화 품질 기준을 세웠고 핵심 명제·정의는 수작업으로 표본 점검했다. 다만 개별 정리·정의가 의미상 충실히 번역되지 못했을 가능성은 남는다고 밝혔다.

규모와 토큰

에이전트 유형별 토큰 사용을 정리한 표는 시스템의 무게를 보여준다.

전체 형식화는 입력 830억 토큰(멀티턴 대화의 중복 계산 포함)과 출력 5억 6,100만 토큰을 썼다. 토큰 캐싱이 없었다면 총비용은 43만 달러에 해당한다. 로그에 캐싱 통계가 없어 대략 계산하면 전체 약 10만 달러, 그중 1만 4천 달러가 출력 토큰 몫이다. 페이지당 약 200달러, 목표 정리·정의당 약 300달러다.

연구진은 이 초기 탐색이 실제 비용을 크게 과대평가한다고 본다. 세 가지 이유다. (1) 실행 중에 오케스트레이션 코드를 고쳐 가며 진행해, 입력 토큰의 절반가량이 재시작 때 이어지지 못한 중단(aborted) 에이전트에 쓰였다. (2) 지시와 달리 연습문제나 인용된 정리를 붙잡은 불필요한 작업이 있었다. (3) 의존성 추적이 없어, 막힌 에이전트를 그냥 다시 큐에 넣었다. 이 세 가지를 개선하면 더 나은 모델 없이도 추론 비용을 3~10배 줄일 수 있다고 본다.

관찰된 실패 유형

논문에서 가장 값진 부분은 협업 공학의 민첩성(agility)과 일관성(coherence) 사이 긴장이 멀티에이전트 형식화에서 어떻게 나타났는지를 구체적 사례로 보여준 대목이다.

수학적 일관성 실패. $N$-분할 데이터 타입이 슈어 다항식·대칭 다항식·피에리 규칙 세 장에서 각각 독립으로 정의됐다. 모두 수학적으로 동등했지만 중복이었다. 공유 정의를 별도 파일로 빼내자 잠시 사본이 넷으로 늘었고, 두 파일은 공유 정의로 옮겼으나 세 번째는 8천 줄에 걸친 사설 API 때문에 이관이 너무 번거로워 대신 동등성을 증명해 두 버전을 이었다.

가장 어려웠던 부분은 벤더~크누스 대합(Bender-Knuth involution)의 형식화였다. 원본은 이 사상을 정의하고 준표준 타블로로 다시 매핑됨을 증명하는 데 다섯 쪽을 쓴다. 조합론 알고리즘이 흔히 그렇듯 매우 비형식적으로 설명되기도 한다.

따라서 $\beta_k(T)$는 $T$의 각 행에서 자유로운 $k$와 자유로운 $(k+1)$ 사이의 불균형을 “뒤집어” 얻는다(자유로운 $k$가 많던 행은 자유로운 $(k+1)$이 똑같이 많아지도록, 그 반대도 마찬가지로).

여기서 두 정의가 원래 따로 주어졌고, 이번에는 엄밀히 동등하지 않았다. 하나는 잘못된 지름길을 택했고(매칭 조건을 무시하고 허용된 항목을 전부 뒤집음), 다른 하나는 매칭을 구현했으나 $k+1$ 항목의 방향을 틀렸다(가장 왼쪽 대신 가장 오른쪽 초과분을 골랐다). 이 모순된 상황이 에이전트 churn으로 이어졌다. 깨진 정의로도 증명 가능한 보조정리는 증명자 에이전트가 기꺼이 증명했고, 거짓이 되는 보조정리 앞에서는 반례를 남기고 이슈를 만들었으나 전역적으로 파고들어 해결 경로를 제시하지는 못했다.

프로세스 수준 실패. 토끼굴(rabbit holes)이 큰 문제였다. 에이전트가 명시적 지시를 어기고 인용된 정리나 지나가듯 언급된 명제의 증명에 착수했다. 예컨대 도미노 타일링의 카스텔레인 공식에서 에이전트들이 파피안과 FKT 알고리즘 이론을 엉성하게 펼치기 시작해 실제 목표에서 자원을 빼돌렸다. 배치 없는 단일 머지 큐도 병렬성이 높은 국면에서 병목이 됐다.

일관성 조종. 오케스트레이션을 빡빡하게 죄면 책임이 분산되어 “LLM 관료(bureaucrats)“로 퇴화하며 왜 자기 작업이 먼 이슈에 막혔는지를 문서화하는 데 그 장치를 쓴다. 느슨하게 풀면 능동성은 커지지만 구조·중복·관례 불일치의 대가를 치른다. 연구진의 경험칙은 프로젝트 초반에는 자유를 더 주어 병렬성을 살리고, 릴리스가 가까워지면 “나사를 조여” 정리·조화한다는 것이다. 형식화 프로젝트에 “모의 담금질(simulated annealing)“을 한다는 비유를 든다.

가장 눈여겨본 대목

내가 가장 곱씹은 것은 사람의 개입이 “무시할 만한(negligible)” 수준이었다는 서술이다. 연구진은 실행을 몇 차례 수동으로 멈추고 CLI 에이전트를 띄워 목표 정리 상태·sorry 발생·의존성에 관한 심층 보고서를 만들게 했다. 그러나 증명이나 그 구조를 일부러 들여다보지 않았고, 에이전트가 내놓은 관찰의 우선순위를 정하고 상세 분석을 요청하는 높은 수준의 상호작용만 했다고 밝혔다. 수학 전문가가 증명 하나하나를 검토하지 않고도, 조율의 방향만 잡아 500쪽 교과서가 형식화됐다는 이야기다.

또 하나는 prover와 maintainer 역할이 결국 합쳐질 수 있는가라는 열린 질문이다. prover는 설계상 단일 Lean 파일만 다루지만, maintainer는 최대 14개 파일에 걸친 무거운 리팩터링을 수행한다. 대신 maintainer는 조정 파일만 건드리는 “장부 정리 PR"에 더 자주 관여한다. 연구진은 답을 내리지 않되, 후속 반복에서 prover 역할이 maintainer에 흡수될 여지를 열어 둔다.

확장 전망

연구진은 연구 수학의 일상적 형식화를 실현하려면 새 논문당 비용이 그 미형식화 의존성 트리의 크기에 비례해 커지는 대신 페이지당 거의 일정한 비용으로 떨어져야 한다고 본다. 그 전제는 공유 수학 인프라의 체계적 형식화다. 이 공유 코퍼스가 1,000~10,000권의 교과서에 걸쳐 있다고 추산한다. 현대 연구 정리 대부분을 진술할 수 있게 해 주는 핵심 대상과 도구를 담은 문헌이다.

경시 수학이나 최신 연구를 직접 겨냥하는 대안과 대비된다. 경시 문제는 대개 고도로 특화된 자기 완결적 퍼즐이고, 최신 연구를 곧장 형식화하면 특정 정리에 맞춘 좁고 임시적인 정의가 나오기 쉽다. 반면 교과서는 일반성과 재사용성을 최대화하도록 설계되어, 형식화하면 오래 값을 내는 복리적·재사용 가능한 수학 지식이 쌓인다. mathlib이 그것을 보였다.

출처

Fabian Gloeckle, Ahmad Rammal, Charles Arnal, Remi Munos, Vivien Cabannes, Gabriel Synnaeve, Amaury Hayat (FAIR, Meta · CERMICS, ENPC · KIAS). “Automatic Textbook Formalization.” arXiv:2604.03071, 2026.

• 원문: https://arxiv.org/abs/2604.03071
• 코드: https://github.com/facebookresearch/repoprover
• 형식화 결과: https://github.com/facebookresearch/algebraic-combinatorics

본문 그림은 논문 arXiv HTML 판(v1)의 figure를 인용했다.