ICML 2026spotlight0 citations
Position: The Case for Theory-Level Autoformalization
Marcus Min, Deyuan Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, Xujie Si, Osbert Bastani
Abstract
Autoformalization, translating informal natural language into formal, machine-verifiable languages, has been framed as a tool to generate training data for neural theorem provers, with most work focusing on individual statements. This position paper argues for theory-level autoformalization: formalizing complete theories, including axioms, definitions, theorems, proofs, tactics, and their inter-dependencies as structured libraries. We examine the significance of this shift, address 3 alternative views, identify 5 open challenges, and propose 3 promising paths forward.
Theory
BibTeX
@inproceedings{icml2026_positionthecasef,
title = {Position: The Case for Theory-Level Autoformalization},
author = {Marcus Min and Deyuan Mike He and Zhaoyu Li and Zixuan Yi and Sharad Malik and Aarti Gupta and Xujie Si and Osbert Bastani},
booktitle = {ICML 2026},
year = {2026}
}