The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization

Chengxiao Dai, Zhaokun Yan, Zhanhui Lin

Headline type-correctness (TC\%) of LLM autoformalization has climbed from $\sim$53\% to $\sim$76\% in two years, yet this scalar conceals which errors each method resolves. We pro…