FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
2026-07-06 • Computation and Language
Computation and Language
AI summaryⓘ
The authors created FormalRx, a new way to better understand and improve how computers turn natural language math statements into formal math expressions. Instead of just giving a pass/fail or a score, FormalRx breaks down mistakes into 28 clear categories, explaining what went wrong and where. They also built a model, FormalRx-8B, to automatically diagnose these errors and showed it works better than existing methods. This helps researchers fix problems more precisely and make autoformalization systems smarter.
autoformalizationsemantic alignmentformal mathematical reasoningerror taxonomydiagnostic evaluationnatural language processinglarge language modelsF1-scoreerror localizationbenchmarks
Authors
Haocheng Wang, Baiyu Huang, Yingjia Wan, Xiao Zhu, Xiaoyang Liu, Yinya Huang, Zhijiang Guo
Abstract
The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why translations fail. This opacity severely limits both human understanding and automated system improvement. To bridge this gap, we introduce FormalRx, a comprehensive diagnostic evaluation framework that transforms autoformalization assessment from black-box judgments into actionable feedback. At its core is SCI Error Taxonomy, a hierarchical classification scheme decomposing autoformalization errors into 28 distinct categories with strict priority ordering. Building on this taxonomy, FormalRx provides four critical diagnostic capabilities: alignment verdicts, error categorization, error localization, and correction. We instantiate the framework with a diagnostic model FormalRx-8B, trained on 56,287 NL-FL pairs with fine-grained diagnostic annotations, and release FormalRx-Test as the first fine-grained diagnostic benchmark. FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), along with accuracies of 0.75 (localization) and 0.73 (correction), substantially outperforming both general-purpose LLMs and specialized baselines. By connecting evaluation with actionable insights, FormalRx enables systematic diagnosis and improvement of autoformalization systems.