# FormalRx: Automated Formalization of Real-World Mathematical Proofs > FormalRx introduces a taxonomy-driven diagnostic framework that outperforms baselines in autoformalization error categorization by 23.4 F1 points, enabling actionable, fine-grained evaluation beyond binary verdicts. - **Source:** [arXiv](https://arxiv.org/abs/2607.04655) - **Published:** 2026-09-05 - **Permalink:** https://picx.dev/p/lBEtTr - **Whiteboard:** https://picx.dev/p/lBEtTr/image ## Summary ## Summary (Overview) - **Novel Diagnostic Framework**: FormalRx transforms autoformalization evaluation from opaque binary judgments into actionable, fine-grained diagnostics with four components: alignment verdict, error categorization, error localization, and statement correction. - **Sci Error Taxonomy**: A hierarchical classification scheme decomposing autoformalization errors into 28 distinct categories across three dimensions (Semantic, Constraint, Implementation) with strict priority ordering for unambiguous classification. - **State-of-the-Art Performance**: FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), with accuracies of 0.75 (localization) and 0.73 (correction), substantially outperforming general-purpose LLMs and specialized baselines. - **Large-Scale Diagnostic Dataset**: Construction of 56,287 NL-FL pairs with fine-grained diagnostic annotations through taxonomy-guided error injection, plus a 7,030-sample held-out benchmark (FormalRx-Test). - **Single-Pass Multi-Task Architecture**: A unified generative approach performing all four diagnostic tasks in a single forward pass, mitigating error propagation between cascaded stages. ## Introduction and Theoretical Foundation ### Background and Motivation Formal mathematical reasoning represents a frontier in AI for rigorous, verifiable logical inference. Proof assistants like Lean enable autoformalization—translating mathematical problems from natural language into formal statements—which serves as a critical bridge to mitigate reasoning unfaithfulness and hallucinations in LLMs. However, existing evaluation approaches suffer from fundamental limitations: 1. **Syntactic validity checks** (type-checking, BLEU scores) fail to capture semantic alignment 2. **Rule-based equivalence checks** achieve high precision but suffer from low recall and limited domain coverage 3. **LLM-as-judge methods** reduce semantic correctness to binary verdicts with no interpretable feedback ### Data Foundation The training data consists of **17,825 aligned NL-FL pairs** from curated datasets including Formal-MATH, FIMO, Compfiles, PutnamBench, ProverBench, CombiBench, and Gaokao-Formal, plus Mathlib library entries. Notably, MiniF2F and ProofNet were deliberately excluded due to documented alignment issues. ## Methodology ### Sci Error Taxonomy The taxonomy formally partitions the error space $\mathcal{E}$ into three dimensions $\mathcal{P} = \{S, C, I\}$ where for any distinct dimensions $D_1, D_2 \in \mathcal{P}$: $$D_1 \cap D_2 = \emptyset \quad \text{and} \quad \bigcup_{D \in \mathcal{P}} D = \mathcal{E}$$ **Semantic Errors (S1–S3):** - **S1 Logical structure**: Errors at the propositional level (quantifier/connective misuse) - **S2 Mathematical objects**: Misrepresentation of types, functions, operators, exponents, coefficients - **S3 Mathematical concepts**: Deeper misunderstandings (infinity, cardinality, geometric relationships) **Constraint Errors (C1–C5):** - **C1 Variable constraints**: Missing, redundant, or incorrect admissible value ranges - **C2 Range errors**: Misspecified iteration domains for sums, products, or index sets - **C3–C5** Location-based catch-alls: premise, conclusion, and auxiliary construction errors **Implementation Errors (I1–I2):** - **I1 Truncation errors**: Discrete numeric type deviations (e.g., $3 - 5 = 0$ over ℕ) - **I2 Precedence errors**: Parser binds operators differently than standard notation ### Training Objective Standard SFT with negative log-likelihood loss: $$\mathcal{L}_{\mathrm{SFT}}(\theta) = -\sum_{i=1}^{N} \sum_{t=1}^{T_i} \log p_\theta(y_{i,t} \mid \mathcal{S}_i, \mathcal{F}_i, y_{i,