MathAtlas: A Benchmark for Autoformalization in the Wild

Current autoformalization benchmarks are largely focused on olympiad or undergraduate mathematics, while graduate and research-level mathematics remains underexplored. In this paper, we introduce MathAtlas, the first large-scale autoformalization benchmark of in the wild graduate-level mathematics, containing ~52k theorems, definitions, exercises, examples, and proofs extracted from 103 graduate mathematics textbooks. MathAtlas is enriched with a mathematical dependency graph containing ~178k relations, and is the first autoformalization benchmark to include such relations, facilitating evaluation and development of dependency-aware autoformalization systems. Our extensive experiments show that MathAtlas is high quality but extremely challenging: strong baselines achieve at most 9.8% correctness on theorem statements and 16.7% on definitions. Furthermore, we find performance of state-of-the-art models degrades substantially with dependency depth: on MA-Hard, a subset of 700 entities with the deepest dependency trees, the best model achieves only 2.6% correctness for autoformalization on this challenging dataset. We release MathAtlas to the community as a benchmark set for large-scale autoformalization of graduate-level mathematics in the wild.

📋 한 줄 요약

**[자동 형식화 / 수학 벤치마크]** 대학원·연구 수준 수학 교과서에서 추출한 약 52k 개체와 178k 의존 관계를 갖춘 최초의 대규모 in-the-wild 자동 형식화 벤치마크 MathAtlas 공개.

🎯 핵심 기여도

올림피아드·학부 수학에 집중돼 있던 기존 자동 형식화(autoformalization) 벤치마크의 한계를 넘어, 대학원 수준 수학을 본격적으로 다룬 첫 대규모 데이터셋 구축.
103권 대학원 수학 교과서에서 정리·정의·연습문제·예제·증명 약 52k개를 추출.
약 178k개의 수학적 의존 관계를 담은 dependency graph를 함께 제공해 의존성 인식(autoformalization) 시스템 연구의 토대 마련.
강력한 베이스라인이 정리 진술에서 9.8%, 정의에서 16.7%에 그치는 매우 도전적인 평가 환경 제시.

💡 핵심 아이디어

실제 연구 수학은 단일 정리가 독립적이지 않고 다른 정의·보조 정리에 깊이 의존한다. 따라서 자동 형식화도 단일 진술 수준이 아니라 의존 구조를 인식하며 수행되어야 하며, 이를 평가할 수 있는 인프라가 필요하다.

🔬 기술적 접근법

**모델/방법론**: 대학원 수학 교과서 103권으로부터 정리·정의·증명을 추출하는 파이프라인 + 개체 간 의존 관계 그래프 구축.
**핵심 기법**: 의존 깊이(dependency depth) 별 난이도 분리, 가장 깊은 의존 트리를 갖는 700개 개체로 구성된 MA-Hard 서브셋 정의, 강력한 LLM 기반 베이스라인에서의 성능 측정.

📊 주요 결과

정리 진술 자동 형식화: 최강 베이스라인 정확도 최대 9.8%.
정의 자동 형식화: 최대 16.7%.
의존 깊이가 깊어질수록 성능 급락 — MA-Hard에서 최상위 모델조차 2.6%.

💭 의의 및 한계

**의의**: 자동 형식화 분야의 평가 한계를 단숨에 연구 수학 수준으로 끌어올리며, 의존 인식(dependency-aware) 자동 형식화라는 새로운 연구 방향을 정식 의제로 제시. **한계**: 교과서 기반이라 최신 연구 논문 수준의 표기 다양성·암묵 가정은 여전히 제한적, 평가 자동화에는 형식 증명 시스템 의존이 필요.

🚀 실용적 활용

Lean·Coq·Isabelle 기반 수학 라이브러리 자동화 도구의 평가 표준.
의존성 인식 LLM autoformalizer 학습용 supervised/instruction 데이터.
대학원 수학 교육에서 정형화된 풀이 검증·튜터링 시스템 구축.