FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

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 synthetically generated samples 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.

When AI systems translate mathematical statements from natural language into formal proof-checking code, they often introduce subtle errors that change the intended meaning. Existing tools can only flag a statement as correct or incorrect, giving no hint about what went wrong or how to fix it. This limits both human debugging and the ability of AI systems to improve themselves. We introduce FormalRx, a diagnostic framework that goes beyond binary judgments. We first designed a taxonomy of 28 error categories covering the ways a formal statement can diverge from its natural language source. We then used this taxonomy to build a large dataset of annotated examples and trained a model that, in a single step, identifies whether an error exists, classifies the error type, pinpoints its location, and suggests a correction. FormalRx gives researchers and AI systems the actionable feedback needed to systematically improve autoformalization quality. In our experiments, plugging FormalRx into an AI self-refinement loop improved the rate of correct formalizations by 7 percentage points over baselines that only provide binary feedback. As formal verification becomes increasingly central to trustworthy AI reasoning, tools like FormalRx that make the translation process transparent and correctable will be essential.