FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

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 the 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.

The SCI Error Taxonomy

The SCI taxonomy partitions autoformalization errors into three disjoint, exhaustive dimensions: Semantic, Constraint, and Implementation. Location-based catch-all categories ensure exhaustiveness, and a priority ordering resolves cases that match more than one.

Figure 2. Overview of the SCI taxonomy. 28 error categories are partitioned into three disjoint, exhaustive dimensions: Semantic (S), Constraint (C), and Implementation (I). Location-based catch-all categories (Premise, Conclusion, Auxiliary Construction) ensure exhaustiveness, and a priority ordering resolves cases that match more than one.

Data Synthesis Pipeline

We synthesize 56,287 annotated NL–FL pairs by taxonomy-guided error injection from 17,825 aligned seed pairs. An LLM agent introduces a targeted error for each applicable SCI category, a second LLM validates and re-tags, and candidates failing Lean compilation or the label check are discarded. Each surviving instance carries full diagnostic metadata: error category, location, reasoning, and corrected statement.

Figure 3. Overview of the data synthesis pipeline. From 17k aligned NL–FL seed pairs, an LLM agent applies taxonomy-guided error injection to produce misaligned candidates together with raw diagnostic labels. A second LLM then validates and re-tags each candidate against the SCI taxonomy; samples failing Lean compilation or the label check are discarded, leaving 56k annotated instances.

We release FormalRx-Test on Hugging Face: 7,030 natural-language / Lean 4 statement pairs annotated under the SCI Error Taxonomy. Each sample carries a natural-language problem, a candidate Lean 4 formalization, and a Lean header required to type-check the candidate.

Schema

Each sample is a JSON object:

{
  "idx":                "formalrx_1",
  "header":             "import Mathlib\nopen Real Set",
  "informal_statement": "...natural language problem...",
  "formal_statement":   "theorem ... := by sorry",
  "diagnosis": {
    "aligned":             "Aligned" | "Misaligned",
    "error_type":          "<one of 28 SCI categories>" | "N/A",
    "error_location":      "<minimal code snippet>" | "N/A",
    "corrected_statement": "<complete corrected Lean 4 statement>" | "N/A"
  }
}

Main Results on FormalRx-Test

On FormalRx-Test (7,030 samples), FormalRx-8B outperforms the strongest frontier baselines on every task: +23.4 pp over the best baseline on 28-class error categorization, while staying competitive on verdict prediction where base models already perform well.

Table 1. Main results on FormalRx-Test (7,030 samples). Underline marks the best baseline within each model category; bold + underline marks the overall best. FormalRx-8B attains the highest score on every task; the categorization gap (+23.4 pp over the strongest baseline) reflects the value of taxonomy-grounded supervision.

Scaling Across Model Sizes

Table 2. Performance across three FormalRx sizes. Verdict and categorization are well-learned even at 1.7B parameters, while the generative tasks (localization and correction) benefit most from scale: FormalRx-8B wins on both. The non-monotonic dip on categorization at 4B is consistent with the paper's observation that 28-class classification is sensitive to factors beyond raw scale.

BibTeX

@inproceedings{wang2026formalrx,
  title     = {FormalRx: Rectify and eXamine Semantic Failures in Autoformalization},
  author    = {Wang, Haocheng and Huang, Baiyu and Wan, Yingjia and Zhu, Xiao and Liu, Xiaoyang and Huang, Yinya and Guo, Zhijiang},
  booktitle = {Proceedings of the 43rd International Conference on Machine Learning},
  year      = {2026},
}