Autoformalization via a Layered Protocol

Autoformalization translates informal language into formal representations whose correctness is machine-verifiable through logical solvers (e.g., SMT solvers, theorem provers, temporal reasoners). This capability is increasingly important as LLMs generate code, executable programs, and actionable decisions that must faithfully satisfy their intended formally representable specifications. While promising, existing methods are largely one-shot, entangling distinct error modalities into a single undifferentiated failure that obscures both where systems fail and how to address them. We introduce a hierarchical taxonomy of autoformalization errors, organized along three modes : syntax, semantics, and grounding. Building on this taxonomy, we propose a layered approach that detects and resolves errors hierarchically, addressing each error class at the stage where it arises rather than at the end of the pipeline. We show that this approach significantly outperforms state-of-the-art methods across three benchmarks spanning first-order logic, theorem proving, and time-series applications.