Salvato in:
| Autori principali: | , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2605.14061 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917493658877952 |
|---|---|
| author | Patel, Nilay Arias, Noah Babayan, Davit Cochran, Victoria Libman, Timothy Mahmood, Hafsah McCarty, Liam Munoz, Soli Willey, Laurel Flanigan, Jeffrey |
| author_facet | Patel, Nilay Arias, Noah Babayan, Davit Cochran, Victoria Libman, Timothy Mahmood, Hafsah McCarty, Liam Munoz, Soli Willey, Laurel Flanigan, Jeffrey |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_14061 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | MathAtlas: A Benchmark for Autoformalization in the Wild Patel, Nilay Arias, Noah Babayan, Davit Cochran, Victoria Libman, Timothy Mahmood, Hafsah McCarty, Liam Munoz, Soli Willey, Laurel Flanigan, Jeffrey Artificial Intelligence Machine Learning 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. |
| title | MathAtlas: A Benchmark for Autoformalization in the Wild |
| topic | Artificial Intelligence Machine Learning |
| url | https://arxiv.org/abs/2605.14061 |